more work on JANI next-state generator

Former-commit-id: d94ab2b81e

src/generator/JaniNextStateGenerator.cpp

@@ -1,89 +1,172 @@
-//#include "src/generator/JaniNextStateGenerator.h"
-//
-//#include "src/models/sparse/StateLabeling.h"
-//
-//#include "src/storage/expressions/SimpleValuation.h"
-//
-//#include "src/utility/constants.h"
-//#include "src/utility/macros.h"
-//#include "src/exceptions/InvalidSettingsException.h"
-//#include "src/exceptions/WrongFormatException.h"
-//
-//namespace storm {
-//    namespace generator {
-//     
-//        template<typename ValueType, typename StateType>
-//        JaniNextStateGenerator<ValueType, StateType>::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options) : NextStateGenerator<ValueType, StateType>(options), model(model.substituteConstants()), variableInformation(this->model), evaluator(this->model.getManager()), state(nullptr), comparator() {
-//            STORM_LOG_THROW(!this->model.hasDefaultComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions.");
-//            STORM_LOG_THROW(!this->options.isBuildAllRewardModelsSet() && this->options.getRewardModelNames().empty(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support building reward models.");
-//            
-//            // If there are terminal states we need to handle, we now need to translate all labels to expressions.
-//            if (this->options.hasTerminalStates()) {
-//                for (auto const& expressionOrLabelAndBool : this->options.getTerminalStates()) {
-//                    if (expressionOrLabelAndBool.first.isExpression()) {
-//                        terminalStates.push_back(std::make_pair(expressionOrLabelAndBool.first.getExpression(), expressionOrLabelAndBool.second));
-//                    } else {
-//                        STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Cannot make label terminal for JANI models.");
-//                    }
-//                }
-//            }
-//        }
-//        
-//        template<typename ValueType, typename StateType>
-//        uint64_t JaniNextStateGenerator<ValueType, StateType>::getStateSize() const {
-//            return variableInformation.getTotalBitOffset(true);
-//        }
-//        
-//        template<typename ValueType, typename StateType>
-//        ModelType JaniNextStateGenerator<ValueType, StateType>::getModelType() const {
-//            switch (model.getModelType()) {
-//                case storm::jani::ModelType::DTMC: return ModelType::DTMC;
-//                case storm::jani::ModelType::CTMC: return ModelType::CTMC;
-//                case storm::jani::ModelType::MDP: return ModelType::MDP;
-//                case storm::jani::ModelType::MA: return ModelType::MA;
-//                default:
-//                    STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Invalid model type.");
-//            }
-//        }
-//        
-//        template<typename ValueType, typename StateType>
-//        bool JaniNextStateGenerator<ValueType, StateType>::isDeterministicModel() const {
-//            return model.isDeterministicModel();
-//        }
-//
-//        template<typename ValueType, typename StateType>
-//        std::vector<StateType> JaniNextStateGenerator<ValueType, StateType>::getInitialStates(StateToIdCallback const& stateToIdCallback) {
-//            // FIXME: This only works for models with exactly one initial state. We should make this more general.
-//            CompressedState initialState(variableInformation.getTotalBitOffset());
-//            
-//            // We need to initialize the values of the variables to their initial value.
-//            for (auto const& booleanVariable : variableInformation.booleanVariables) {
-//                initialState.set(booleanVariable.bitOffset, booleanVariable.initialValue);
-//            }
-//            for (auto const& integerVariable : variableInformation.integerVariables) {
-//                initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast<uint_fast64_t>(integerVariable.initialValue - integerVariable.lowerBound));
-//            }
-//            
-//            // Register initial state and return it.
-//            StateType id = stateToIdCallback(initialState);
-//            return {id};
-//        }
-//        
-//        template<typename ValueType, typename StateType>
-//        void JaniNextStateGenerator<ValueType, StateType>::load(CompressedState const& state) {
-//            // Since almost all subsequent operations are based on the evaluator, we load the state into it now.
-//            unpackStateIntoEvaluator(state, variableInformation, evaluator);
-//            
-//            // Also, we need to store a pointer to the state itself, because we need to be able to access it when expanding it.
-//            this->state = &state;
-//        }
-//        
-//        template<typename ValueType, typename StateType>
-//        bool JaniNextStateGenerator<ValueType, StateType>::satisfies(storm::expressions::Expression const& expression) const {
-//            if (expression.isTrue()) {
-//                return true;
-//            }
-//            return evaluator.asBool(expression);
-//        }
-//    }
-//}
+#include "src/generator/JaniNextStateGenerator.h"
+
+#include "src/models/sparse/StateLabeling.h"
+
+#include "src/storage/expressions/SimpleValuation.h"
+
+#include "src/solver/SmtSolver.h"
+
+#include "src/utility/constants.h"
+#include "src/utility/macros.h"
+#include "src/utility/solver.h"
+#include "src/exceptions/InvalidSettingsException.h"
+#include "src/exceptions/WrongFormatException.h"
+
+namespace storm {
+    namespace generator {
+     
+        template<typename ValueType, typename StateType>
+        JaniNextStateGenerator<ValueType, StateType>::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options) : JaniNextStateGenerator(model.substituteConstants(), options, false) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType, typename StateType>
+        JaniNextStateGenerator<ValueType, StateType>::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator<ValueType, StateType>(model.getExpressionManager(), VariableInformation(model), options), model(model) {
+            STORM_LOG_THROW(!this->model.hasDefaultComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions.");
+            STORM_LOG_THROW(!this->options.isBuildAllRewardModelsSet() && this->options.getRewardModelNames().empty(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support building reward models.");
+            
+            // If there are terminal states we need to handle, we now need to translate all labels to expressions.
+            if (this->options.hasTerminalStates()) {
+                for (auto const& expressionOrLabelAndBool : this->options.getTerminalStates()) {
+                    if (expressionOrLabelAndBool.first.isExpression()) {
+                        this->terminalStates.push_back(std::make_pair(expressionOrLabelAndBool.first.getExpression(), expressionOrLabelAndBool.second));
+                    } else {
+                        STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Cannot make label terminal for JANI models.");
+                    }
+                }
+            }
+        }
+        
+        template<typename ValueType, typename StateType>
+        ModelType JaniNextStateGenerator<ValueType, StateType>::getModelType() const {
+            switch (model.getModelType()) {
+                case storm::jani::ModelType::DTMC: return ModelType::DTMC;
+                case storm::jani::ModelType::CTMC: return ModelType::CTMC;
+                case storm::jani::ModelType::MDP: return ModelType::MDP;
+                case storm::jani::ModelType::MA: return ModelType::MA;
+                default:
+                    STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Invalid model type.");
+            }
+        }
+        
+        template<typename ValueType, typename StateType>
+        bool JaniNextStateGenerator<ValueType, StateType>::isDeterministicModel() const {
+            return model.isDeterministicModel();
+        }
+
+        template<typename ValueType, typename StateType>
+        std::vector<StateType> JaniNextStateGenerator<ValueType, StateType>::getInitialStates(StateToIdCallback const& stateToIdCallback) {
+            // Prepare an SMT solver to enumerate all initial states.
+            storm::utility::solver::SmtSolverFactory factory;
+            std::unique_ptr<storm::solver::SmtSolver> solver = factory.create(model.getExpressionManager());
+            
+            std::vector<storm::expressions::Expression> rangeExpressions = model.getAllRangeExpressions();
+            for (auto const& expression : rangeExpressions) {
+                solver->add(expression);
+            }
+            solver->add(model.getInitialStatesExpression(true));
+            
+            // Proceed ss long as the solver can still enumerate initial states.
+            std::vector<StateType> initialStateIndices;
+            while (solver->check() == storm::solver::SmtSolver::CheckResult::Sat) {
+                // Create fresh state.
+                CompressedState initialState(this->variableInformation.getTotalBitOffset());
+                
+                // Read variable assignment from the solution of the solver. Also, create an expression we can use to
+                // prevent the variable assignment from being enumerated again.
+                storm::expressions::Expression blockingExpression;
+                std::shared_ptr<storm::solver::SmtSolver::ModelReference> model = solver->getModel();
+                for (auto const& booleanVariable : this->variableInformation.booleanVariables) {
+                    bool variableValue = model->getBooleanValue(booleanVariable.variable);
+                    storm::expressions::Expression localBlockingExpression = variableValue ? !booleanVariable.variable : booleanVariable.variable;
+                    blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression;
+                    initialState.set(booleanVariable.bitOffset, variableValue);
+                }
+                for (auto const& integerVariable : this->variableInformation.integerVariables) {
+                    int_fast64_t variableValue = model->getIntegerValue(integerVariable.variable);
+                    storm::expressions::Expression localBlockingExpression = integerVariable.variable != model->getManager().integer(variableValue);
+                    blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression;
+                    initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast<uint_fast64_t>(variableValue - integerVariable.lowerBound));
+                }
+                
+                // Register initial state and return it.
+                StateType id = stateToIdCallback(initialState);
+                initialStateIndices.push_back(id);
+                
+                // Block the current initial state to search for the next one.
+                solver->add(blockingExpression);
+            }
+            
+            return initialStateIndices;
+        }
+
+        template<typename ValueType, typename StateType>
+        CompressedState JaniNextStateGenerator<ValueType, StateType>::applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& destination) {
+            CompressedState newState(state);
+            
+            auto assignmentIt = destination.getAssignments().begin();
+            auto assignmentIte = destination.getAssignments().end();
+            
+            // Iterate over all boolean assignments and carry them out.
+            auto boolIt = this->variableInformation.booleanVariables.begin();
+            for (; assignmentIt != assignmentIte && assignmentIt->getAssignedExpression().hasBooleanType(); ++assignmentIt) {
+                while (assignmentIt->getExpressionVariable() != boolIt->variable) {
+                    ++boolIt;
+                }
+                newState.set(boolIt->bitOffset, this->evaluator.asBool(assignmentIt->getExpressionVariable()));
+            }
+            
+            // Iterate over all integer assignments and carry them out.
+            auto integerIt = this->variableInformation.integerVariables.begin();
+            for (; assignmentIt != assignmentIte && assignmentIt->getAssignedExpression().hasIntegerType(); ++assignmentIt) {
+                while (assignmentIt->getExpressionVariable() != integerIt->variable) {
+                    ++integerIt;
+                }
+                int_fast64_t assignedValue = this->evaluator.asInt(assignmentIt->getAssignedExpression());
+                STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << assignmentIt->getExpressionVariable().getName() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'.");
+                newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound);
+                STORM_LOG_ASSERT(static_cast<int_fast64_t>(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth)) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ").");
+            }
+            
+            // Check that we processed all assignments.
+            STORM_LOG_ASSERT(assignmentIt == assignmentIte, "Not all assignments were consumed.");
+            
+            return newState;
+        }
+        
+        template<typename ValueType, typename StateType>
+        StateBehavior<ValueType, StateType> JaniNextStateGenerator<ValueType, StateType>::expand(StateToIdCallback const& stateToIdCallback) {
+            
+        }
+        
+        template<typename ValueType, typename StateType>
+        std::vector<Choice<ValueType>> JaniNextStateGenerator<ValueType, StateType>::getSilentActionChoices(CompressedState const& state, StateToIdCallback stateToIdCallback) {
+            
+        }
+        
+        template<typename ValueType, typename StateType>
+        std::vector<Choice<ValueType>> JaniNextStateGenerator<ValueType, StateType>::getNonsilentActionChoices(CompressedState const& state, StateToIdCallback stateToIdCallback) {
+            
+        }
+        
+        template<typename ValueType, typename StateType>
+        std::size_t JaniNextStateGenerator<ValueType, StateType>::getNumberOfRewardModels() const {
+            return 0;
+        }
+        
+        template<typename ValueType, typename StateType>
+        RewardModelInformation JaniNextStateGenerator<ValueType, StateType>::getRewardModelInformation(uint64_t const& index) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Cannot retrieve reward model information.");
+            return RewardModelInformation("", false, false, false);
+        }
+        
+        template<typename ValueType, typename StateType>
+        storm::models::sparse::StateLabeling JaniNextStateGenerator<ValueType, StateType>::label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices) {
+            return NextStateGenerator<ValueType, StateType>::label(states, initialStateIndices, {});
+        }
+
+        template class JaniNextStateGenerator<double>;
+        template class JaniNextStateGenerator<storm::RationalFunction>;
+        
+    }
+}

