From 3b68059e2be8d005263ee0e4bd6c6f5a492e186f Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 25 May 2020 17:38:26 +0200
Subject: [PATCH] Hiding the StateValuation object of a single state.

---
 src/storm/storage/Scheduler.cpp              |   2 +-
 src/storm/storage/sparse/StateValuations.cpp | 101 +++++++++----------
 src/storm/storage/sparse/StateValuations.h   |  68 ++++++-------
 3 files changed, 81 insertions(+), 90 deletions(-)

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<storm::RationalNumber> 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<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
             }
             
-            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;
                 if (selectedVariables) {
                     setIt = selectedVariables->begin();
                 }
                 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
                     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<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;
                 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<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:
+                    
+                    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;
                 
-                // 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<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
                  * @param selectedVariables If given, only the informations for the variables in this set are processed.
                  * @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;
+                Json toJson(storm::storage::sparse::state_type const& stateIndex, boost::optional<std::set<storm::expressions::Variable>> 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<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;
                 // A mapping from state indices to their variable valuations.
                 std::vector<StateValuation> valuations;