started working on more flexible model generation using next-state-generators

Former-commit-id: 805940f179

src/CMakeLists.txt

@@ -11,6 +11,8 @@ file(GLOB_RECURSE STORM_SOURCES_CLI ${PROJECT_SOURCE_DIR}/src/cli/*.cpp)
 file(GLOB_RECURSE STORM_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm.cpp)
 file(GLOB_RECURSE STORM_ADAPTERS_FILES ${PROJECT_SOURCE_DIR}/src/adapters/*.h ${PROJECT_SOURCE_DIR}/src/adapters/*.cpp)
 file(GLOB_RECURSE STORM_BUILDER_FILES ${PROJECT_SOURCE_DIR}/src/builder/*.h ${PROJECT_SOURCE_DIR}/src/builder/*.cpp)
+file(GLOB STORM_GENERATOR_FILES ${PROJECT_SOURCE_DIR}/src/generator/*.h ${PROJECT_SOURCE_DIR}/src/generator/*.cpp)
+file(GLOB_RECURSE STORM_GENERATOR_PRISM_FILES ${PROJECT_SOURCE_DIR}/src/generator/prism/*.h ${PROJECT_SOURCE_DIR}/src/generator/prism/*.cpp)
 file(GLOB_RECURSE STORM_CLI_FILES ${PROJECT_SOURCE_DIR}/src/cli/*.h ${PROJECT_SOURCE_DIR}/src/cli/*.cpp)
 file(GLOB_RECURSE STORM_EXCEPTIONS_FILES ${PROJECT_SOURCE_DIR}/src/exceptions/*.h ${PROJECT_SOURCE_DIR}/src/exceptions/*.cpp)
 file(GLOB_RECURSE STORM_LOGIC_FILES ${PROJECT_SOURCE_DIR}/src/logic/*.h ${PROJECT_SOURCE_DIR}/src/logic/*.cpp)
@@ -57,6 +59,8 @@ set(STORM_MAIN_HEADERS ${STORM_HEADERS_CLI})
 source_group(main FILES ${STORM_MAIN_FILE})
 source_group(adapters FILES ${STORM_ADAPTERS_FILES})
 source_group(builder FILES ${STORM_BUILDER_FILES})
+source_group(generator FILES ${STORM_GENERATOR_FILES})
+source_group(generator\\prism FILES ${STORM_GENERATOR_PRISM_FILES})
 source_group(cli FILES ${STORM_CLI_FILES})
 source_group(exceptions FILES ${STORM_EXCEPTIONS_FILES})
 source_group(logic FILES ${STORM_LOGIC_FILES})

src/builder/ExplicitPrismModelBuilder.cpp

@@ -75,44 +75,7 @@ namespace storm {
         ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::InternalStateInformation::InternalStateInformation(uint64_t bitsPerState) : stateStorage(bitsPerState, 10000000), bitsPerState(bitsPerState), reachableStates() {
             // Intentionally left empty.
         }
-        
-        template <typename ValueType, typename RewardModelType, typename IndexType>
-        ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::VariableInformation::BooleanVariableInformation::BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset) : variable(variable), initialValue(initialValue), bitOffset(bitOffset) {
-            // Intentionally left empty.
-        }
-        
-        template <typename ValueType, typename RewardModelType, typename IndexType>
-        ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::VariableInformation::IntegerVariableInformation::IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t initialValue, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth) : variable(variable), initialValue(initialValue), lowerBound(lowerBound), upperBound(upperBound), bitOffset(bitOffset), bitWidth(bitWidth) {
-            // Intentionally left empty.
-        }
-        
-        template <typename ValueType, typename RewardModelType, typename IndexType>
-        ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::VariableInformation::VariableInformation(storm::expressions::ExpressionManager const& manager) : manager(manager) {
-            // Intentionally left empty.
-        }
-        
-        template <typename ValueType, typename RewardModelType, typename IndexType>
-        uint_fast64_t ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::VariableInformation::getBitOffset(storm::expressions::Variable const& variable) const {
-            auto const& booleanIndex = booleanVariableToIndexMap.find(variable);
-            if (booleanIndex != booleanVariableToIndexMap.end()) {
-                return booleanVariables[booleanIndex->second].bitOffset;
-            }
-            auto const& integerIndex = integerVariableToIndexMap.find(variable);
-            if (integerIndex != integerVariableToIndexMap.end()) {
-                return integerVariables[integerIndex->second].bitOffset;
-            }
-            STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit index of unknown variable.");
-        }
-
-        template <typename ValueType, typename RewardModelType, typename IndexType>
-        uint_fast64_t ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::VariableInformation::getBitWidth(storm::expressions::Variable const& variable) const {
-            auto const& integerIndex = integerVariableToIndexMap.find(variable);
-            if (integerIndex != integerVariableToIndexMap.end()) {
-                return integerVariables[integerIndex->second].bitWidth;
-            }
-            STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit width of unknown variable.");
-        }
-        
+            
         template <typename ValueType, typename RewardModelType, typename IndexType>
         ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), rewardModels(), choiceLabeling() {
             // Intentionally left empty.

src/builder/ExplicitPrismModelBuilder.h

@@ -74,60 +74,6 @@ namespace storm {
                 }
             };
             
-            // A structure storing information about the used variables of the program.
-            struct VariableInformation {
-                VariableInformation(storm::expressions::ExpressionManager const& manager);
-                
-                struct BooleanVariableInformation {
-                    BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset);
-                    
-                    // The boolean variable.
-                    storm::expressions::Variable variable;
-                    
-                    // Its initial value.
-                    bool initialValue;
-                    
-                    // Its bit offset in the compressed state.
-                    uint_fast64_t bitOffset;
-                };
-
-                struct IntegerVariableInformation {
-                    IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t initialValue, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth);
-                    
-                    // The integer variable.
-                    storm::expressions::Variable variable;
-                    
-                    // Its initial value.
-                    int_fast64_t initialValue;
-                    
-                    // The lower bound of its range.
-                    int_fast64_t lowerBound;
-                    
-                    // The upper bound of its range.
-                    int_fast64_t upperBound;
-                    
-                    // Its bit offset in the compressed state.
-                    uint_fast64_t bitOffset;
-                    
-                    // Its bit width in the compressed state.
-                    uint_fast64_t bitWidth;
-                };
-                
-                // Provide methods to access the bit offset and width of variables in the compressed state.
-                uint_fast64_t getBitOffset(storm::expressions::Variable const& variable) const;
-                uint_fast64_t getBitWidth(storm::expressions::Variable const& variable) const;
-
-                // The known boolean variables.
-                boost::container::flat_map<storm::expressions::Variable, uint_fast64_t> booleanVariableToIndexMap;
-                std::vector<BooleanVariableInformation> booleanVariables;
-
-                // The known integer variables.
-                boost::container::flat_map<storm::expressions::Variable, uint_fast64_t> integerVariableToIndexMap;
-                std::vector<IntegerVariableInformation> integerVariables;
-                
-                storm::expressions::ExpressionManager const& manager;
-            };
-            
             // A structure holding the individual components of a model.
             struct ModelComponents {
                 ModelComponents();

src/generator/Choice.cpp

@@ -0,0 +1,111 @@
+#include "src/generator/Choice.h"
+
+#include "src/utility/constants.h"
+
+namespace storm {
+    namespace generator {
+        
+        template<typename ValueType, typename StateType>
+        Choice<ValueType, StateType>::Choice(uint_fast64_t actionIndex, bool markovian) : markovian(markovian), actionIndex(actionIndex), distribution(), totalMass(storm::utility::zero<ValueType>()), choiceReward(storm::utility::zero<ValueType>()) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType, typename StateType>
+        typename storm::storage::Distribution<ValueType, StateType>::iterator Choice<ValueType, StateType>::begin() {
+            return distribution.begin();
+        }
+        
+        template<typename ValueType, typename StateType>
+        typename storm::storage::Distribution<ValueType, StateType>::const_iterator Choice<ValueType, StateType>::begin() const {
+            return distribution.cbegin();
+        }
+        
+        template<typename ValueType, typename StateType>
+        typename storm::storage::Distribution<ValueType, StateType>::iterator Choice<ValueType, StateType>::end() {
+            return distribution.end();
+        }
+        
+        template<typename ValueType, typename StateType>
+        typename storm::storage::Distribution<ValueType, StateType>::const_iterator Choice<ValueType, StateType>::end() const {
+            return distribution.cend();
+        }
+        
+        template<typename ValueType, typename StateType>
+        void Choice<ValueType, StateType>::addChoiceLabel(uint_fast64_t label) {
+            if (!choiceLabels) {
+                choiceLabels = LabelSet();
+            }
+            choiceLabels->insert(label);
+        }
+        
+        template<typename ValueType, typename StateType>
+        void Choice<ValueType, StateType>::addChoiceLabels(LabelSet const& labelSet) {
+            if (!choiceLabels) {
+                choiceLabels = LabelSet();
+            }
+            choiceLabels->insert(labelSet.begin(), labelSet.end());
+        }
+        
+        template<typename ValueType, typename StateType>
+        boost::container::flat_set<uint_fast64_t> const& Choice<ValueType, StateType>::getChoiceLabels() const {
+            return *choiceLabels;
+        }
+        
+        template<typename ValueType, typename StateType>
+        uint_fast64_t Choice<ValueType, StateType>::getActionIndex() const {
+            return actionIndex;
+        }
+        
+        template<typename ValueType, typename StateType>
+        ValueType Choice<ValueType, StateType>::getTotalMass() const {
+            return totalMass;
+        }
+        
+        template<typename ValueType, typename StateType>
+        ValueType& Choice<ValueType, StateType>::getOrAddEntry(StateType const& state) {
+            auto stateProbabilityPair = distribution.find(state);
+            
+            if (stateProbabilityPair == distribution.end()) {
+                distribution[state] = ValueType();
+            }
+            return distribution.at(state);
+        }
+        
+        template<typename ValueType, typename StateType>
+        ValueType const& Choice<ValueType, StateType>::getOrAddEntry(StateType const& state) const {
+            auto stateProbabilityPair = distribution.find(state);
+            
+            if (stateProbabilityPair == distribution.end()) {
+                distribution[state] = ValueType();
+            }
+            return distribution.at(state);
+        }
+        
+        template<typename ValueType, typename StateType>
+        void Choice<ValueType, StateType>::addProbability(StateType const& state, ValueType const& value) {
+            totalMass += value;
+            distribution[state] += value;
+        }
+        
+        template<typename ValueType, typename StateType>
+        void Choice<ValueType, StateType>::addChoiceReward(ValueType const& value) {
+            choiceReward += value;
+        }
+        
+        template<typename ValueType, typename StateType>
+        std::size_t Choice<ValueType, StateType>::size() const {
+            return distribution.size();
+        }
+        
+        template<typename ValueType, typename StateType>
+        std::ostream& operator<<(std::ostream& out, Choice<ValueType, StateType> const& choice) {
+            out << "<";
+            for (auto const& stateProbabilityPair : choice) {
+                out << stateProbabilityPair.first << " : " << stateProbabilityPair.second << ", ";
+            }
+            out << ">";
+            return out;
+        }
+        
+    }
+}

src/generator/Choice.h

@@ -0,0 +1,158 @@
+#ifndef STORM_GENERATOR_CHOICE_H_
+#define STORM_GENERATOR_CHOICE_H_
+
+#include <cstdint>
+#include <functional>
+
+#include <boost/optional.hpp>
+#include <boost/container/flat_set.hpp>
+
+#include "src/storage/Distribution.h"
+
+namespace storm {
+    namespace generator {
+        
+        // A structure holding information about a particular choice.
+        template<typename ValueType, typename StateType=uint32_t>
+        struct Choice {
+        public:
+            typedef boost::container::flat_set<uint_fast64_t> LabelSet;
+            
+            Choice(uint_fast64_t actionIndex = 0, bool markovian = false);
+            
+            Choice(Choice const& other) = default;
+            Choice& operator=(Choice const& other) = default;
+            Choice(Choice&& other) = default;
+            Choice& operator=(Choice&& other) = default;
+            
+            /*!
+             * Returns an iterator to the distribution associated with this choice.
+             *
+             * @return An iterator to the first element of the distribution.
+             */
+            typename storm::storage::Distribution<ValueType, StateType>::iterator begin();
+            
+            /*!
+             * Returns an iterator to the distribution associated with this choice.
+             *
+             * @return An iterator to the first element of the distribution.
+             */
+            typename storm::storage::Distribution<ValueType, StateType>::const_iterator begin() const;
+            
+            /*!
+             * Returns an iterator past the end of the distribution associated with this choice.
+             *
+             * @return An iterator past the end of the distribution.
+             */
+            typename storm::storage::Distribution<ValueType, StateType>::iterator end();
+            
+            /*!
+             * Returns an iterator past the end of the distribution associated with this choice.
+             *
+             * @return An iterator past the end of the distribution.
+             */
+            typename storm::storage::Distribution<ValueType, StateType>::const_iterator end() const;
+            
+            /*!
+             * Inserts the contents of this object to the given output stream.
+             *
+             * @param out The stream in which to insert the contents.
+             */
+            template<typename ValueTypePrime, typename StateTypePrime>
+            friend std::ostream& operator<<(std::ostream& out, Choice<ValueTypePrime, StateTypePrime> const& choice);
+            
+            /*!
+             * Adds the given label to the labels associated with this choice.
+             *
+             * @param label The label to associate with this choice.
+             */
+            void addChoiceLabel(uint_fast64_t label);
+            
+            /*!
+             * Adds the given label set to the labels associated with this choice.
+             *
+             * @param labelSet The label set to associate with this choice.
+             */
+            void addChoiceLabels(LabelSet const& labelSet);
+            
+            /*!
+             * Retrieves the set of labels associated with this choice.
+             *
+             * @return The set of labels associated with this choice.
+             */
+            LabelSet const& getChoiceLabels() const;
+            
+            /*!
+             * Retrieves the index of the action of this choice.
+             *
+             * @return The index of the action of this choice.
+             */
+            uint_fast64_t getActionIndex() const;
+            
+            /*!
+             * Retrieves the total mass of this choice.
+             *
+             * @return The total mass.
+             */
+            ValueType getTotalMass() const;
+            
+            /*!
+             * Retrieves the entry in the choice that is associated with the given state and creates one if none exists,
+             * yet.
+             *
+             * @param state The state for which to add the entry.
+             * @return A reference to the entry that is associated with the given state.
+             */
+            ValueType& getOrAddEntry(StateType const& state);
+            
+            /*!
+             * Retrieves the entry in the choice that is associated with the given state and creates one if none exists,
+             * yet.
+             *
+             * @param state The state for which to add the entry.
+             * @return A reference to the entry that is associated with the given state.
+             */
+            ValueType const& getOrAddEntry(StateType const& state) const;
+            
+            /*!
+             * Adds the given probability value to the given state in the underlying distribution.
+             */
+            void addProbability(StateType const& state, ValueType const& value);
+            
+            /*!
+             * Adds the given value to the reward associated with this choice.
+             */
+            void addChoiceReward(ValueType const& value);
+            
+            /*!
+             * Retrieves the size of the distribution associated with this choice.
+             */
+            std::size_t size() const;
+            
+        private:
+            // A flag indicating whether this choice is Markovian or not.
+            bool markovian;
+
+            // The action index associated with this choice.
+            uint_fast64_t actionIndex;
+            
+            // The distribution that is associated with the choice.
+            storm::storage::Distribution<ValueType, StateType> distribution;
+            
+            // The total probability mass (or rates) of this choice.
+            ValueType totalMass;
+            
+            // The reward value associated with this choice.
+            ValueType choiceReward;
+            
+            // The labels that are associated with this choice.
+            boost::optional<LabelSet> choiceLabels;
+        };
+
+        template<typename ValueType, typename StateType>
+        std::ostream& operator<<(std::ostream& out, Choice<ValueType, StateType> const& choice);
+
+    }
+}
+
+#endif /* STORM_GENERATOR_CHOICE_H_ */