src/generator/JaniNextStateGenerator.h

@@ -1,68 +1,66 @@
-//#pragma once
-//
-//#include "src/generator/NextStateGenerator.h"
-//#include "src/generator/VariableInformation.h"
-//
-//#include "src/storage/jani/Model.h"
-//#include "src/storage/expressions/ExpressionEvaluator.h"
-//
-//#include "src/utility/ConstantsComparator.h"
-//
-//namespace storm {
-//    namespace generator {
-//        
-//        template<typename ValueType, typename StateType = uint32_t>
-//        class JaniNextStateGenerator : public NextStateGenerator<ValueType, StateType> {
-//        public:
-//            typedef typename NextStateGenerator<ValueType, StateType>::StateToIdCallback StateToIdCallback;
-//            
-//            JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options = NextStateGeneratorOptions());
-//            
-//            virtual uint64_t getStateSize() const override;
-//            virtual ModelType getModelType() const override;
-//            virtual bool isDeterministicModel() const override;
-//            virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) override;
-//            
-//            virtual void load(CompressedState const& state) override;
-//            virtual StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback) override;
-//            virtual bool satisfies(storm::expressions::Expression const& expression) const override;
-//            
-//            virtual std::size_t getNumberOfRewardModels() const override;
-//            virtual RewardModelInformation getRewardModelInformation(uint64_t const& index) const override;
-//            
-//            virtual storm::expressions::SimpleValuation toValuation(CompressedState const& state) const override;
-//            
-//            virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}) override;
-//            
-//        private:
-//            /*!
-//             * Applies an update to the state currently loaded into the evaluator and applies the resulting values to
-//             * the given compressed state.
-//             * @params state The state to which to apply the new values.
-//             * @params update The update to apply.
-//             * @return The resulting state.
-//             */
-//            CompressedState applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& update);
-//            
-//            /*!
-//             * Retrieves all choices labeled with the silent action possible from the given state.
-//             *
-//             * @param state The state for which to retrieve the silent choices.
-//             * @return The silent action choices of the state.
-//             */
-//            std::vector<Choice<ValueType>> getSilentActionChoices(CompressedState const& state, StateToIdCallback stateToIdCallback);
-//            
-//            /*!
-//             * Retrieves all choices labeled with some non-silent action possible from the given state.
-//             *
-//             * @param state The state for which to retrieve the non-silent choices.
-//             * @return The non-silent action choices of the state.
-//             */
-//            std::vector<Choice<ValueType>> getNonsilentActionChoices(CompressedState const& state, StateToIdCallback stateToIdCallback);
-//            
-//            // The model used for the generation of next states.
-//            storm::jani::Model model;
-//        };
-//        
-//    }
-//}
+#pragma once
+
+#include "src/generator/NextStateGenerator.h"
+
+#include "src/storage/jani/Model.h"
+
+namespace storm {
+    namespace generator {
+        
+        template<typename ValueType, typename StateType = uint32_t>
+        class JaniNextStateGenerator : public NextStateGenerator<ValueType, StateType> {
+        public:
+            typedef typename NextStateGenerator<ValueType, StateType>::StateToIdCallback StateToIdCallback;
+            
+            JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options = NextStateGeneratorOptions());
+            
+            virtual ModelType getModelType() const override;
+            virtual bool isDeterministicModel() const override;
+            virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) override;
+            
+            virtual StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback) override;
+            
+            virtual std::size_t getNumberOfRewardModels() const override;
+            virtual RewardModelInformation getRewardModelInformation(uint64_t const& index) const override;
+                        
+            virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}) override;
+            
+        private:
+            /*!
+             * A delegate constructor that is used to preprocess the model before the constructor of the superclass is
+             * being called. The last argument is only present to distinguish the signature of this constructor from the
+             * public one.
+             */
+            JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool flag);
+            
+            /*!
+             * Applies an update to the state currently loaded into the evaluator and applies the resulting values to
+             * the given compressed state.
+             * @params state The state to which to apply the new values.
+             * @params update The update to apply.
+             * @return The resulting state.
+             */
+            CompressedState applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& update);
+            
+            /*!
+             * Retrieves all choices labeled with the silent action possible from the given state.
+             *
+             * @param state The state for which to retrieve the silent choices.
+             * @return The silent action choices of the state.
+             */
+            std::vector<Choice<ValueType>> getSilentActionChoices(CompressedState const& state, StateToIdCallback stateToIdCallback);
+            
+            /*!
+             * Retrieves all choices labeled with some non-silent action possible from the given state.
+             *
+             * @param state The state for which to retrieve the non-silent choices.
+             * @return The non-silent action choices of the state.
+             */
+            std::vector<Choice<ValueType>> getNonsilentActionChoices(CompressedState const& state, StateToIdCallback stateToIdCallback);
+            
+            // The model used for the generation of next states.
+            storm::jani::Model model;
+        };
+        
+    }
+}

