diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp index 5fbf8bd94..689917f32 100644 --- a/src/storm/storage/Scheduler.cpp +++ b/src/storm/storage/Scheduler.cpp @@ -241,7 +241,7 @@ namespace storm { } storm::json stateChoicesJson; if (model && model->hasStateValuations()) { - stateChoicesJson["s"] = model->getStateValuations()[state].toJson(model->getStateValuations()); + stateChoicesJson["s"] = model->getStateValuations().toJson(state); } else { stateChoicesJson["s"] = state; } diff --git a/src/storm/storage/sparse/StateValuations.cpp b/src/storm/storage/sparse/StateValuations.cpp index 93409c860..b1d70b81b 100644 --- a/src/storm/storage/sparse/StateValuations.cpp +++ b/src/storm/storage/sparse/StateValuations.cpp @@ -10,71 +10,78 @@ namespace storm { namespace storage { namespace sparse { - StateValuation::StateValuation(std::vector&& booleanValues, std::vector&& integerValues, std::vector&& rationalValues) : booleanValues(std::move(booleanValues)), integerValues(std::move(integerValues)), rationalValues(std::move(rationalValues)) { + StateValuations::StateValuation::StateValuation(std::vector&& booleanValues, std::vector&& integerValues, std::vector&& rationalValues) : booleanValues(std::move(booleanValues)), integerValues(std::move(integerValues)), rationalValues(std::move(rationalValues)) { // 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> const& selectedVariables) const { - STORM_LOG_ASSERT(assertValuations(valuations), "Invalid state valuations"); - typename std::map::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> const& selectedVariables) const { + auto const& valuation = getValuation(stateIndex); + typename std::map::const_iterator mapIt = variableToIndexMap.begin(); typename std::set::const_iterator setIt; if (selectedVariables) { setIt = selectedVariables->begin(); } std::vector 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 if (selectedVariables) { while (mapIt->first != *setIt) { ++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; std::stringstream stream; if (pretty) { - if (variable.hasBooleanType() && !booleanValues[mapIt->second]) { + if (variable.hasBooleanType() && !valuation.booleanValues[mapIt->second]) { stream << "!"; } stream << variable.getName(); if (variable.hasIntegerType()) { - stream << "=" << integerValues[mapIt->second]; + stream << "=" << valuation.integerValues[mapIt->second]; } else if (variable.hasRationalType()) { - stream << "=" << rationalValues[mapIt->second]; + stream << "=" << valuation.rationalValues[mapIt->second]; } else { STORM_LOG_THROW(variable.hasBooleanType(), storm::exceptions::InvalidTypeException, "Unexpected variable type."); } } else { if (variable.hasBooleanType()) { - stream << std::boolalpha << booleanValues[mapIt->second] << std::noboolalpha; + stream << std::boolalpha << valuation.booleanValues[mapIt->second] << std::noboolalpha; } else if (variable.hasIntegerType()) { - stream << integerValues[mapIt->second]; + stream << valuation.integerValues[mapIt->second]; } else if (variable.hasRationalType()) { - stream << rationalValues[mapIt->second]; + stream << valuation.rationalValues[mapIt->second]; } } assignments.push_back(stream.str()); @@ -93,30 +100,30 @@ namespace storm { } } - typename StateValuation::Json StateValuation::toJson(StateValuations const& valuations, boost::optional> const& selectedVariables) const { - STORM_LOG_ASSERT(assertValuations(valuations), "Invalid state valuations"); - typename std::map::const_iterator mapIt = valuations.variableToIndexMap.begin(); + typename StateValuations::Json StateValuations::toJson(storm::storage::sparse::state_type const& stateIndex, boost::optional> const& selectedVariables) const { + auto const& valuation = getValuation(stateIndex); + typename std::map::const_iterator mapIt = variableToIndexMap.begin(); typename std::set::const_iterator setIt; if (selectedVariables) { setIt = selectedVariables->begin(); } 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 if (selectedVariables) { while (mapIt->first != *setIt) { ++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; if (variable.hasBooleanType()) { - result[variable.getName()] = bool(booleanValues[mapIt->second]); + result[variable.getName()] = bool(valuation.booleanValues[mapIt->second]); } else if (variable.hasIntegerType()) { - result[variable.getName()] = integerValues[mapIt->second]; + result[variable.getName()] = valuation.integerValues[mapIt->second]; } else if (variable.hasRationalType()) { - result[variable.getName()] = rationalValues[mapIt->second]; + result[variable.getName()] = valuation.rationalValues[mapIt->second]; } else { STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unexpected variable type."); } @@ -131,11 +138,11 @@ namespace storm { 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; if (varIndex.first.hasBooleanType()) { bv = &foundBooleanValues; @@ -169,19 +176,9 @@ namespace storm { std::string StateValuations::getStateInfo(state_type const& state) const { 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]; + return this->toString(state); } - StateValuation const& StateValuations::operator[](storm::storage::sparse::state_type const& state) const { - STORM_LOG_ASSERT(state < getNumberOfStates(), "Invalid state index."); - return valuations[state]; - } - uint_fast64_t StateValuations::getNumberOfStates() const { return valuations.size(); } @@ -228,8 +225,8 @@ namespace storm { if (state == currentStateValuations.valuations.size()) { currentStateValuations.valuations.emplace_back(std::move(booleanValues), std::move(integerValues), std::move(rationalValues)); } 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)); } } diff --git a/src/storm/storage/sparse/StateValuations.h b/src/storm/storage/sparse/StateValuations.h index 873f49f33..43edda895 100644 --- a/src/storm/storage/sparse/StateValuations.h +++ b/src/storm/storage/sparse/StateValuations.h @@ -13,21 +13,38 @@ namespace storm { namespace storage { namespace sparse { - class StateValuations; 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: + friend class StateValuationsBuilder; typedef storm::json Json; - StateValuation() = default; - StateValuation(std::vector&& booleanValues, std::vector&& integerValues, std::vector&& 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&& booleanValues, std::vector&& integerValues, std::vector&& rationalValues); + + private: + + std::vector booleanValues; + std::vector integerValues; + std::vector rationalValues; + }; + + + StateValuations() = default; + + virtual ~StateValuations() = default; + virtual std::string getStateInfo(storm::storage::sparse::state_type const& state) const override; - // Returns true, if this valuation does not contain any value. - bool isEmpty() const; + 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. @@ -35,41 +52,15 @@ namespace storm { * @param selectedVariables If given, only the informations for the variables in this set are processed. * @return The string representation. */ - std::string toString(StateValuations const& valuations, bool pretty = true, boost::optional> const& selectedVariables = boost::none) const; + std::string toString(storm::storage::sparse::state_type const& stateIndex, bool pretty = true, boost::optional> const& selectedVariables = boost::none) const; /*! * Returns a JSON representation of this valuation * @param selectedVariables If given, only the informations for the variables in this set are processed. * @return */ - Json toJson(StateValuations const& valuations, boost::optional> 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 booleanValues; - std::vector integerValues; - std::vector 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; + Json toJson(storm::storage::sparse::state_type const& stateIndex, boost::optional> const& selectedVariables = boost::none) const; - 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; - // Returns the (current) number of states that this object describes. uint_fast64_t getNumberOfStates() const; @@ -88,6 +79,9 @@ namespace storm { private: StateValuations(std::map const& variableToIndexMap, std::vector&& valuations); + bool assertValuation(StateValuation const& valuation) const; + StateValuation const& getValuation(storm::storage::sparse::state_type const& stateIndex) const; + std::map variableToIndexMap; // A mapping from state indices to their variable valuations. std::vector valuations;