moved some internal structs from model builder to their own files to make them reusable

Former-commit-id: a354059fe8

src/builder/ExplicitPrismModelBuilder.cpp

@@ -62,39 +62,24 @@ namespace storm {
             // The state-action reward vector.
             std::vector<ValueType> stateActionRewardVector;
         };
-        
-        template <typename ValueType, typename RewardModelType, typename StateType>
-        ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::StateInformation::StateInformation(uint_fast64_t numberOfStates) : valuations(numberOfStates) {
-            // Intentionally left empty.
-        }
-        
-        template <typename ValueType, typename RewardModelType, typename StateType>
-        ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::InternalStateInformation::InternalStateInformation() : stateStorage(64, 10), initialStateIndices(), bitsPerState(64), numberOfStates() {
-            // Intentionally left empty.
-        }
-        
-        template <typename ValueType, typename RewardModelType, typename StateType>
-        ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::InternalStateInformation::InternalStateInformation(uint64_t bitsPerState) : stateStorage(bitsPerState, 10000000), initialStateIndices(), bitsPerState(bitsPerState), numberOfStates() {
-            // Intentionally left empty.
-        }
-        
+                        
         template <typename ValueType, typename RewardModelType, typename StateType>
         ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), rewardModels(), choiceLabeling() {
             // Intentionally left empty.
         }
         
         template <typename ValueType, typename RewardModelType, typename StateType>
-        ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::Options::Options() : explorationOrder(storm::settings::generalSettings().getExplorationOrder()), buildCommandLabels(false), buildAllRewardModels(true), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
+        ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::Options::Options() : explorationOrder(storm::settings::generalSettings().getExplorationOrder()), buildCommandLabels(false), buildAllRewardModels(true), buildStateValuations(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
             // Intentionally left empty.
         }
         
         template <typename ValueType, typename RewardModelType, typename StateType>