src/generator/NextStateGenerator.h

@@ -0,0 +1,27 @@
+#ifndef STORM_GENERATOR_NEXTSTATEGENERATOR_H_
+#define STORM_GENERATOR_NEXTSTATEGENERATOR_H_
+
+#include <vector>
+#include <cstdint>
+
+#include "src/storage/sparse/StateType.h"
+#include "src/storage/BitVector.h"
+
+#include "src/generator/Choice.h"
+
+namespace storm {
+    namespace generator {
+        template<typename ValueType, typename StateType = uint32_t>
+        class NextStateGenerator {
+        public:
+            typedef storm::storage::BitVector InternalStateType;
+            typedef StateType (*StateToIdCallback)(InternalStateType const&);
+            
+            virtual std::vector<StateType> getInitialStates(StateToIdCallback stateToIdCallback) = 0;
+            virtual std::vector<Choice<ValueType>> expand(StateType const& state, StateToIdCallback stateToIdCallback) = 0;
+            virtual ValueType getStateReward(StateType const& state) = 0;
+        };
+    }
+}
+
+#endif

src/generator/PrismNextStateGenerator.cpp

@@ -0,0 +1,22 @@
+#include "src/generator/PrismNextStateGenerator.h"
+
+namespace storm {
+    namespace generator {
+        
+        template<typename ValueType, typename StateType>
+        PrismNextStateGenerator<ValueType, StateType>::PrismNextStateGenerator(storm::prism::Program const& program) : program(program) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType, typename StateType>
+        std::vector<Choice<ValueType>> PrismNextStateGenerator<ValueType, StateType>::expand(StateType const& state, typename NextStateGenerator<ValueType, StateType>::StateToIdCallback stateToIdCallback) {
+            // TODO
+        }
+        
+        template<typename ValueType, typename StateType>
+        ValueType PrismNextStateGenerator<ValueType, StateType>::getStateReward(StateType const& state) {
+            // TODO
+        }
+        
+    }
+}