src/generator/PrismNextStateGenerator.cpp

@@ -6,6 +6,8 @@
 
 #include "src/storage/expressions/SimpleValuation.h"
 
+#include "src/solver/SmtSolver.h"
+
 #include "src/utility/constants.h"
 #include "src/utility/macros.h"
 #include "src/exceptions/InvalidArgumentException.h"
@@ -20,7 +22,7 @@ namespace storm {
         }
         
         template<typename ValueType, typename StateType>
-        PrismNextStateGenerator<ValueType, StateType>::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator<ValueType, StateType>(program.getManager(), VariableInformation(program), options), program(program.substituteConstants()), rewardModels() {
+        PrismNextStateGenerator<ValueType, StateType>::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator<ValueType, StateType>(program.getManager(), VariableInformation(program), options), program(program), rewardModels() {
             STORM_LOG_THROW(!this->program.specifiesSystemComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions.");
             
             if (this->options.isBuildAllRewardModelsSet()) {
@@ -82,20 +84,48 @@ namespace storm {
         
         template<typename ValueType, typename StateType>
         std::vector<StateType> PrismNextStateGenerator<ValueType, StateType>::getInitialStates(StateToIdCallback const& stateToIdCallback) {
-            // FIXME: This only works for models with exactly one initial state. We should make this more general.
+            // Prepare an SMT solver to enumerate all initial states.
+            storm::utility::solver::SmtSolverFactory factory;
+            std::unique_ptr<storm::solver::SmtSolver> solver = factory.create(program.getManager());
+            
+            std::vector<storm::expressions::Expression> rangeExpressions = program.getAllRangeExpressions();
+            for (auto const& expression : rangeExpressions) {
+                solver->add(expression);
+            }
+            solver->add(program.getInitialConstruct().getInitialStatesExpression());
+            
+            // Proceed ss long as the solver can still enumerate initial states.
+            std::vector<StateType> initialStateIndices;
+            while (solver->check() == storm::solver::SmtSolver::CheckResult::Sat) {
+                // Create fresh state.
                 CompressedState initialState(this->variableInformation.getTotalBitOffset());
                 
-            // We need to initialize the values of the variables to their initial value.
+                // Read variable assignment from the solution of the solver. Also, create an expression we can use to
+                // prevent the variable assignment from being enumerated again.
+                storm::expressions::Expression blockingExpression;
+                std::shared_ptr<storm::solver::SmtSolver::ModelReference> model = solver->getModel();
                 for (auto const& booleanVariable : this->variableInformation.booleanVariables) {
-                initialState.set(booleanVariable.bitOffset, booleanVariable.initialValue);
+                    bool variableValue = model->getBooleanValue(booleanVariable.variable);
+                    storm::expressions::Expression localBlockingExpression = variableValue ? !booleanVariable.variable : booleanVariable.variable;
+                    blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression;
+                    initialState.set(booleanVariable.bitOffset, variableValue);
                 }
                 for (auto const& integerVariable : this->variableInformation.integerVariables) {
-                initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast<uint_fast64_t>(integerVariable.initialValue - integerVariable.lowerBound));
+                    int_fast64_t variableValue = model->getIntegerValue(integerVariable.variable);
+                    storm::expressions::Expression localBlockingExpression = integerVariable.variable != model->getManager().integer(variableValue);
+                    blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression;
+                    initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast<uint_fast64_t>(variableValue - integerVariable.lowerBound));
                 }
                 
                 // Register initial state and return it.
                 StateType id = stateToIdCallback(initialState);
-            return {id};
+                initialStateIndices.push_back(id);
+                
+                // Block the current initial state to search for the next one.
+                solver->add(blockingExpression);
+            }
+            
+            return initialStateIndices;
         }
         
         template<typename ValueType, typename StateType>
@@ -202,6 +232,11 @@ namespace storm {
         CompressedState PrismNextStateGenerator<ValueType, StateType>::applyUpdate(CompressedState const& state, storm::prism::Update const& update) {
             CompressedState newState(state);
             
+            // NOTE: the following process assumes that the assignments of the update are ordered in such a way that the
+            // assignments to boolean variables precede the assignments to all integer variables and that within the
+            // types, the assignments to variables are ordered (in ascending order) by the expression variables.
+            // This is guaranteed for PRISM models, by sorting the assignments as soon as an update is created.
+            
             auto assignmentIt = update.getAssignments().begin();
             auto assignmentIte = update.getAssignments().end();
             

src/generator/VariableInformation.cpp

@@ -1,77 +1,92 @@
 #include "src/generator/VariableInformation.h"
 
+#include "src/storage/prism/Program.h"
+#include "src/storage/jani/Model.h"
+
 #include "src/utility/macros.h"
 #include "src/exceptions/InvalidArgumentException.h"
 
 namespace storm {
     namespace generator {
         
-        BooleanVariableInformation::BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset) : variable(variable), initialValue(initialValue), bitOffset(bitOffset) {
+        BooleanVariableInformation::BooleanVariableInformation(storm::expressions::Variable const& variable, uint_fast64_t bitOffset) : variable(variable), 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) {
+        IntegerVariableInformation::IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth) : variable(variable), lowerBound(lowerBound), upperBound(upperBound), bitOffset(bitOffset), bitWidth(bitWidth) {
             // Intentionally left empty.
         }
         
         VariableInformation::VariableInformation(storm::prism::Program const& program) : totalBitOffset(0) {
             for (auto const& booleanVariable : program.getGlobalBooleanVariables()) {
-                booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), booleanVariable.getInitialValueExpression().evaluateAsBool(), totalBitOffset);
+                booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), totalBitOffset);
                 ++totalBitOffset;
-                booleanVariableToIndexMap[booleanVariable.getExpressionVariable()] = booleanVariables.size() - 1;
             }
             for (auto const& integerVariable : program.getGlobalIntegerVariables()) {
                 int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt();
                 int_fast64_t upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt();
                 uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));
-                integerVariables.emplace_back(integerVariable.getExpressionVariable(), integerVariable.getInitialValueExpression().evaluateAsInt(), lowerBound, upperBound, totalBitOffset, bitwidth);
+                integerVariables.emplace_back(integerVariable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth);
                 totalBitOffset += bitwidth;
-                integerVariableToIndexMap[integerVariable.getExpressionVariable()] = integerVariables.size() - 1;
             }
             for (auto const& module : program.getModules()) {
                 for (auto const& booleanVariable : module.getBooleanVariables()) {
-                    booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), booleanVariable.getInitialValueExpression().evaluateAsBool(), totalBitOffset);
+                    booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), totalBitOffset);
                     ++totalBitOffset;