-        ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::Options::Options(storm::logic::Formula const& formula) : explorationOrder(storm::settings::generalSettings().getExplorationOrder()), buildCommandLabels(false), buildAllRewardModels(false), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()), terminalStates(), negatedTerminalStates() {
+        ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::Options::Options(storm::logic::Formula const& formula) : explorationOrder(storm::settings::generalSettings().getExplorationOrder()), buildCommandLabels(false), buildAllRewardModels(false), buildStateValuations(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()), terminalStates(), negatedTerminalStates() {
             this->preserveFormula(formula);
         }
         
         template <typename ValueType, typename RewardModelType, typename StateType>
-        ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::Options::Options(std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) : explorationOrder(storm::settings::generalSettings().getExplorationOrder()), buildCommandLabels(false), buildAllRewardModels(false), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
+        ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::Options::Options(std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) : explorationOrder(storm::settings::generalSettings().getExplorationOrder()), buildCommandLabels(false), buildAllRewardModels(false), buildStateValuations(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
             if (formulas.empty()) {
                 this->buildAllRewardModels = true;
                 this->buildAllLabels = true;
@@ -182,19 +167,14 @@ namespace storm {
         }
         
         template <typename ValueType, typename RewardModelType, typename StateType>
-        ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::ExplicitPrismModelBuilder(storm::prism::Program const& program, Options const& options) : program(storm::utility::prism::preprocessProgram<ValueType>(program, options.constantDefinitions, !options.buildAllLabels ? options.labelsToBuild : boost::none, options.expressionLabels)), options(options) {
-
-            // Create the variable information for the transformed program.
-            this->variableInformation = VariableInformation(this->program);
-            
-            // Create the internal state storage.
-            this->internalStateInformation = InternalStateInformation(variableInformation.getTotalBitOffset(true));
+        ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::ExplicitPrismModelBuilder(storm::prism::Program const& program, Options const& options) : program(storm::utility::prism::preprocessProgram<ValueType>(program, options.constantDefinitions, !options.buildAllLabels ? options.labelsToBuild : boost::none, options.expressionLabels)), options(options), variableInformation(this->program), stateStorage(variableInformation.getTotalBitOffset(true)) {
+            // Intentionally left empty.
         }
         
         template <typename ValueType, typename RewardModelType, typename StateType>
-        typename ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::StateInformation const& ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::getStateInformation() const {
-            STORM_LOG_THROW(static_cast<bool>(stateInformation), storm::exceptions::InvalidOperationException, "The state information was not properly build.");
-            return stateInformation.get();
+        storm::storage::sparse::StateValuations const& ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::getStateValuations() const {
+            STORM_LOG_THROW(static_cast<bool>(stateValuations), storm::exceptions::InvalidOperationException, "The state information was not properly build.");
+            return stateValuations.get();
         }
         
         template <typename ValueType, typename RewardModelType, typename StateType>
@@ -261,10 +241,10 @@ namespace storm {
         
         template <typename ValueType, typename RewardModelType, typename StateType>
         StateType ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::getOrAddStateIndex(CompressedState const& state) {
-            uint32_t newIndex = internalStateInformation.numberOfStates;
+            uint32_t newIndex = stateStorage.numberOfStates;
             
             // Check, if the state was already registered.
-            std::pair<uint32_t, std::size_t> actualIndexBucketPair = internalStateInformation.stateStorage.findOrAddAndGetBucket(state, newIndex);
+            std::pair<uint32_t, std::size_t> actualIndexBucketPair = stateStorage.stateToId.findOrAddAndGetBucket(state, newIndex);
             
             if (actualIndexBucketPair.first == newIndex) {
                 if (options.explorationOrder == ExplorationOrder::Dfs) {
@@ -277,7 +257,7 @@ namespace storm {
                 } else {
                     STORM_LOG_ASSERT(false, "Invalid exploration order.");
                 }
-                ++internalStateInformation.numberOfStates;
+                ++stateStorage.numberOfStates;
             }
             
             return actualIndexBucketPair.first;
@@ -311,7 +291,7 @@ namespace storm {
             }
             
             // Let the generator create all initial states.
-            this->internalStateInformation.initialStateIndices = generator.getInitialStates(stateToIdCallback);
+            this->stateStorage.initialStateIndices = generator.getInitialStates(stateToIdCallback);
             
             // Now explore the current state until there is no more reachable state.
             uint_fast64_t currentRowGroup = 0;
@@ -321,7 +301,7 @@ namespace storm {
             while (!statesToExplore.empty()) {
                 // Get the first state in the queue.
                 CompressedState currentState = statesToExplore.front();
-                StateType currentIndex = internalStateInformation.stateStorage.getValue(currentState);
+                StateType currentIndex = stateStorage.stateToId.getValue(currentState);
                 statesToExplore.pop_front();
                 
                 // If the exploration order differs from breadth-first, we remember that this row group was actually
@@ -426,13 +406,13 @@ namespace storm {
                 transitionMatrixBuilder.replaceColumns(remapping, 0);
 
                 // Fix (b).
-                std::vector<StateType> newInitialStateIndices(this->internalStateInformation.initialStateIndices.size());
-                std::transform(this->internalStateInformation.initialStateIndices.begin(), this->internalStateInformation.initialStateIndices.end(), newInitialStateIndices.begin(), [&remapping] (StateType const& state) { return remapping[state]; } );
+                std::vector<StateType> newInitialStateIndices(this->stateStorage.initialStateIndices.size());
+                std::transform(this->stateStorage.initialStateIndices.begin(), this->stateStorage.initialStateIndices.end(), newInitialStateIndices.begin(), [&remapping] (StateType const& state) { return remapping[state]; } );
                 std::sort(newInitialStateIndices.begin(), newInitialStateIndices.end());
-                this->internalStateInformation.initialStateIndices = std::move(newInitialStateIndices);
+                this->stateStorage.initialStateIndices = std::move(newInitialStateIndices);
                 
                 // Fix (c).
-                this->internalStateInformation.stateStorage.remap([&remapping] (StateType const& state) { return remapping[state]; } );
+                this->stateStorage.stateToId.remap([&remapping] (StateType const& state) { return remapping[state]; } );
             }
             
             return choiceLabels;
@@ -497,10 +477,10 @@ namespace storm {
             modelComponents.stateLabeling = buildStateLabeling();
             
             // Finally -- if requested -- build the state information that can be retrieved from the outside.
-            if (options.buildStateInformation) {
-                stateInformation = StateInformation(internalStateInformation.numberOfStates);
-                for (auto const& bitVectorIndexPair : internalStateInformation.stateStorage) {
-                    stateInformation.get().valuations[bitVectorIndexPair.second] = unpackStateIntoValuation(bitVectorIndexPair.first);
+            if (options.buildStateValuations) {
+                stateValuations = storm::storage::sparse::StateValuations(stateStorage.numberOfStates);
+                for (auto const& bitVectorIndexPair : stateStorage.stateToId) {
+                    stateValuations.get().valuations[bitVectorIndexPair.second] = unpackStateIntoValuation(bitVectorIndexPair.first);
                 }
             }
             
@@ -510,7 +490,7 @@ namespace storm {
         template <typename ValueType, typename RewardModelType, typename StateType>
         storm::models::sparse::StateLabeling ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::buildStateLabeling() {
             storm::generator::PrismStateLabelingGenerator<ValueType, StateType> generator(program, variableInformation);
-            return generator.generate(internalStateInformation.stateStorage, internalStateInformation.initialStateIndices);
+            return generator.generate(stateStorage.stateToId, stateStorage.initialStateIndices);
         }
         
         // Explicitly instantiate the class.

src/builder/ExplicitPrismModelBuilder.h

@@ -20,6 +20,8 @@
 #include "src/models/sparse/Model.h"
 #include "src/models/sparse/StateLabeling.h"
 #include "src/storage/SparseMatrix.h"
+#include "src/storage/sparse/StateValuations.h"
+#include "src/storage/sparse/StateStorage.h"
 #include "src/settings/SettingsManager.h"
 
 #include "src/utility/prism.h"
@@ -45,42 +47,6 @@ namespace storm {
         template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename StateType = uint32_t>
         class ExplicitPrismModelBuilder {
         public:
-            // A structure holding information about the reachable state space while building it.
-            struct InternalStateInformation {
-                // Builds an empty state information.
-                InternalStateInformation();
-                
-                // Creates a state information structure for storing states of the given bit width.
-                InternalStateInformation(uint64_t bitsPerState);
-
-                // This member stores all the states and maps them to their unique indices.
-                storm::storage::BitVectorHashMap<StateType> stateStorage;
-                
-                // A list of initial states in terms of their global indices.
-                std::vector<StateType> initialStateIndices;
-
-                // The number of bits of each state.
-                uint64_t bitsPerState;
-                
-                // The number of states that were found in the exploration so far.
-                uint_fast64_t numberOfStates;
-            };
-            
-            // A structure holding information about the reachable state space that can be retrieved from the outside.
-            struct StateInformation : public storm::models::sparse::StateAnnotation {
-                /*!
-                 * Constructs a state information object for the given number of states.
-                 */
-                StateInformation(uint_fast64_t numberOfStates);
-                
-                // A mapping from state indices to their variable valuations.
-                std::vector<storm::expressions::SimpleValuation> valuations;
-
-                std::string stateInfo(uint_fast64_t state) const override {
-                    return valuations[state].toString();
-                }
-            };
-            
             // A structure holding the individual components of a model.
             struct ModelComponents {
                 ModelComponents();
@@ -163,7 +129,7 @@ namespace storm {
                 // A flag that indicates whether or not to store the state information after successfully building the
                 // model. If it is to be preserved, it can be retrieved via the appropriate methods after a successful
                 // call to <code>translateProgram</code>.
-                bool buildStateInformation;
+                bool buildStateValuations;
                 
                 // A list of reward models to be build in case not all reward models are to be build.
                 std::set<std::string> rewardModelsToBuild;
@@ -214,7 +180,7 @@ namespace storm {
              *
              * @return A structure that stores information about all reachable states.
              */
-            StateInformation const& getStateInformation() const;
+            storm::storage::sparse::StateValuations const& getStateValuations() const;
             
             /*!
              * Retrieves the program that was actually translated (i.e. including constant substitutions etc.).
@@ -233,7 +199,6 @@ namespace storm {
              * used after invoking this method.
              *
              * @param state A pointer to a state for which to retrieve the index. This must not be used after the call.
-             * @param internalStateInformation The information about the already explored part of the reachable state space.
              * @return A pair indicating whether the state was already discovered before and the state id of the state.
              */
             StateType getOrAddStateIndex(CompressedState const& state);
@@ -245,7 +210,6 @@ namespace storm {
              * @param variableInformation A structure containing information about the variables in the program.
              * @param transitionRewards A list of transition rewards that are to be considered in the transition reward
              * matrix.
-             * @param internalStateInformation A structure containing information about the states of the program.
              * @param deterministicModel A flag indicating whether the model is supposed to be deterministic or not.
              * @param transitionMatrix A reference to an initialized matrix which is filled with all transitions by this
              * function.
@@ -270,9 +234,6 @@ namespace storm {
             /*!
              * Builds the state labeling for the given program.
              *
-             * @param program The program for which to build the state labeling.
-             * @param variableInformation Information about the variables in the program.
-             * @param internalStateInformation Information about the state space of the program.
              * @return The state labeling of the given program.
              */
             storm::models::sparse::StateLabeling buildStateLabeling();
@@ -287,11 +248,11 @@ namespace storm {
             VariableInformation variableInformation;
             
             // Internal information about the states that were explored.
-            InternalStateInformation internalStateInformation;
+            storm::storage::sparse::StateStorage<StateType> stateStorage;
             
             // This member holds information about reachable states that can be retrieved from the outside after a
             // successful build.
-            boost::optional<StateInformation> stateInformation;
+            boost::optional<storm::storage::sparse::StateValuations> stateValuations;
             
             // A set of states that still need to be explored.
             std::deque<CompressedState> statesToExplore;

src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp

@@ -2,27 +2,38 @@
 
 #include "src/logic/FragmentSpecification.h"
 
+#include "src/utility/prism.h"
+
 #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 
 namespace storm {
     namespace modelchecker {
-        template<typename SparseMdpModelType>
-        SparseMdpLearningModelChecker<SparseMdpModelType>::SparseMdpLearningModelChecker(storm::prism::Program const& program) : program(program) {
+        template<typename ValueType>
+        SparseMdpLearningModelChecker<ValueType>::SparseMdpLearningModelChecker(storm::prism::Program const& program) : program(storm::utility::prism::preprocessProgram<ValueType>(program)), variableInformation(this->program), generator(program, variableInformation, false) {
             // Intentionally left empty.
         }
         
-        template<typename SparseMdpModelType>
-        bool SparseMdpLearningModelChecker<SparseMdpModelType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const {
+        template<typename ValueType>
+        bool SparseMdpLearningModelChecker<ValueType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const {
             storm::logic::Formula const& formula = checkTask.getFormula();
             storm::logic::FragmentSpecification fragment = storm::logic::propositional().setProbabilityOperatorsAllowed(true).setReachabilityProbabilityFormulasAllowed(true);
             return formula.isInFragment(fragment);
         }
         
-        template<typename SparseMdpModelType>
-        std::unique_ptr<CheckResult> SparseMdpLearningModelChecker<SparseMdpModelType>::computeReachabilityProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+        template<typename ValueType>
+        std::unique_ptr<CheckResult> SparseMdpLearningModelChecker<ValueType>::computeReachabilityProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+            
+            // Create a callback for the next-state generator to enable it to request the index of states.
+            std::function<StateType (storm::generator::CompressedState const&)> stateToIdCallback = std::bind(&SparseMdpLearningModelChecker<ValueType>::getOrAddStateIndex, this, std::placeholders::_1);
+
             return nullptr;
         }
         
+        template<typename ValueType>
+        typename SparseMdpLearningModelChecker<ValueType>::StateType SparseMdpLearningModelChecker<ValueType>::getOrAddStateIndex(storm::generator::CompressedState const& state) {
+            
+        }
+        
         template class SparseMdpLearningModelChecker<double>;
     }
 }

src/modelchecker/reachability/SparseMdpLearningModelChecker.h

@@ -5,6 +5,9 @@
 
 #include "src/storage/prism/Program.h"
 
+#include "src/generator/PrismNextStateGenerator.h"
+#include "src/generator/VariableInformation.h"
+
 #include "src/utility/constants.h"
 
 namespace storm {
@@ -13,6 +16,8 @@ namespace storm {
         template<typename ValueType>
         class SparseMdpLearningModelChecker : public AbstractModelChecker {
         public:
+            typedef uint32_t StateType;
+            
             SparseMdpLearningModelChecker(storm::prism::Program const& program);
             
             virtual bool canHandle(CheckTask<storm::logic::Formula> const& checkTask) const override;
@@ -20,8 +25,16 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeReachabilityProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
             
         private:
+            StateType getOrAddStateIndex(storm::generator::CompressedState const& state);
+            
             // The program that defines the model to check.
             storm::prism::Program program;
+            
+            // The variable information.
+            storm::generator::VariableInformation variableInformation;
+            
+            // A generator used to explore the model.
+            storm::generator::PrismNextStateGenerator<ValueType, StateType> generator;
         };
     }
 }

src/models/sparse/StateAnnotation.h

@@ -1,16 +1,19 @@
-#ifndef STORM_STATEANNOTATION_H
-#define STORM_STATEANNOTATION_H
+#ifndef STORM_MODELS_SPARSE_STATEANNOTATION_H_
+#define STORM_MODELS_SPARSE_STATEANNOTATION_H_
+
+#include "src/storage/sparse/StateType.h"
 
 namespace storm {
     namespace models {
         namespace sparse {
+            
             class StateAnnotation {
             public:
-                virtual std::string stateInfo(uint_fast64_t s) const = 0;
+                virtual std::string stateInfo(storm::storage::sparse::state_type const& state) const = 0;
             };
+            
         }
     }
-
 }
 
-#endif //STORM_STATEANNOTATION_H
+#endif /* STORM_MODELS_SPARSE_STATEANNOTATION_H_ */

src/storage/sparse/StateStorage.cpp

@@ -0,0 +1,15 @@
+#include "src/storage/sparse/StateStorage.h"
+
+namespace storm {
+    namespace storage {
+        namespace sparse {
+                        
+            template <typename StateType>
+            StateStorage<StateType>::StateStorage(uint64_t bitsPerState) : stateToId(bitsPerState, 10000000), initialStateIndices(), bitsPerState(bitsPerState), numberOfStates() {
+                // Intentionally left empty.
+            }
+
+            template class StateStorage<uint32_t>;
+        }
+    }
+}

src/storage/sparse/StateStorage.h

@@ -0,0 +1,35 @@
+#ifndef STORM_STORAGE_SPARSE_STATESTORAGE_H_
+#define STORM_STORAGE_SPARSE_STATESTORAGE_H_
+
+#include <cstdint>
+
+#include "src/storage/BitVectorHashMap.h"
+
+namespace storm {
+    namespace storage {
+        namespace sparse {
+            
+            // A structure holding information about the reachable state space while building it.
+            template <typename StateType>
+            struct StateStorage {
+                // Creates an empty state storage structure for storing states of the given bit width.
+                StateStorage(uint64_t bitsPerState);
+                
+                // This member stores all the states and maps them to their unique indices.
+                storm::storage::BitVectorHashMap<StateType> stateToId;
+                
+                // A list of initial states in terms of their global indices.
+                std::vector<StateType> initialStateIndices;
+                
+                // The number of bits of each state.
+                uint64_t bitsPerState;
+                
+                // The number of states that were found in the exploration so far.
+                uint_fast64_t numberOfStates;
+            };
+            
+        }
+    }
+}
+
+#endif /* STORM_STORAGE_SPARSE_STATESTORAGE_H_ */

src/storage/sparse/StateValuations.cpp

@@ -0,0 +1,17 @@
+#include "src/storage/sparse/StateValuations.h"
+
+namespace storm {
+    namespace storage {
+        namespace sparse {
+            
+            StateValuations::StateValuations(state_type const& numberOfStates) : valuations(numberOfStates) {
+                // Intentionally left empty.
+            }
+            
+            std::string StateValuations::stateInfo(state_type const& state) const {
+                return valuations[state].toString();
+            }
+            
+        }
+    }
+}

src/storage/sparse/StateValuations.h

@@ -0,0 +1,33 @@
+#ifndef STORM_STORAGE_SPARSE_STATEVALUATIONS_H_
+#define STORM_STORAGE_SPARSE_STATEVALUATIONS_H_
+
+#include <cstdint>
+#include <string>
+
+#include "src/storage/sparse/StateType.h"
+#include "src/storage/expressions/SimpleValuation.h"
+
+#include "src/models/sparse/StateAnnotation.h"
+
+namespace storm {
+    namespace storage {
+        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 {
+                /*!
+                 * Constructs a state information object for the given number of states.
+                 */
+                StateValuations(state_type const& numberOfStates);
+                
+                // 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;
+            };
+            
+        }
+    }
+}
+
+#endif /* STORM_STORAGE_SPARSE_STATEVALUATIONS_H_ */