src/generator/PrismNextStateGenerator.h

@@ -0,0 +1,32 @@
+#ifndef STORM_GENERATOR_PRISMNEXTSTATEGENERATOR_H_
+#define STORM_GENERATOR_PRISMNEXTSTATEGENERATOR_H_
+
+#include "src/generator/NextStateGenerator.h"
+
+#include "src/storage/prism/Program.h"
+
+namespace storm {
+    namespace generator {
+        
+        template<typename ValueType, typename StateType = uint32_t>
+        class PrismNextStateGenerator : public NextStateGenerator<ValueType, StateType> {
+        public:
+            typedef typename NextStateGenerator<ValueType, StateType>::StateToIdCallback StateToIdCallback;
+            
+            PrismNextStateGenerator(storm::prism::Program const& program);
+            
+            virtual std::vector<StateType> getInitialStates(StateToIdCallback stateToIdCallback) = 0;
+            virtual std::vector<Choice<ValueType>> expand(StateType const& state, StateToIdCallback stateToIdCallback) override;
+            virtual ValueType getStateReward(StateType const& state) override;
+            
+        private:
+            // The program used for the generation of next states.
+            storm::prism::Program program;
+            
+            
+        };
+        
+    }
+}
+
+#endif /* STORM_GENERATOR_PRISMNEXTSTATEGENERATOR_H_ */

