Skip to content

Commit

Permalink
Added two functions for more convenient access to state valuations
Browse files Browse the repository at this point in the history
* prism::Program::getAllExpressionVariables now has the possibility to not include constants
* added storage::sparse::StateValuations::getIntegerValues() and similar for other types, to provide access to all state values of a given variable
  • Loading branch information
tquatmann committed Dec 21, 2024
1 parent eceee50 commit 1f9a84d
Show file tree
Hide file tree
Showing 4 changed files with 50 additions and 4 deletions.
8 changes: 5 additions & 3 deletions src/storm/storage/prism/Program.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -487,11 +487,13 @@ std::vector<IntegerVariable> const& Program::getGlobalIntegerVariables() const {
return this->globalIntegerVariables;
}

std::set<storm::expressions::Variable> Program::getAllExpressionVariables() const {
std::set<storm::expressions::Variable> Program::getAllExpressionVariables(bool includeConstants) const {
std::set<storm::expressions::Variable> result;

for (auto const& constant : constants) {
result.insert(constant.getExpressionVariable());
if (includeConstants) {
for (auto const& constant : constants) {
result.insert(constant.getExpressionVariable());
}
}
for (auto const& variable : globalBooleanVariables) {
result.insert(variable.getExpressionVariable());
Expand Down
3 changes: 2 additions & 1 deletion src/storm/storage/prism/Program.h
Original file line number Diff line number Diff line change
Expand Up @@ -258,9 +258,10 @@ class Program : public LocatedInformation {
/*!
* Retrieves all expression variables used by this program.
*
* @param includeConstants Whether to include constants in the set of expression variables.
* @return The set of expression variables used by this program.
*/
std::set<storm::expressions::Variable> getAllExpressionVariables() const;
std::set<storm::expressions::Variable> getAllExpressionVariables(bool includeConstants = true) const;

/*!
* Retrieves a list of expressions that characterize the legal ranges of all variables.
Expand Down
28 changes: 28 additions & 0 deletions src/storm/storage/sparse/StateValuations.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -164,6 +164,34 @@ storm::RationalNumber const& StateValuations::getRationalValue(storm::storage::s
return valuation.rationalValues[variableToIndexMap.at(rationalVariable)];
}

storm::storage::BitVector StateValuations::getBooleanValues(storm::expressions::Variable const& booleanVariable) const {
storm::storage::BitVector result(getNumberOfStates(), false);
for (uint64_t stateIndex = 0; stateIndex < getNumberOfStates(); ++stateIndex) {
if (getBooleanValue(stateIndex, booleanVariable)) {
result.set(stateIndex);
}
}
return result;
}

std::vector<int64_t> StateValuations::getIntegerValues(storm::expressions::Variable const& integerVariable) const {
std::vector<int64_t> result;
result.reserve(getNumberOfStates());
for (uint64_t stateIndex = 0; stateIndex < getNumberOfStates(); ++stateIndex) {
result.push_back(getIntegerValue(stateIndex, integerVariable));
}
return result;
}

std::vector<storm::RationalNumber> StateValuations::getRationalValues(storm::expressions::Variable const& rationalVariable) const {
std::vector<storm::RationalNumber> result;
result.reserve(getNumberOfStates());
for (uint64_t stateIndex = 0; stateIndex < getNumberOfStates(); ++stateIndex) {
result.push_back(getRationalValue(stateIndex, rationalVariable));
}
return result;
}

bool StateValuations::isEmpty(storm::storage::sparse::state_type const& stateIndex) const {
auto const& valuation = valuations[stateIndex]; // Do not use getValuations, as that is only valid after adding stuff.
return valuation.booleanValues.empty() && valuation.integerValues.empty() && valuation.rationalValues.empty() && valuation.observationLabelValues.empty();
Expand Down
15 changes: 15 additions & 0 deletions src/storm/storage/sparse/StateValuations.h
Original file line number Diff line number Diff line change
Expand Up @@ -101,6 +101,21 @@ class StateValuations : public storm::models::sparse::StateAnnotation {
/// Returns true, if this valuation does not contain any value.
bool isEmpty(storm::storage::sparse::state_type const& stateIndex) const;

/*!
* Returns a vector of size getNumberOfStates() such that the i'th entry is the value of the given variable of state i.
*/
storm::storage::BitVector getBooleanValues(storm::expressions::Variable const& booleanVariable) const;

/*!
* Returns a vector of size getNumberOfStates() such that the i'th entry is the value of the given variable of state i.
*/
std::vector<int64_t> getIntegerValues(storm::expressions::Variable const& integerVariable) const;

/*!
* Returns a vector of size getNumberOfStates() such that the i'th entry is the value of the given variable of state i.
*/
std::vector<storm::RationalNumber> getRationalValues(storm::expressions::Variable const& rationalVariable) const;

/*!
* Returns a string representation of the valuation.
*
Expand Down

0 comments on commit 1f9a84d

Please sign in to comment.