-                    booleanVariableToIndexMap[booleanVariable.getExpressionVariable()] = booleanVariables.size() - 1;
                 }
                 for (auto const& integerVariable : module.getIntegerVariables()) {
                     int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt();
                     int_fast64_t upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt();
                     uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));
-                    integerVariables.emplace_back(integerVariable.getExpressionVariable(), integerVariable.getInitialValueExpression().evaluateAsInt(), lowerBound, upperBound, totalBitOffset, bitwidth);
+                    integerVariables.emplace_back(integerVariable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth);
                     totalBitOffset += bitwidth;
-                    integerVariableToIndexMap[integerVariable.getExpressionVariable()] = integerVariables.size() - 1;
                 }
             }
+
+            sortVariables();
         }
         
-        uint_fast64_t VariableInformation::getTotalBitOffset(bool roundTo64Bit) const {
-            uint_fast64_t result = totalBitOffset;
-            if (roundTo64Bit) {
-                result = ((result >> 6) + 1) << 6;
+        VariableInformation::VariableInformation(storm::jani::Model const& model) {
+            for (auto const& variable : model.getGlobalVariables().getBooleanVariables()) {
+                booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset);
+                ++totalBitOffset;
             }
-            return result;
+            for (auto const& variable : model.getGlobalVariables().getBoundedIntegerVariables()) {
+                int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt();
+                int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt();
+                uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));
+                integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth);
+                totalBitOffset += bitwidth;
             }