src/generator/prism/VariableInformation.cpp

@@ -0,0 +1,44 @@
+#include "src/generator/prism/VariableInformation.h"
+
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidArgumentException.h"
+
+namespace storm {
+    namespace generator {
+        namespace prism {
+            
+            BooleanVariableInformation::BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset) : variable(variable), initialValue(initialValue), bitOffset(bitOffset) {
+                // Intentionally left empty.
+            }
+            
+            IntegerVariableInformation::IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t initialValue, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth) : variable(variable), initialValue(initialValue), lowerBound(lowerBound), upperBound(upperBound), bitOffset(bitOffset), bitWidth(bitWidth) {
+                // Intentionally left empty.
+            }
+            
+            VariableInformation::VariableInformation(storm::expressions::ExpressionManager const& manager) : manager(manager) {
+                // Intentionally left empty.
+            }
+            
+            uint_fast64_t VariableInformation::getBitOffset(storm::expressions::Variable const& variable) const {
+                auto const& booleanIndex = booleanVariableToIndexMap.find(variable);
+                if (booleanIndex != booleanVariableToIndexMap.end()) {
+                    return booleanVariables[booleanIndex->second].bitOffset;
+                }
+                auto const& integerIndex = integerVariableToIndexMap.find(variable);
+                if (integerIndex != integerVariableToIndexMap.end()) {
+                    return integerVariables[integerIndex->second].bitOffset;
+                }
+                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit index of unknown variable.");
+            }
+            
+            uint_fast64_t VariableInformation::getBitWidth(storm::expressions::Variable const& variable) const {
+                auto const& integerIndex = integerVariableToIndexMap.find(variable);
+                if (integerIndex != integerVariableToIndexMap.end()) {
+                    return integerVariables[integerIndex->second].bitWidth;
+                }
+                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit width of unknown variable.");
+            }
+
+        }
+    }
+}

