sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Hiding the StateValuation object of a single state.

main
Tim Quatmann 6 years ago
parent
adfdf8c572
commit
3b68059e2b
3 changed files with 81 additions and 90 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      src/storm/storage/Scheduler.cpp
  2. 101
      src/storm/storage/sparse/StateValuations.cpp
  3. 68
      src/storm/storage/sparse/StateValuations.h

2
src/storm/storage/Scheduler.cpp
View File

@ -241,7 +241,7 @@ namespace storm {
} }
storm::json<storm::RationalNumber> stateChoicesJson; storm::json<storm::RationalNumber> stateChoicesJson;
if (model && model->hasStateValuations()) { if (model && model->hasStateValuations()) {
stateChoicesJson["s"] = model->getStateValuations()[state].toJson(model->getStateValuations());
stateChoicesJson["s"] = model->getStateValuations().toJson(state);
} else { } else {
stateChoicesJson["s"] = state; stateChoicesJson["s"] = state;
} }

101
src/storm/storage/sparse/StateValuations.cpp
View File

@ -10,71 +10,78 @@ namespace storm {
namespace storage { namespace storage {
namespace sparse { namespace sparse {
StateValuation::StateValuation(std::vector<bool>&& booleanValues, std::vector<int64_t>&& integerValues, std::vector<storm::RationalNumber>&& rationalValues) : booleanValues(std::move(booleanValues)), integerValues(std::move(integerValues)), rationalValues(std::move(rationalValues)) {
StateValuations::StateValuation::StateValuation(std::vector<bool>&& booleanValues, std::vector<int64_t>&& integerValues, std::vector<storm::RationalNumber>&& rationalValues) : booleanValues(std::move(booleanValues)), integerValues(std::move(integerValues)), rationalValues(std::move(rationalValues)) {
// Intentionally left empty // Intentionally left empty
} }
bool StateValuation::getBooleanValue(StateValuations const& valuations, storm::expressions::Variable const& booleanVariable) const {
STORM_LOG_ASSERT(assertValuations(valuations), "Invalid state valuations");
STORM_LOG_ASSERT(valuations.variableToIndexMap.count(booleanVariable) > 0, "Variable " << booleanVariable.getName() << " is not part of this valuation.");
return booleanValues[valuations.variableToIndexMap.at(booleanVariable)];
typename StateValuations::StateValuation const& StateValuations::getValuation(storm::storage::sparse::state_type const& stateIndex) const {
STORM_LOG_ASSERT(stateIndex < valuations.size(), "Invalid state index.");
STORM_LOG_ASSERT(assertValuation(valuations[stateIndex]), "Invalid state valuations");
return valuations[stateIndex];
} }
int64_t const& StateValuation::getIntegerValue(StateValuations const& valuations, storm::expressions::Variable const& integerVariable) const {
STORM_LOG_ASSERT(assertValuations(valuations), "Invalid state valuations");
STORM_LOG_ASSERT(valuations.variableToIndexMap.count(integerVariable) > 0, "Variable " << integerVariable.getName() << " is not part of this valuation.");
return integerValues[valuations.variableToIndexMap.at(integerVariable)];
bool StateValuations::getBooleanValue(storm::storage::sparse::state_type const& stateIndex, storm::expressions::Variable const& booleanVariable) const {
auto const& valuation = getValuation(stateIndex);
STORM_LOG_ASSERT(variableToIndexMap.count(booleanVariable) > 0, "Variable " << booleanVariable.getName() << " is not part of this valuation.");
return valuation.booleanValues[variableToIndexMap.at(booleanVariable)];
} }
storm::RationalNumber const& StateValuation::getRationalValue(StateValuations const& valuations, storm::expressions::Variable const& rationalVariable) const {
STORM_LOG_ASSERT(assertValuations(valuations), "Invalid state valuations");
STORM_LOG_ASSERT(valuations.variableToIndexMap.count(rationalVariable) > 0, "Variable " << rationalVariable.getName() << " is not part of this valuation.");
return rationalValues[valuations.variableToIndexMap.at(rationalVariable)];
int64_t const& StateValuations::getIntegerValue(storm::storage::sparse::state_type const& stateIndex, storm::expressions::Variable const& integerVariable) const {
auto const& valuation = getValuation(stateIndex);
STORM_LOG_ASSERT(variableToIndexMap.count(integerVariable) > 0, "Variable " << integerVariable.getName() << " is not part of this valuation.");
return valuation.integerValues[variableToIndexMap.at(integerVariable)];
} }
bool StateValuation::isEmpty() const {
return booleanValues.empty() && integerValues.empty() && rationalValues.empty();
storm::RationalNumber const& StateValuations::getRationalValue(storm::storage::sparse::state_type const& stateIndex, storm::expressions::Variable const& rationalVariable) const {
auto const& valuation = getValuation(stateIndex);
STORM_LOG_ASSERT(variableToIndexMap.count(rationalVariable) > 0, "Variable " << rationalVariable.getName() << " is not part of this valuation.");
return valuation.rationalValues[variableToIndexMap.at(rationalVariable)];
} }
std::string StateValuation::toString(StateValuations const& valuations, bool pretty, boost::optional<std::set<storm::expressions::Variable>> const& selectedVariables) const {
STORM_LOG_ASSERT(assertValuations(valuations), "Invalid state valuations");
typename std::map<storm::expressions::Variable, uint64_t>::const_iterator mapIt = valuations.variableToIndexMap.begin();
bool StateValuations::isEmpty(storm::storage::sparse::state_type const& stateIndex) const {
auto const& valuation = getValuation(stateIndex);
return valuation.booleanValues.empty() && valuation.integerValues.empty() && valuation.rationalValues.empty();
}
std::string StateValuations::toString(storm::storage::sparse::state_type const& stateIndex, bool pretty, boost::optional<std::set<storm::expressions::Variable>> const& selectedVariables) const {
auto const& valuation = getValuation(stateIndex);
typename std::map<storm::expressions::Variable, uint64_t>::const_iterator mapIt = variableToIndexMap.begin();
typename std::set<storm::expressions::Variable>::const_iterator setIt; typename std::set<storm::expressions::Variable>::const_iterator setIt;
if (selectedVariables) { if (selectedVariables) {
setIt = selectedVariables->begin(); setIt = selectedVariables->begin();
} }
std::vector<std::string> assignments; std::vector<std::string> assignments;
while (mapIt != valuations.variableToIndexMap.end() && (!selectedVariables || setIt != selectedVariables->end())) {
while (mapIt != variableToIndexMap.end() && (!selectedVariables || setIt != selectedVariables->end())) {
// Move Map iterator to next relevant position // Move Map iterator to next relevant position
if (selectedVariables) { if (selectedVariables) {
while (mapIt->first != *setIt) { while (mapIt->first != *setIt) {
++mapIt; ++mapIt;
STORM_LOG_ASSERT(mapIt != valuations.variableToIndexMap.end(), "Valuation does not consider selected variable " << setIt->getName() << ".");
STORM_LOG_ASSERT(mapIt != variableToIndexMap.end(), "Valuation does not consider selected variable " << setIt->getName() << ".");
} }
} }
auto const& variable = mapIt->first; auto const& variable = mapIt->first;
std::stringstream stream; std::stringstream stream;
if (pretty) { if (pretty) {
if (variable.hasBooleanType() && !booleanValues[mapIt->second]) {
if (variable.hasBooleanType() && !valuation.booleanValues[mapIt->second]) {
stream << "!"; stream << "!";
} }
stream << variable.getName(); stream << variable.getName();
if (variable.hasIntegerType()) { if (variable.hasIntegerType()) {
stream << "=" << integerValues[mapIt->second];
stream << "=" << valuation.integerValues[mapIt->second];
} else if (variable.hasRationalType()) { } else if (variable.hasRationalType()) {
stream << "=" << rationalValues[mapIt->second];
stream << "=" << valuation.rationalValues[mapIt->second];
} else { } else {
STORM_LOG_THROW(variable.hasBooleanType(), storm::exceptions::InvalidTypeException, "Unexpected variable type."); STORM_LOG_THROW(variable.hasBooleanType(), storm::exceptions::InvalidTypeException, "Unexpected variable type.");
} }
} else { } else {
if (variable.hasBooleanType()) { if (variable.hasBooleanType()) {
stream << std::boolalpha << booleanValues[mapIt->second] << std::noboolalpha;
stream << std::boolalpha << valuation.booleanValues[mapIt->second] << std::noboolalpha;
} else if (variable.hasIntegerType()) { } else if (variable.hasIntegerType()) {
stream << integerValues[mapIt->second];
stream << valuation.integerValues[mapIt->second];
} else if (variable.hasRationalType()) { } else if (variable.hasRationalType()) {
stream << rationalValues[mapIt->second];
stream << valuation.rationalValues[mapIt->second];
} }
} }
assignments.push_back(stream.str()); assignments.push_back(stream.str());
@ -93,30 +100,30 @@ namespace storm {
} }
} }
typename StateValuation::Json StateValuation::toJson(StateValuations const& valuations, boost::optional<std::set<storm::expressions::Variable>> const& selectedVariables) const {
STORM_LOG_ASSERT(assertValuations(valuations), "Invalid state valuations");
typename std::map<storm::expressions::Variable, uint64_t>::const_iterator mapIt = valuations.variableToIndexMap.begin();
typename StateValuations::Json StateValuations::toJson(storm::storage::sparse::state_type const& stateIndex, boost::optional<std::set<storm::expressions::Variable>> const& selectedVariables) const {
auto const& valuation = getValuation(stateIndex);
typename std::map<storm::expressions::Variable, uint64_t>::const_iterator mapIt = variableToIndexMap.begin();
typename std::set<storm::expressions::Variable>::const_iterator setIt; typename std::set<storm::expressions::Variable>::const_iterator setIt;
if (selectedVariables) { if (selectedVariables) {
setIt = selectedVariables->begin(); setIt = selectedVariables->begin();
} }
Json result; Json result;
while (mapIt != valuations.variableToIndexMap.end() && (!selectedVariables || setIt != selectedVariables->end())) {
while (mapIt != variableToIndexMap.end() && (!selectedVariables || setIt != selectedVariables->end())) {
// Move Map iterator to next relevant position // Move Map iterator to next relevant position
if (selectedVariables) { if (selectedVariables) {
while (mapIt->first != *setIt) { while (mapIt->first != *setIt) {
++mapIt; ++mapIt;
STORM_LOG_ASSERT(mapIt != valuations.variableToIndexMap.end(), "Valuation does not consider selected variable " << setIt->getName() << ".");
STORM_LOG_ASSERT(mapIt != variableToIndexMap.end(), "Valuation does not consider selected variable " << setIt->getName() << ".");
} }
} }
auto const& variable = mapIt->first; auto const& variable = mapIt->first;
if (variable.hasBooleanType()) { if (variable.hasBooleanType()) {
result[variable.getName()] = bool(booleanValues[mapIt->second]);
result[variable.getName()] = bool(valuation.booleanValues[mapIt->second]);
} else if (variable.hasIntegerType()) { } else if (variable.hasIntegerType()) {
result[variable.getName()] = integerValues[mapIt->second];
result[variable.getName()] = valuation.integerValues[mapIt->second];
} else if (variable.hasRationalType()) { } else if (variable.hasRationalType()) {
result[variable.getName()] = rationalValues[mapIt->second];
result[variable.getName()] = valuation.rationalValues[mapIt->second];
} else { } else {
STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unexpected variable type."); STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unexpected variable type.");
} }
@ -131,11 +138,11 @@ namespace storm {
return result; return result;
} }
bool StateValuation::assertValuations(StateValuations const& valuations) const {
storm::storage::BitVector foundBooleanValues(booleanValues.size(), false);
storm::storage::BitVector foundIntegerValues(integerValues.size(), false);
storm::storage::BitVector foundRationalValues(rationalValues.size(), false);
for (auto const& varIndex : valuations.variableToIndexMap) {
bool StateValuations::assertValuation(StateValuation const& valuation) const {
storm::storage::BitVector foundBooleanValues(valuation.booleanValues.size(), false);
storm::storage::BitVector foundIntegerValues(valuation.integerValues.size(), false);
storm::storage::BitVector foundRationalValues(valuation.rationalValues.size(), false);
for (auto const& varIndex : variableToIndexMap) {
storm::storage::BitVector* bv; storm::storage::BitVector* bv;
if (varIndex.first.hasBooleanType()) { if (varIndex.first.hasBooleanType()) {
bv = &foundBooleanValues; bv = &foundBooleanValues;
@ -169,17 +176,7 @@ namespace storm {
std::string StateValuations::getStateInfo(state_type const& state) const { std::string StateValuations::getStateInfo(state_type const& state) const {
STORM_LOG_ASSERT(state < getNumberOfStates(), "Invalid state index."); STORM_LOG_ASSERT(state < getNumberOfStates(), "Invalid state index.");
return (*this)[state].toString(*this);
}
StateValuation& StateValuations::operator[](storm::storage::sparse::state_type const& state) {
STORM_LOG_ASSERT(state < getNumberOfStates(), "Invalid state index.");
return valuations[state];
}
StateValuation const& StateValuations::operator[](storm::storage::sparse::state_type const& state) const {
STORM_LOG_ASSERT(state < getNumberOfStates(), "Invalid state index.");
return valuations[state];
return this->toString(state);
} }
uint_fast64_t StateValuations::getNumberOfStates() const { uint_fast64_t StateValuations::getNumberOfStates() const {
@ -228,8 +225,8 @@ namespace storm {
if (state == currentStateValuations.valuations.size()) { if (state == currentStateValuations.valuations.size()) {
currentStateValuations.valuations.emplace_back(std::move(booleanValues), std::move(integerValues), std::move(rationalValues)); currentStateValuations.valuations.emplace_back(std::move(booleanValues), std::move(integerValues), std::move(rationalValues));
} else { } else {
STORM_LOG_ASSERT(currentStateValuations[state].isEmpty(), "Adding a valuation to the same state multiple times.");
currentStateValuations[state] = StateValuation(std::move(booleanValues), std::move(integerValues), std::move(rationalValues));
STORM_LOG_ASSERT(currentStateValuations.isEmpty(state), "Adding a valuation to the same state multiple times.");
currentStateValuations.valuations[state] = typename StateValuations::StateValuation(std::move(booleanValues), std::move(integerValues), std::move(rationalValues));
} }
} }

68
src/storm/storage/sparse/StateValuations.h
View File

@ -13,21 +13,38 @@ namespace storm {
namespace storage { namespace storage {
namespace sparse { namespace sparse {
class StateValuations;
class StateValuationsBuilder; class StateValuationsBuilder;
class StateValuation {
// A structure holding information about the reachable state space that can be retrieved from the outside.
class StateValuations : public storm::models::sparse::StateAnnotation {
public: public:
friend class StateValuationsBuilder;
typedef storm::json<storm::RationalNumber> Json; typedef storm::json<storm::RationalNumber> Json;
StateValuation() = default;
StateValuation(std::vector<bool>&& booleanValues, std::vector<int64_t>&& integerValues, std::vector<storm::RationalNumber>&& rationalValues);
bool getBooleanValue(StateValuations const& valuations, storm::expressions::Variable const& booleanVariable) const;
int64_t const& getIntegerValue(StateValuations const& valuations, storm::expressions::Variable const& integerVariable) const;
storm::RationalNumber const& getRationalValue(StateValuations const& valuations, storm::expressions::Variable const& rationalVariable) const;
class StateValuation {
public:
friend class StateValuations;
StateValuation() = default;
StateValuation(std::vector<bool>&& booleanValues, std::vector<int64_t>&& integerValues, std::vector<storm::RationalNumber>&& rationalValues);
private:
// Returns true, if this valuation does not contain any value.
bool isEmpty() const;
std::vector<bool> booleanValues;
std::vector<int64_t> integerValues;
std::vector<storm::RationalNumber> rationalValues;
};
StateValuations() = default;
virtual ~StateValuations() = default;
virtual std::string getStateInfo(storm::storage::sparse::state_type const& state) const override;
bool getBooleanValue(storm::storage::sparse::state_type const& stateIndex, storm::expressions::Variable const& booleanVariable) const;
int64_t const& getIntegerValue(storm::storage::sparse::state_type const& stateIndex, storm::expressions::Variable const& integerVariable) const;
storm::RationalNumber const& getRationalValue(storm::storage::sparse::state_type const& stateIndex, storm::expressions::Variable const& rationalVariable) const;
/// Returns true, if this valuation does not contain any value.
bool isEmpty(storm::storage::sparse::state_type const& stateIndex) const;
/*! /*!
* Returns a string representation of the valuation. * Returns a string representation of the valuation.
@ -35,40 +52,14 @@ namespace storm {
* @param selectedVariables If given, only the informations for the variables in this set are processed. * @param selectedVariables If given, only the informations for the variables in this set are processed.
* @return The string representation. * @return The string representation.
*/ */
std::string toString(StateValuations const& valuations, bool pretty = true, boost::optional<std::set<storm::expressions::Variable>> const& selectedVariables = boost::none) const;
std::string toString(storm::storage::sparse::state_type const& stateIndex, bool pretty = true, boost::optional<std::set<storm::expressions::Variable>> const& selectedVariables = boost::none) const;
/*! /*!
* Returns a JSON representation of this valuation * Returns a JSON representation of this valuation
* @param selectedVariables If given, only the informations for the variables in this set are processed. * @param selectedVariables If given, only the informations for the variables in this set are processed.
* @return * @return
*/ */
Json toJson(StateValuations const& valuations, boost::optional<std::set<storm::expressions::Variable>> const& selectedVariables = boost::none) const;
private:
// Asserts whether the variable and value counts for each type match.
bool assertValuations(StateValuations const& valuations) const;
std::vector<bool> booleanValues;
std::vector<int64_t> integerValues;
std::vector<storm::RationalNumber> rationalValues;
};
// A structure holding information about the reachable state space that can be retrieved from the outside.
class StateValuations : public storm::models::sparse::StateAnnotation {
public:
friend class StateValuation;
friend class StateValuationsBuilder;
StateValuations() = default;
virtual ~StateValuations() = default;
virtual std::string getStateInfo(storm::storage::sparse::state_type const& state) const override;
/*!
* Returns the valuation at the specific state
*/
StateValuation& operator[](storm::storage::sparse::state_type const& state);
StateValuation const& operator[](storm::storage::sparse::state_type const& state) const;
Json toJson(storm::storage::sparse::state_type const& stateIndex, boost::optional<std::set<storm::expressions::Variable>> const& selectedVariables = boost::none) const;
// Returns the (current) number of states that this object describes. // Returns the (current) number of states that this object describes.
@ -88,6 +79,9 @@ namespace storm {
private: private:
StateValuations(std::map<storm::expressions::Variable, uint64_t> const& variableToIndexMap, std::vector<StateValuation>&& valuations); StateValuations(std::map<storm::expressions::Variable, uint64_t> const& variableToIndexMap, std::vector<StateValuation>&& valuations);
bool assertValuation(StateValuation const& valuation) const;
StateValuation const& getValuation(storm::storage::sparse::state_type const& stateIndex) const;
std::map<storm::expressions::Variable, uint64_t> variableToIndexMap; std::map<storm::expressions::Variable, uint64_t> variableToIndexMap;
// A mapping from state indices to their variable valuations. // A mapping from state indices to their variable valuations.
std::vector<StateValuation> valuations; std::vector<StateValuation> valuations;

Write Preview
Loading…
Cancel
Save