-        
-        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;
+            for (auto const& automaton : model.getAutomata()) {
+                for (auto const& variable : automaton.getVariables().getBooleanVariables()) {
+                    booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset);
+                    ++totalBitOffset;
                 }
-            auto const& integerIndex = integerVariableToIndexMap.find(variable);
-            if (integerIndex != integerVariableToIndexMap.end()) {
-                return integerVariables[integerIndex->second].bitOffset;
+                for (auto const& variable : automaton.getVariables().getBoundedIntegerVariables()) {
+                    int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt();
+                    int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt();
+                    uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));
+                    integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth);
+                    totalBitOffset += bitwidth;
                 }
-            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;
+            sortVariables();
         }
-            STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit width of unknown variable.");
+        
+        uint_fast64_t VariableInformation::getTotalBitOffset(bool roundTo64Bit) const {
+            uint_fast64_t result = totalBitOffset;
+            if (roundTo64Bit) {
+                result = ((result >> 6) + 1) << 6;
+            }
+            return result;
         }
         
+        void VariableInformation::sortVariables() {
+            // Sort the variables so we can make some assumptions when iterating over them (in the next-state generators).
+            std::sort(booleanVariables.begin(), booleanVariables.end(), [] (BooleanVariableInformation const& a, BooleanVariableInformation const& b) { return a.variable < b.variable; } );
+            std::sort(integerVariables.begin(), integerVariables.end(), [] (IntegerVariableInformation const& a, IntegerVariableInformation const& b) { return a.variable < b.variable; });
+        }
     }
 }

src/generator/VariableInformation.h

@@ -5,35 +5,36 @@
 #include <boost/container/flat_map.hpp>
 
 #include "src/storage/expressions/Variable.h"