src/generator/prism/VariableInformation.h

@@ -0,0 +1,73 @@
+#ifndef STORM_GENERATOR_PRISM_VARIABLEINFORMATION_H_
+#define STORM_GENERATOR_PRISM_VARIABLEINFORMATION_H_
+
+#include <vector>
+#include <boost/container/flat_map.hpp>
+
+#include "src/storage/expressions/Variable.h"
+
+namespace storm {
+    namespace generator {
+        namespace prism {
+            
+            // A structure storing information about the boolean variables of the program.
+            struct BooleanVariableInformation {
+                BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset);
+                
+                // The boolean variable.
+                storm::expressions::Variable variable;
+                
+                // Its initial value.
+                bool initialValue;
+                
+                // Its bit offset in the compressed state.
+                uint_fast64_t bitOffset;
+            };
+            
+            // A structure storing information about the integer variables of the program.
+            struct IntegerVariableInformation {
+                IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t initialValue, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth);
+                
+                // The integer variable.
+                storm::expressions::Variable variable;
+                
+                // Its initial value.
+                int_fast64_t initialValue;
+                
+                // The lower bound of its range.
+                int_fast64_t lowerBound;
+                
+                // The upper bound of its range.
+                int_fast64_t upperBound;
+                
+                // Its bit offset in the compressed state.
+                uint_fast64_t bitOffset;
+                
+                // Its bit width in the compressed state.
+                uint_fast64_t bitWidth;
+            };
+            
+            // A structure storing information about the used variables of the program.
+            struct VariableInformation {
+                VariableInformation(storm::expressions::ExpressionManager const& manager);
+                
+                // Provide methods to access the bit offset and width of variables in the compressed state.
+                uint_fast64_t getBitOffset(storm::expressions::Variable const& variable) const;
+                uint_fast64_t getBitWidth(storm::expressions::Variable const& variable) const;
+                
+                // The known boolean variables.
+                boost::container::flat_map<storm::expressions::Variable, uint_fast64_t> booleanVariableToIndexMap;
+                std::vector<BooleanVariableInformation> booleanVariables;
+                
+                // The known integer variables.
+                boost::container::flat_map<storm::expressions::Variable, uint_fast64_t> integerVariableToIndexMap;
+                std::vector<IntegerVariableInformation> integerVariables;
+                
+                storm::expressions::ExpressionManager const& manager;
+            };
+            
+        }
+    }
+}
+
+#endif /* STORM_GENERATOR_PRISM_VARIABLEINFORMATION_H_ */

