improved state valuations class

src/storm/builder/BuilderOptions.cpp

@@ -35,7 +35,7 @@ namespace storm {
             return boost::get<storm::expressions::Expression>(labelOrExpression);
         }
         
-        BuilderOptions::BuilderOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false), buildChoiceOrigins(false), explorationChecks(false) {
+        BuilderOptions::BuilderOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false), buildStateValuations(false), buildChoiceOrigins(false), explorationChecks(false) {
             // Intentionally left empty.
         }
         
@@ -139,6 +139,10 @@ namespace storm {
             return buildChoiceLabels;
         }
         
+       bool BuilderOptions::isBuildStateValuationsSet() const {
+            return buildStateValuations;
+        }
+        
         bool BuilderOptions::isBuildChoiceOriginsSet() const {
             return buildChoiceOrigins;
         }
@@ -202,6 +206,11 @@ namespace storm {
             return *this;
         }
         
+        BuilderOptions& BuilderOptions::setBuildStateValuations(bool newValue) {
+            buildStateValuations = newValue;
+            return *this;
+        }
+ 
         BuilderOptions& BuilderOptions::setBuildChoiceOrigins(bool newValue) {
             buildChoiceOrigins = newValue;
             return *this;

src/storm/builder/BuilderOptions.h

@@ -89,6 +89,7 @@ namespace storm {
             bool hasTerminalStates() const;
             void clearTerminalStates();
             bool isBuildChoiceLabelsSet() const;
+            bool isBuildStateValuationsSet() const;
             bool isBuildChoiceOriginsSet() const;
             bool isBuildAllRewardModelsSet() const;
             bool isBuildAllLabelsSet() const;
@@ -102,6 +103,7 @@ namespace storm {
             BuilderOptions& addTerminalExpression(storm::expressions::Expression const& expression, bool value);
             BuilderOptions& addTerminalLabel(std::string const& label, bool value);
             BuilderOptions& setBuildChoiceLabels(bool newValue);
+            BuilderOptions& setBuildStateValuations(bool newValue);
             BuilderOptions& setBuildChoiceOrigins(bool newValue);
             BuilderOptions& setExplorationChecks(bool newValue);
             
@@ -128,6 +130,9 @@ namespace storm {
             /// A flag indicating whether or not to build choice labels.
             bool buildChoiceLabels;
                          
+            /// A flag indicating whether or not to build for each state the variable valuation from which it originates.
+            bool buildStateValuations;
+            
             // A flag that indicates whether or not to generate the information from which parts of the model specification
             // each choice originates.
             bool buildChoiceOrigins;

src/storm/builder/ExplicitModelBuilder.cpp

@@ -308,11 +308,12 @@ namespace storm {
             modelComponents.choiceLabeling = choiceInformationBuilder.buildChoiceLabeling(modelComponents.transitionMatrix.getRowCount());
             
             // if requested, build the state valuations and choice origins
-            if (options.buildStateValuations) {
-                modelComponents.stateValuations = std::make_shared<storm::storage::sparse::StateValuations>(stateStorage.getNumberOfStates());
+            if (generator->getOptions().isBuildStateValuationsSet()) {
+                std::vector<storm::expressions::SimpleValuation> valuations(modelComponents.transitionMatrix.getRowGroupCount());
                 for (auto const& bitVectorIndexPair : stateStorage.stateToId) {
-                    modelComponents.stateValuations->valuations[bitVectorIndexPair.second] = generator->toValuation(bitVectorIndexPair.first);
+                    valuations[bitVectorIndexPair.second] = generator->toValuation(bitVectorIndexPair.first);
                 }
+                modelComponents.stateValuations = storm::storage::sparse::StateValuations(std::move(valuations));
             }
             auto originData = choiceInformationBuilder.buildDataOfChoiceOrigins(modelComponents.transitionMatrix.getRowCount());
             modelComponents.choiceOrigins = generator->generateChoiceOrigins(originData);

src/storm/builder/ExplicitModelBuilder.h

@@ -16,7 +16,6 @@
 #include "storm/storage/expressions/ExpressionEvaluator.h"
 #include "storm/storage/BitVectorHashMap.h"
 #include "storm/logic/Formulas.h"
-#include "storm/models/sparse/StateAnnotation.h"
 #include "storm/models/sparse/Model.h"
 #include "storm/models/sparse/StateLabeling.h"
 #include "storm/models/sparse/ChoiceLabeling.h"
@@ -70,11 +69,11 @@ namespace storm {
                 // A vector that stores which states are markovian.
                 boost::optional<storm::storage::BitVector> markovianStates;
                 
-                // Stores for each state to which variable valuation it belongs (is nullptr if not generated)
-                std::shared_ptr<storm::storage::sparse::StateValuations> stateValuations;
+                // If generated, stores for each state to which variable valuation it belongs
+                boost::optional<storm::storage::sparse::StateValuations> stateValuations;
                 
-                // Stores for each choice from which parts of the input model description it originates (is nullptr if not generated)
-                std::shared_ptr<storm::storage::sparse::ChoiceOrigins> choiceOrigins;
+                // If generated, stores for each choice from which parts of the input model description it originates
+                boost::optional<std::shared_ptr<storm::storage::sparse::ChoiceOrigins>> choiceOrigins;
 
             };
             
@@ -86,10 +85,6 @@ namespace storm {
                 
                 // The order in which to explore the model.
                 ExplorationOrder explorationOrder;
-                
-                // A flag that indicates whether or not to store the state information after successfully building the
-                // model. If it is to be preserved, it is contained in the result obtained from <code> build </code>
-                bool buildStateValuations;
             };
             
             /*!

src/storm/models/sparse/StateAnnotation.h

@@ -9,7 +9,7 @@ namespace storm {
             
             class StateAnnotation {
             public:
-                virtual std::string stateInfo(storm::storage::sparse::state_type const& state) const = 0;
+                virtual std::string getStateInfo(storm::storage::sparse::state_type const& state) const = 0;
             };
             
         }

src/storm/storage/sparse/StateValuations.cpp

@@ -1,17 +1,43 @@
 #include "storm/storage/sparse/StateValuations.h"
 
+#include "storm/utility/vector.h"
+
 namespace storm {
     namespace storage {
         namespace sparse {
             
-            StateValuations::StateValuations(state_type const& numberOfStates) : valuations(numberOfStates) {
+            StateValuations::StateValuations(std::vector<storm::expressions::SimpleValuation> const& valuations) : valuations(valuations) {
+                // Intentionally left empty.
+            }
+                        
+            StateValuations::StateValuations(std::vector<storm::expressions::SimpleValuation>&& valuations) : valuations(std::move(valuations)) {
                 // Intentionally left empty.
             }
             
-            std::string StateValuations::stateInfo(state_type const& state) const {
-                return valuations[state].toString();
+            std::string StateValuations::getStateInfo(state_type const& state) const {
+                return getStateValuation(state).toString();
+            }
+            
+            storm::expressions::SimpleValuation const& StateValuations::getStateValuation(storm::storage::sparse::state_type const& state) const {
+                return valuations[state];
             }
 
+            StateValuations StateValuations::selectStates(storm::storage::BitVector const& selectedStates) const {
+                return StateValuations(storm::utility::vector::filterVector(valuations, selectedStates));
+            }
+
+            StateValuations StateValuations::selectStates(std::vector<storm::storage::sparse::state_type> const& selectedStates) const {
+                std::vector<storm::expressions::SimpleValuation> selectedValuations;
+                selectedValuations.reserve(selectedStates.size());
+                for (auto const& selectedState : selectedStates){
+                    if (selectedState < valuations.size()) {
+                        selectedValuations.push_back(valuations[selectedState]);
+                    } else {
+                        selectedValuations.emplace_back();
+                    }
+                }
+                return StateValuations(std::move(selectedValuations));
+            }
         }
     }
 }

src/storm/storage/sparse/StateValuations.h

@@ -5,8 +5,8 @@
 #include <string>
 
 #include "storm/storage/sparse/StateType.h"
+#include "storm/storage/BitVector.h"
 #include "storm/storage/expressions/SimpleValuation.h"
-
 #include "storm/models/sparse/StateAnnotation.h"
 
 namespace storm {
@@ -14,18 +14,38 @@ namespace storm {
         namespace sparse {
             
             // A structure holding information about the reachable state space that can be retrieved from the outside.
-            struct StateValuations : public storm::models::sparse::StateAnnotation {
+            class StateValuations : public storm::models::sparse::StateAnnotation {
+            
+            public:
                 /*!
                  * Constructs a state information object for the given number of states.
                  */
-                StateValuations(state_type const& numberOfStates);
+                StateValuations(std::vector<storm::expressions::SimpleValuation> const& valuations);
+                StateValuations(std::vector<storm::expressions::SimpleValuation>&& valuations);
                 
                 virtual ~StateValuations() = default;
                 
+                virtual std::string getStateInfo(storm::storage::sparse::state_type const& state) const override;
+                storm::expressions::SimpleValuation const& getStateValuation(storm::storage::sparse::state_type const& state) const;
+                
+                /*
+                 * Derive new state valuations from this by selecting the given states.
+                 */
+                StateValuations selectStates(storm::storage::BitVector const& selectedStates) const;
+                
+                /*
+                 * Derive new state valuations from this by selecting the given states.
+                 * If an invalid state index is selected, the corresponding valuation will be empty.
+                 */
+                StateValuations selectStates(std::vector<storm::storage::sparse::state_type> const& selectedStates) const;
+
+                
+                
+            private:
+                
                 // A mapping from state indices to their variable valuations.
                 std::vector<storm::expressions::SimpleValuation> valuations;
                 
-                virtual std::string stateInfo(state_type const& state) const override;
             };
             
         }