-#include "src/storage/prism/Program.h"
 
 namespace storm {
+    namespace prism {
+        class Program;
+    }
+    
+    namespace jani {
+        class Model;
+    }
+    
     namespace generator {
         
         // 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);
+            BooleanVariableInformation(storm::expressions::Variable const& variable, 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);
+            IntegerVariableInformation(storm::expressions::Variable const& variable, 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;
             
@@ -49,24 +50,26 @@ namespace storm {
         
         // A structure storing information about the used variables of the program.
         struct VariableInformation {
-            VariableInformation() = default;
             VariableInformation(storm::prism::Program const& program);
-            uint_fast64_t getTotalBitOffset(bool roundTo64Bit = false) const;
+            VariableInformation(storm::jani::Model const& model);
             
-            // 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;
+            VariableInformation() = default;
+            uint_fast64_t getTotalBitOffset(bool roundTo64Bit = false) const;
             
             // The total bit offset over all variables.
             uint_fast64_t totalBitOffset;
             
             // 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;
+            
+        private:
+            /*!
+             * Sorts the variables to establish a known ordering.
+             */
+            void sortVariables();
         };
         
     }

src/storage/jani/Automaton.cpp

@@ -199,5 +199,12 @@ namespace storm {
             return actionIndices.find(actionIndex) != actionIndices.end();
         }
         
+        std::vector<storm::expressions::Expression> Automaton::getAllRangeExpressions() const {
+            std::vector<storm::expressions::Expression> result;
+            for (auto const& variable : this->getVariables().getBoundedIntegerVariables()) {
+                result.push_back(variable.getRangeExpression());
+            }
+            return result;
+        }
     }
 }

src/storage/jani/Automaton.h

@@ -230,6 +230,11 @@ namespace storm {
              */
             bool hasEdgeLabeledWithActionIndex(uint64_t actionIndex) const;
             
+            /*!
+             * Retrieves a list of expressions that characterize the legal values of the variables in this automaton.
+             */
+            std::vector<storm::expressions::Expression> getAllRangeExpressions() const;
+            
         private:
             /// The name of the automaton.
             std::string name;

src/storage/jani/BoundedIntegerVariable.cpp

@@ -23,6 +23,10 @@ namespace storm {
             this->upperBound = expression;
         }
         
+        storm::expressions::Expression BoundedIntegerVariable::getRangeExpression() const {
+            return this->getLowerBound() <= this->getExpressionVariable() && this->getExpressionVariable() <= this->getUpperBound();
+        }
+
         bool BoundedIntegerVariable::isBoundedIntegerVariable() const {
             return true;
         }

src/storage/jani/BoundedIntegerVariable.h

@@ -33,6 +33,11 @@ namespace storm {
              */
             void setUpperBound(storm::expressions::Expression const& expression);
 
+            /*!
+             * Retrieves an expression characterizing the legal range of the bounded integer variable.
+             */
+            storm::expressions::Expression getRangeExpression() const;
+            
             virtual bool isBoundedIntegerVariable() const override;
 
         private:

src/storage/jani/CompositionInformationVisitor.cpp

@@ -0,0 +1,92 @@
+#include "src/storage/jani/CompositionInformationVisitor.h"
+
+#include "src/storage/jani/Model.h"
+#include "src/storage/jani/Compositions.h"
+
+namespace storm {
+    namespace jani {
+        
+        CompositionInformation::CompositionInformation(std::map<std::string, uint64_t> const& automatonNameToMultiplicity, std::set<std::string> const& nonsilentActions, bool containsRenameComposition, bool containsRestrictedParallelComposition) : automatonNameToMultiplicity(automatonNameToMultiplicity), nonsilentActions(nonsilentActions), renameComposition(containsRenameComposition), restrictedParallelComposition(containsRestrictedParallelComposition) {
+            // Intentionally left empty.
+        }
+        
+        void CompositionInformation::increaseAutomatonMultiplicity(std::string const& automatonName, uint64_t count) {
+            automatonNameToMultiplicity[automatonName] += count;
+        }
+        
+        void CompositionInformation::addNonsilentAction(std::string const& actionName) {
+            // FIXME
+        }
+        
+        std::set<std::string> const& CompositionInformation::getNonsilentActions() const {
+            // FIXME
+        }
+        
+        void CompositionInformation::renameNonsilentActions(std::map<std::string, std::string> const& renaming) {
+            // FIXME
+        }
+        
+        void CompositionInformation::setContainsRenameComposition() {
+            renameComposition = true;
+        }
+        
+        bool CompositionInformation::containsRenameComposition() const {
+            return renameComposition;
+        }
+        
+        void CompositionInformation::setContainsRestrictedParallelComposition() {
+            restrictedParallelComposition = true;
+        }
+        
+        bool CompositionInformation::containsRestrictedParallelComposition() const {
+            return restrictedParallelComposition;
+        }
+        
+        std::map<std::string, uint64_t> CompositionInformation::joinMultiplicityMaps(std::map<std::string, uint64_t> const& first, std::map<std::string, uint64_t> const& second) {
+            std::map<std::string, uint64_t> result = first;
+            for (auto const& element : second) {
+                result[element.first] += element.second;
+            }
+            return result;
+        }
+        
+        std::map<std::string, uint64_t> const& CompositionInformation::getAutomatonToMultiplicityMap() const {
+            return automatonNameToMultiplicity;
+        }
+        
+        CompositionInformation CompositionInformationVisitor::getInformation(Composition const& composition, Model const& model) {
+            return boost::any_cast<CompositionInformation>(composition.accept(*this, model));
+        }
+        
+        boost::any CompositionInformationVisitor::visit(AutomatonComposition const& composition, boost::any const& data) {
+            CompositionInformation result;
+            result.increaseAutomatonMultiplicity(composition.getAutomatonName());
+            return result;
+        }
+        
+        boost::any CompositionInformationVisitor::visit(RenameComposition const& composition, boost::any const& data) {
+            CompositionInformation subresult = boost::any_cast<CompositionInformation>(composition.getSubcomposition().accept(*this, data));
+            subresult.setContainsRenameComposition();
+            return subresult;
+        }
+        
+        boost::any CompositionInformationVisitor::visit(ParallelComposition const& composition, boost::any const& data) {
+            Model const& model = boost::any_cast<Model const&>(data);
+            CompositionInformation left = boost::any_cast<CompositionInformation>(composition.getLeftSubcomposition().accept(*this, data));
+            CompositionInformation right = boost::any_cast<CompositionInformation>(composition.getRightSubcomposition().accept(*this, data));
+
+            // Join the information from both sides.
+            bool containsRenameComposition = left.containsRenameComposition() || right.containsRenameComposition();
+            bool containsRestrictedParallelComposition = left.containsRestrictedParallelComposition() || right.containsRestrictedParallelComposition();
+            std::map<std::string, uint64_t> joinedAutomatonToMultiplicity = CompositionInformation::joinMultiplicityMaps(left.getAutomatonToMultiplicityMap(), right.getAutomatonToMultiplicityMap());
+            
+            // If there was no restricted parallel composition yet, maybe the current composition is one, so check it.
+            if (!containsRestrictedParallelComposition) {
+                // FIXME.
+            }
+            
+            return CompositionInformation(joinedAutomatonToMultiplicity, containsRenameComposition, containsRestrictedParallelComposition);
+        }
+        
+    }
+}

src/storage/jani/CompositionInformationVisitor.h

@@ -0,0 +1,60 @@
+#pragma once
+
+#include <map>
+#include <set>
+#include <cstdint>
+
+#include "src/storage/jani/CompositionVisitor.h"
+
+namespace storm {
+    namespace jani {
+        
+        class Model;
+        
+        class CompositionInformation {
+        public:
+            CompositionInformation() = default;
+            CompositionInformation(std::map<std::string, uint64_t> const& automatonNameToMultiplicity, std::set<std::string> const& nonsilentActions, bool containsRenaming, bool containsRestrictedParallelComposition);
+
+            void increaseAutomatonMultiplicity(std::string const& automatonName, uint64_t count = 1);
+            
+            void addNonsilentAction(std::string const& actionName);
+            std::set<std::string> const& getNonsilentActions() const;
+            void renameNonsilentActions(std::map<std::string, std::string> const& renaming);
+            
+            void setContainsRenameComposition();
+            bool containsRenameComposition() const;
+            
+            void setContainsRestrictedParallelComposition();
+            bool containsRestrictedParallelComposition() const;
+            
+            static std::map<std::string, uint64_t> joinMultiplicityMaps(std::map<std::string, uint64_t> const& first, std::map<std::string, uint64_t> const& second);
+            std::map<std::string, uint64_t> const& getAutomatonToMultiplicityMap() const;
+            
+        private:
+            /// A mapping from the automata's names to the amount of times they occur in the composition.
+            std::map<std::string, uint64_t> automatonNameToMultiplicity;
+            
+            /// The set of non-silent actions contained in the composition.
+            std::set<std::string> nonsilentActions;
+            
+            /// A flag indicating whether the composition contains a renaming composition.
+            bool renameComposition;
+            
+            /// A flag indicating whether the composition contains
+            bool restrictedParallelComposition;
+        };
+        
+        class CompositionInformationVisitor : public CompositionVisitor {
+        public:
+            CompositionInformationVisitor() = default;
+            
+            CompositionInformation getInformation(Composition const& composition, Model const& model);
+            
+            virtual boost::any visit(AutomatonComposition const& composition, boost::any const& data) override;
+            virtual boost::any visit(RenameComposition const& composition, boost::any const& data) override;
+            virtual boost::any visit(ParallelComposition const& composition, boost::any const& data) override;
+        };
+        
+    }
+}

src/storage/jani/CompositionVisitor.h

@@ -5,6 +5,7 @@
 namespace storm {
     namespace jani {
         
+        class Composition;
         class AutomatonComposition;
         class RenameComposition;
         class ParallelComposition;

src/storage/jani/Compositions.h

@@ -0,0 +1,3 @@
+#include "src/storage/jani/AutomatonComposition.h"
+#include "src/storage/jani/RenameComposition.h"
+#include "src/storage/jani/ParallelComposition.h"

src/storage/jani/EdgeDestination.cpp

@@ -7,7 +7,7 @@ namespace storm {
     namespace jani {
         
         EdgeDestination::EdgeDestination(uint64_t locationId, storm::expressions::Expression const& probability, std::vector<Assignment> const& assignments, std::vector<RewardIncrement> const& rewardIncrements) : locationId(locationId), probability(probability), assignments(assignments), rewardIncrements(rewardIncrements) {
-            // Intentionally left empty.
+            sortAssignments();
         }
         
         void EdgeDestination::addAssignment(Assignment const& assignment) {
@@ -16,6 +16,7 @@ namespace storm {
                 STORM_LOG_THROW(oldAssignment.getExpressionVariable() != assignment.getExpressionVariable(), storm::exceptions::WrongFormatException, "Cannot add assignment '" << assignment << "', because another assignment '" << assignment << "' writes to the same target variable.");
             }
             assignments.push_back(assignment);
+            sortAssignments();
         }
         
         void EdgeDestination::addRewardIncrement(RewardIncrement const& rewardIncrement) {
@@ -46,5 +47,16 @@ namespace storm {
             return rewardIncrements;
         }
         
+        void EdgeDestination::sortAssignments() {
+            std::sort(this->assignments.begin(), this->assignments.end(), [] (storm::jani::Assignment const& assignment1, storm::jani::Assignment const& assignment2) {
+                bool smaller = assignment1.getExpressionVariable().getType().isBooleanType() && !assignment2.getExpressionVariable().getType().isBooleanType();
+                if (!smaller) {
+                    smaller = assignment1.getExpressionVariable() < assignment2.getExpressionVariable();
+                }
+                return smaller;
+            });
+
+        }
+        
     }
 }

src/storage/jani/EdgeDestination.h

@@ -58,6 +58,12 @@ namespace storm {
             std::vector<RewardIncrement> const& getRewardIncrements() const;
             
         private:
+            /*!
+             * Sorts the assignments to make all assignments to boolean variables precede all others and order the
+             * assignments within one variable group by the expression variables.
+             */
+            void sortAssignments();
+            
             // The id of the destination location.
             uint64_t locationId;
 

src/storage/jani/Model.cpp

@@ -357,6 +357,19 @@ namespace storm {
             return this->getModelType() == ModelType::DTMC || this->getModelType() == ModelType::CTMC;
         }
         
+        std::vector<storm::expressions::Expression> Model::getAllRangeExpressions() const {
+            std::vector<storm::expressions::Expression> result;
+            for (auto const& variable : this->getGlobalVariables().getBoundedIntegerVariables()) {
+                result.push_back(variable.getRangeExpression());
+            }
+            
+            for (auto const& automaton : automata) {
+                std::vector<storm::expressions::Expression> automatonRangeExpressions = automaton.getAllRangeExpressions();
+                result.insert(result.end(), automatonRangeExpressions.begin(), automatonRangeExpressions.end());
+            }
+            return result;
+        }
+        
         bool Model::checkValidity(bool logdbg) const {
             // TODO switch to exception based return value.
             

src/storage/jani/Model.h

@@ -248,6 +248,11 @@ namespace storm {
              */
             bool isDeterministicModel() const;
             
+            /*!
+             * Retrieves a list of expressions that characterize the legal values of the variables in this model.
+             */
+            std::vector<storm::expressions::Expression> getAllRangeExpressions() const;
+            
             /*!
              *  Checks if the model is valid JANI, which should be verified before any further operations are applied to a model.
              */

src/storage/prism/IntegerVariable.cpp

@@ -14,6 +14,10 @@ namespace storm {
             return this->upperBoundExpression;
         }
         
+        storm::expressions::Expression IntegerVariable::getRangeExpression() const {
+            return this->getLowerBoundExpression() <= this->getExpressionVariable() && this->getExpressionVariable() <= this->getUpperBoundExpression();
+        }
+        
         IntegerVariable IntegerVariable::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
             return IntegerVariable(this->getExpressionVariable(), this->getLowerBoundExpression().substitute(substitution), this->getUpperBoundExpression().substitute(substitution), this->getInitialValueExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
         }

src/storage/prism/IntegerVariable.h

@@ -45,6 +45,13 @@ namespace storm {
              */
             storm::expressions::Expression const& getUpperBoundExpression() const;
             
+            /*!
+             * Retrieves an expression characterizing the legal range of the variable.
+             *
+             * @return An expression characterizing the legal range of the variable.
+             */
+            storm::expressions::Expression getRangeExpression() const;
+            
             /*!
              * Substitutes all identifiers in the boolean variable according to the given map.
              *

src/storage/prism/Module.cpp

@@ -43,6 +43,25 @@ namespace storm {
             return this->integerVariables;
         }
         
+        std::set<storm::expressions::Variable> Module::getAllExpressionVariables() const {
+            std::set<storm::expressions::Variable> result;
+            for (auto const& var : this->getBooleanVariables()) {
+                result.insert(var.getExpressionVariable());
+            }
+            for (auto const& var : this->getIntegerVariables()) {
+                result.insert(var.getExpressionVariable());
+            }
+            return result;
+        }
+        
+        std::vector<storm::expressions::Expression> Module::getAllRangeExpressions() const {
+            std::vector<storm::expressions::Expression> result;
+            for (auto const& integerVariable : this->integerVariables) {
+                result.push_back(integerVariable.getRangeExpression());
+            }
+            return result;
+        }
+        
         std::size_t Module::getNumberOfCommands() const {
             return this->commands.size();
         }

src/storage/prism/Module.h

@@ -97,6 +97,22 @@ namespace storm {
              */
             std::vector<storm::prism::IntegerVariable> const& getIntegerVariables() const;
 
+            /*!
+             * Retrieves all expression variables used by this module.
+             *
+             * @return The set of expression variables used by this module.
+             */
+            std::set<storm::expressions::Variable> getAllExpressionVariables() const;
+            
+            
+            /*!
+             * Retrieves a list of expressions that characterize the legal ranges of all variables declared by this
+             * module.
+             *
+             * @return The list of expressions that characterize the legal ranges.
+             */
+            std::vector<storm::expressions::Expression> getAllRangeExpressions() const;
+            
             /*!
              * Retrieves the number of commands of this module.
              *

src/storage/prism/Program.cpp

@@ -349,6 +349,40 @@ namespace storm {
             return this->globalIntegerVariables;
         }
         
+        std::set<storm::expressions::Variable> Program::getAllExpressionVariables() const {
+            std::set<storm::expressions::Variable> result;
+            
+            for (auto const& constant : constants) {
+                result.insert(constant.getExpressionVariable());
+            }
+            for (auto const& variable : globalBooleanVariables) {
+                result.insert(variable.getExpressionVariable());
+            }
+            for (auto const& variable : globalIntegerVariables) {
+                result.insert(variable.getExpressionVariable());
+            }
+            for (auto const& module : modules) {
+                auto const& moduleVariables = module.getAllExpressionVariables();
+                result.insert(moduleVariables.begin(), moduleVariables.end());
+            }
+            
+            return result;
+        }
+        
+        std::vector<storm::expressions::Expression> Program::getAllRangeExpressions() const {
+            std::vector<storm::expressions::Expression> result;
+            for (auto const& globalIntegerVariable : this->globalIntegerVariables) {
+                result.push_back(globalIntegerVariable.getRangeExpression());
+            }
+            
+            for (auto const& module : modules) {
+                std::vector<storm::expressions::Expression> moduleRangeExpressions = module.getAllRangeExpressions();
+                result.insert(result.end(), moduleRangeExpressions.begin(), moduleRangeExpressions.end());
+            }
+            
+            return result;
+        }
+        
         bool Program::globalBooleanVariableExists(std::string const& variableName) const {
             return this->globalBooleanVariableToIndexMap.count(variableName) > 0;
         }

src/storage/prism/Program.h

@@ -199,6 +199,20 @@ namespace storm {
              */
             IntegerVariable const& getGlobalIntegerVariable(std::string const& variableName) const;
 
+            /*!
+             * Retrieves all expression variables used by this program.
+             *
+             * @return The set of expression variables used by this program.
+             */
+            std::set<storm::expressions::Variable> getAllExpressionVariables() const;
+            
+            /*!
+             * Retrieves a list of expressions that characterize the legal ranges of all variables.
+             *
+             * @return A list of expressions that characterize the legal ranges of all variables.
+             */
+            std::vector<storm::expressions::Expression> getAllRangeExpressions() const;
+            
             /*!
              * Retrieves the number of global boolean variables of the program.
              *

src/storage/prism/Update.cpp

@@ -9,7 +9,13 @@
 namespace storm {
     namespace prism {
         Update::Update(uint_fast64_t globalIndex, storm::expressions::Expression const& likelihoodExpression, std::vector<storm::prism::Assignment> const& assignments, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), likelihoodExpression(likelihoodExpression), assignments(assignments), variableToAssignmentIndexMap(), globalIndex(globalIndex) {
-            std::sort(this->assignments.begin(), this->assignments.end(), [] (storm::prism::Assignment const& assignment1, storm::prism::Assignment const& assignment2) { return assignment1.getVariable() < assignment2.getVariable(); } );
+            std::sort(this->assignments.begin(), this->assignments.end(), [] (storm::prism::Assignment const& assignment1, storm::prism::Assignment const& assignment2) {
+                bool smaller = assignment1.getVariable().getType().isBooleanType() && !assignment2.getVariable().getType().isBooleanType();
+                if (!smaller) {
+                    smaller = assignment1.getVariable() < assignment2.getVariable();
+                }
+                return smaller;
+            });
             this->createAssignmentMapping();
         }