src/storage/Distribution.cpp

@@ -14,13 +14,13 @@
 namespace storm {
     namespace storage {
         
-        template<typename ValueType>
-        Distribution<ValueType>::Distribution() {
+        template<typename ValueType, typename StateType>
+        Distribution<ValueType, StateType>::Distribution() {
             // Intentionally left empty.
         }
         
-        template<typename ValueType>
-        bool Distribution<ValueType>::equals(Distribution<ValueType> const& other, storm::utility::ConstantsComparator<ValueType> const& comparator) const {
+        template<typename ValueType, typename StateType>
+        bool Distribution<ValueType, StateType>::equals(Distribution<ValueType, StateType> const& other, storm::utility::ConstantsComparator<ValueType> const& comparator) const {
             // We need to check equality by ourselves, because we need to account for epsilon differences.
             if (this->distribution.size() != other.distribution.size()) {
                 return false;
@@ -42,8 +42,8 @@ namespace storm {
             return true;
         }
         
-        template<typename ValueType>
-        void Distribution<ValueType>::addProbability(storm::storage::sparse::state_type const& state, ValueType const& probability) {
+        template<typename ValueType, typename StateType>
+        void Distribution<ValueType, StateType>::addProbability(StateType const& state, ValueType const& probability) {
             auto it = this->distribution.find(state);
             if (it == this->distribution.end()) {
                 this->distribution.emplace_hint(it, state, probability);
@@ -52,8 +52,8 @@ namespace storm {
             }
         }
         
-        template<typename ValueType>
-        void Distribution<ValueType>::removeProbability(storm::storage::sparse::state_type const& state, ValueType const& probability, storm::utility::ConstantsComparator<ValueType> const& comparator) {
+        template<typename ValueType, typename StateType>
+        void Distribution<ValueType, StateType>::removeProbability(StateType const& state, ValueType const& probability, storm::utility::ConstantsComparator<ValueType> const& comparator) {
             auto it = this->distribution.find(state);
             STORM_LOG_ASSERT(it != this->distribution.end(), "Cannot remove probability, because the state is not in the support of the distribution.");
             it->second -= probability;
@@ -62,34 +62,34 @@ namespace storm {
             }
         }
         
-        template<typename ValueType>
-        void Distribution<ValueType>::shiftProbability(storm::storage::sparse::state_type const& fromState, storm::storage::sparse::state_type const& toState, ValueType const& probability, storm::utility::ConstantsComparator<ValueType> const& comparator) {
+        template<typename ValueType, typename StateType>
+        void Distribution<ValueType, StateType>::shiftProbability(StateType const& fromState, StateType const& toState, ValueType const& probability, storm::utility::ConstantsComparator<ValueType> const& comparator) {
             removeProbability(fromState, probability, comparator);
             addProbability(toState, probability);
         }
         
-        template<typename ValueType>
-        typename Distribution<ValueType>::iterator Distribution<ValueType>::begin() {
+        template<typename ValueType, typename StateType>
+        typename Distribution<ValueType, StateType>::iterator Distribution<ValueType, StateType>::begin() {
             return this->distribution.begin();
         }
 
-        template<typename ValueType>
-        typename Distribution<ValueType>::const_iterator Distribution<ValueType>::begin() const {
+        template<typename ValueType, typename StateType>
+        typename Distribution<ValueType, StateType>::const_iterator Distribution<ValueType, StateType>::begin() const {
             return this->distribution.begin();
         }
         
-        template<typename ValueType>
-        typename Distribution<ValueType>::iterator Distribution<ValueType>::end() {
+        template<typename ValueType, typename StateType>
+        typename Distribution<ValueType, StateType>::iterator Distribution<ValueType, StateType>::end() {
             return this->distribution.end();
         }
         
-        template<typename ValueType>
-        typename Distribution<ValueType>::const_iterator Distribution<ValueType>::end() const {
+        template<typename ValueType, typename StateType>
+        typename Distribution<ValueType, StateType>::const_iterator Distribution<ValueType, StateType>::end() const {
             return this->distribution.end();
         }
         
-        template<typename ValueType>
-        void Distribution<ValueType>::scale(storm::storage::sparse::state_type const& state) {
+        template<typename ValueType, typename StateType>
+        void Distribution<ValueType, StateType>::scale(StateType const& state) {
             auto probabilityIterator = this->distribution.find(state);
             if (probabilityIterator != this->distribution.end()) {
                 ValueType scaleValue = storm::utility::one<ValueType>() / probabilityIterator->second;
@@ -101,13 +101,13 @@ namespace storm {
             }
         }
                 
-        template<typename ValueType>
-        std::size_t Distribution<ValueType>::size() const {
+        template<typename ValueType, typename StateType>
+        std::size_t Distribution<ValueType, StateType>::size() const {
             return this->distribution.size();
         }
         
-        template<typename ValueType>
-        std::ostream& operator<<(std::ostream& out, Distribution<ValueType> const& distribution) {
+        template<typename ValueType, typename StateType>
+        std::ostream& operator<<(std::ostream& out, Distribution<ValueType, StateType> const& distribution) {
             out << "{";
             for (auto const& entry : distribution) {
                 out << "[" << entry.second << ": " << entry.first << "], ";
@@ -117,8 +117,8 @@ namespace storm {
             return out;
         }
         
-        template<typename ValueType>
-        bool Distribution<ValueType>::less(Distribution<ValueType> const& other, storm::utility::ConstantsComparator<ValueType> const& comparator) const {
+        template<typename ValueType, typename StateType>
+        bool Distribution<ValueType, StateType>::less(Distribution<ValueType, StateType> const& other, storm::utility::ConstantsComparator<ValueType> const& comparator) const {
             if (this->size() != other.size()) {
                 return this->size() < other.size();
             }

src/storage/Distribution.h

@@ -17,10 +17,10 @@ namespace storm {
     
     namespace storage {
         
-        template<typename ValueType>
+        template<typename ValueType, typename StateType=storm::storage::sparse::state_type>
         class Distribution {
         public:
-            typedef boost::container::flat_map<storm::storage::sparse::state_type, ValueType> container_type;
+            typedef boost::container::flat_map<StateType, ValueType> container_type;
             typedef typename container_type::iterator iterator;
             typedef typename container_type::const_iterator const_iterator;
             
@@ -51,7 +51,7 @@ namespace storm {
              * @param state The state to which to assign the probability.
              * @param probability The probability to assign.
              */
-            void addProbability(storm::storage::sparse::state_type const& state, ValueType const& probability);
+            void addProbability(StateType const& state, ValueType const& probability);
             
             /*!
              * Removes the given probability mass of going to the given state.
@@ -61,7 +61,7 @@ namespace storm {
              * @param comparator A comparator that is used to determine if the remaining probability is zero. If so, the
              * entry is removed.
              */
-            void removeProbability(storm::storage::sparse::state_type const& state, ValueType const& probability, storm::utility::ConstantsComparator<ValueType> const& comparator = storm::utility::ConstantsComparator<ValueType>());
+            void removeProbability(StateType const& state, ValueType const& probability, storm::utility::ConstantsComparator<ValueType> const& comparator = storm::utility::ConstantsComparator<ValueType>());
             
             /*!
              * Removes the probability mass from one state and adds it to another.
@@ -72,7 +72,7 @@ namespace storm {
              * @param comparator A comparator that is used to determine if the remaining probability is zero. If so, the
              * entry is removed.
              */
-            void shiftProbability(storm::storage::sparse::state_type const& fromState, storm::storage::sparse::state_type const& toState, ValueType const& probability, storm::utility::ConstantsComparator<ValueType> const& comparator = storm::utility::ConstantsComparator<ValueType>());
+            void shiftProbability(StateType const& fromState, StateType const& toState, ValueType const& probability, storm::utility::ConstantsComparator<ValueType> const& comparator = storm::utility::ConstantsComparator<ValueType>());
             
             /*!
              * Retrieves an iterator to the elements in this distribution.
@@ -109,7 +109,7 @@ namespace storm {
              *
              * @param state The state whose associated probability is used to scale the distribution.
              */
-            void scale(storm::storage::sparse::state_type const& state);
+            void scale(StateType const& state);
             
             /*!
              * Retrieves the size of the distribution, i.e. the size of the support set.