Merge from future (not yet compiling)

Former-commit-id: 7ead44e805

src/CMakeLists.txt

@@ -12,6 +12,7 @@ file(GLOB_RECURSE STORM_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm.cpp)
 file(GLOB_RECURSE STORM_DFT_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm-dyftee.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_RECURSE STORM_GENERATOR_FILES ${PROJECT_SOURCE_DIR}/src/generator/*.h ${PROJECT_SOURCE_DIR}/src/generator/*.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)
@@ -63,6 +64,7 @@ source_group(main FILES ${STORM_MAIN_FILE})
 source_group(dft FILES ${STORM_DYFTTEE_FILE})
 source_group(adapters FILES ${STORM_ADAPTERS_FILES})
 source_group(builder FILES ${STORM_BUILDER_FILES})
+source_group(generator FILES ${STORM_GENERATOR_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.h

@@ -1,10 +1,10 @@
-#ifndef STORM_ADAPTERS_EXPLICITPRISMMODELBUILDER_H
-#define	STORM_ADAPTERS_EXPLICITPRISMMODELBUILDER_H
+#ifndef STORM_BUILDER_EXPLICITPRISMMODELBUILDER_H
+#define	STORM_BUILDER_EXPLICITPRISMMODELBUILDER_H
 
 #include <memory>
 #include <utility>
 #include <vector>
-#include <queue>
+#include <deque>
 #include <cstdint>
 #include <boost/functional/hash.hpp>
 #include <boost/container/flat_set.hpp>
@@ -22,9 +22,13 @@
 #include "src/storage/SparseMatrix.h"
 #include "src/settings/SettingsManager.h"
 
-#include "src/utility/constants.h"
 #include "src/utility/prism.h"
 
+#include "src/builder/ExplorationOrder.h"
+
+#include "src/generator/CompressedState.h"
+#include "src/generator/VariableInformation.h"
+
 namespace storm {
     namespace utility {
         template<typename ValueType> class ConstantsComparator;
@@ -33,30 +37,33 @@ namespace storm {
     namespace builder {
         
         using namespace storm::utility::prism;
+        using namespace storm::generator;
         
         // Forward-declare classes.
         template <typename ValueType> struct RewardModelBuilder;
         
-        template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename IndexType = uint32_t>
+        template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename StateType = uint32_t>
         class ExplicitPrismModelBuilder {
         public:
-            typedef storm::storage::BitVector CompressedState;
-            
             // A structure holding information about the reachable state space while building it.
             struct InternalStateInformation {
+                // Builds an empty state information.
+                InternalStateInformation();
+                
+                // Creates a state information structure for storing states of the given bit width.
                 InternalStateInformation(uint64_t bitsPerState);
 
                 // This member stores all the states and maps them to their unique indices.
-                storm::storage::BitVectorHashMap<IndexType> stateStorage;
+                storm::storage::BitVectorHashMap<StateType> stateStorage;
                 
                 // A list of initial states in terms of their global indices.
-                std::vector<IndexType> initialStateIndices;
+                std::vector<StateType> initialStateIndices;
 
                 // The number of bits of each state.
                 uint64_t bitsPerState;
                 
-                // A list of reachable states as indices in the stateToIndexMap.
-                std::vector<storm::storage::BitVector> reachableStates;
+                // The number of states that were found in the exploration so far.
+                uint_fast64_t numberOfStates;
             };
             
             // A structure holding information about the reachable state space that can be retrieved from the outside.
@@ -74,60 +81,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();
@@ -151,6 +104,11 @@ namespace storm {
                  */
                 Options();
                 
+                /*!
+                 * Copies the given set of options.
+                 */
+                Options(Options const& other) = default;
+                
                 /*! Creates an object representing the suggested building options assuming that the given formula is the
                  * only one to check. Additional formulas may be preserved by calling <code>preserveFormula</code>.
                  *
@@ -193,6 +151,9 @@ namespace storm {
                  */
                 void setTerminalStatesFromFormula(storm::logic::Formula const& formula);
                 
+                // The order in which to explore the model.
+                ExplorationOrder explorationOrder;
+                
                 // A flag that indicates whether or not command labels are to be built.
                 bool buildCommandLabels;
                 
@@ -228,6 +189,13 @@ namespace storm {
                 boost::optional<boost::variant<storm::expressions::Expression, std::string>> negatedTerminalStates;
             };
             
+            /*!
+             * Creates a builder for the given program.
+             *
+             * @param program The program to build.
+             */
+            ExplicitPrismModelBuilder(storm::prism::Program const& program, Options const& options = Options());
+            
             /*!
              * Convert the program given at construction time to an abstract model. The type of the model is the one
              * specified in the program. The given reward model name selects the rewards that the model will contain.
@@ -238,7 +206,7 @@ namespace storm {
              * @param rewardModel The reward model that is to be built.
              * @return The explicit model that was given by the probabilistic program.
              */
-            std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> translateProgram(storm::prism::Program program, Options const& options = Options());
+            std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> translate();
             
             /*!
              * If requested in the options, information about the variable valuations in the reachable states can be
@@ -249,39 +217,14 @@ namespace storm {
             StateInformation const& getStateInformation() const;
             
             /*!
-             * Retrieves the program that was actually translated (i.e. including constant substitutions etc.). Note
-             * that this function may only be called after a succesful translation.
+             * Retrieves the program that was actually translated (i.e. including constant substitutions etc.).
              *
              * @return The translated program.
              */
             storm::prism::Program const& getTranslatedProgram() const;
             
         private:
-            static void unpackStateIntoEvaluator(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<ValueType>& evaluator);
-
-            static storm::expressions::SimpleValuation unpackStateIntoValuation(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation);
-
-            /*!
-             * Applies an update to the given state and returns the resulting new state object. This methods does not
-             * modify the given state but returns a new one.
-             *
-             * @params state The state to which to apply the update.
-             * @params update The update to apply.
-             * @return The resulting state.
-             */
-            static CompressedState applyUpdate(VariableInformation const& variableInformation, CompressedState const& state, storm::prism::Update const& update, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator);
-            
-            /*!
-             * Applies an update to the given state and returns the resulting new state object. The update is evaluated
-             * over the variable values of the given base state. This methods does not modify the given state but
-             * returns a new one.
-             *
-             * @param state The state to which to apply the update.
-             * @param baseState The state used for evaluating the update.
-             * @param update The update to apply.
-             * @return The resulting state.
-             */
-            static CompressedState applyUpdate(VariableInformation const& variableInformation, CompressedState const& state, CompressedState const& baseState, storm::prism::Update const& update, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator);
+            storm::expressions::SimpleValuation unpackStateIntoValuation(storm::storage::BitVector const& currentState);
             
             /*!
              * Retrieves the state id of the given state. If the state has not been encountered yet, it will be added to
@@ -293,29 +236,8 @@ namespace storm {
              * @param internalStateInformation The information about the already explored part of the reachable state space.
              * @return A pair indicating whether the state was already discovered before and the state id of the state.
              */
-            static IndexType getOrAddStateIndex(CompressedState const& state, InternalStateInformation& internalStateInformation, std::queue<storm::storage::BitVector>& stateQueue);
+            StateType getOrAddStateIndex(CompressedState const& state);
     
-            /*!
-             * Retrieves all commands that are labeled with the given label and enabled in the given state, grouped by
-             * modules.
-             *
-             * This function will iterate over all modules and retrieve all commands that are labeled with the given
-             * action and active (i.e. enabled) in the current state. The result is a list of lists of commands in which
-             * the inner lists contain all commands of exactly one module. If a module does not have *any* (including
-             * disabled) commands, there will not be a list of commands of that module in the result. If, however, the
-             * module has a command with a relevant label, but no enabled one, nothing is returned to indicate that there
-             * is no legal transition possible.
-             *
-             * @param The program in which to search for active commands.
-             * @param state The current state.
-             * @param actionIndex The index of the action label to select.
-             * @return A list of lists of active commands or nothing.
-             */
-            static boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> getActiveCommandsByActionIndex(storm::prism::Program const& program,storm::expressions::ExpressionEvaluator<ValueType> const& evaluator, uint_fast64_t const& actionIndex);
-                        
-            static std::vector<Choice<ValueType>> getUnlabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, InternalStateInformation& internalStateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator, std::queue<storm::storage::BitVector>& stateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator);
-            
-            static std::vector<Choice<ValueType>> getLabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, InternalStateInformation& internalStateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator, std::queue<storm::storage::BitVector>& stateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator);
             /*!
              * Builds the transition matrix and the transition reward matrix based for the given program.
              *
@@ -333,7 +255,7 @@ namespace storm {
              * @return A tuple containing a vector with all rows at which the nondeterministic choices of each state begin
              * and a vector containing the labels associated with each choice.
              */
-            static boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, InternalStateInformation& internalStateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, boost::optional<storm::expressions::Expression> const& terminalExpression);
+            boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> buildMatrices(std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, boost::optional<storm::expressions::Expression> const& terminalExpression);
             
             /*!
              * Explores the state space of the given program and returns the components of the model as a result.
@@ -343,7 +265,7 @@ namespace storm {
              * @param options A set of options used to customize the building process.
              * @return A structure containing the components of the resulting model.
              */
-            ModelComponents buildModelComponents(storm::prism::Program const& program, std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, Options const& options);
+            ModelComponents buildModelComponents(std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels);
             
             /*!
              * Builds the state labeling for the given program.
@@ -353,17 +275,34 @@ namespace storm {
              * @param internalStateInformation Information about the state space of the program.
              * @return The state labeling of the given program.
              */
-            static storm::models::sparse::StateLabeling buildStateLabeling(storm::prism::Program const& program, VariableInformation const& variableInformation, InternalStateInformation const& internalStateInformation);
+            storm::models::sparse::StateLabeling buildStateLabeling();
+            
+            // The program to translate. The necessary transformations are performed upon construction of the builder.
+            storm::prism::Program program;
+            
+            // The options to be used for translating the program.
+            Options options;
+            
+            // The variable information.
+            VariableInformation variableInformation;
+            
+            // Internal information about the states that were explored.
+            InternalStateInformation internalStateInformation;
             
             // This member holds information about reachable states that can be retrieved from the outside after a
             // successful build.
             boost::optional<StateInformation> stateInformation;
             
-            // This member holds the program that was most recently translated (if any).
-            boost::optional<storm::prism::Program> preparedProgram;
+            // A set of states that still need to be explored.
+            std::deque<CompressedState> statesToExplore;
+            
+            // An optional mapping from state indices to the row groups in which they actually reside. This needs to be
+            // built in case the exploration order is not BFS.
+            boost::optional<std::vector<uint_fast64_t>> stateRemapping;
+
         };
         
     } // namespace adapters
 } // namespace storm
 
-#endif	/* STORM_ADAPTERS_EXPLICITPRISMMODELBUILDER_H */
+#endif	/* STORM_BUILDER_EXPLICITPRISMMODELBUILDER_H */

src/builder/ExplorationOrder.cpp

@@ -0,0 +1,22 @@
+#include "src/builder/ExplorationOrder.h"
+
+namespace storm {
+    namespace builder {
+        
+        std::ostream& operator<<(std::ostream& out, ExplorationOrder const& order) {
+            switch (order) {
+                case ExplorationOrder::Dfs:
+                    out << "depth-first";
+                    break;
+                case ExplorationOrder::Bfs:
+                    out << "breadth-first";
+                    break;
+                default:
+                    out << "undefined";
+                    break;
+            }
+            return out;
+        }
+        
+    }
+}

src/builder/ExplorationOrder.h

@@ -0,0 +1,17 @@
+#ifndef STORM_BUILDER_EXPLORATIONORDER_H_
+#define STORM_BUILDER_EXPLORATIONORDER_H_
+
+#include <ostream>
+
+namespace storm {
+    namespace builder {
+        
+        // An enum that contains all currently supported exploration orders.
+        enum class ExplorationOrder { Dfs, Bfs };
+        
+        std::ostream& operator<<(std::ostream& out, ExplorationOrder const& order);
+        
+    }
+}
+
+#endif /* STORM_BUILDER_EXPLORATIONORDER_H_ */

src/generator/Choice.cpp

@@ -0,0 +1,105 @@
+#include "src/generator/Choice.h"
+
+#include "src/adapters/CarlAdapter.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>()), choiceRewards() {
+            // 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>
+        void Choice<ValueType, StateType>::addProbability(StateType const& state, ValueType const& value) {
+            totalMass += value;
+            distribution.addProbability(state, value);
+        }
+        
+        template<typename ValueType, typename StateType>
+        void Choice<ValueType, StateType>::addChoiceReward(ValueType const& value) {
+            choiceRewards.push_back(value);
+        }
+        
+        template<typename ValueType, typename StateType>
+        std::vector<ValueType> const& Choice<ValueType, StateType>::getChoiceRewards() const {
+            return choiceRewards;
+        }
+        
+        template<typename ValueType, typename StateType>
+        bool Choice<ValueType, StateType>::isMarkovian() const {
+            return markovian;
+        }
+        
+        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;
+        }
+        
+        template class Choice<double>;
+        template class Choice<storm::RationalFunction>;
+    }
+}

src/generator/Choice.h

@@ -0,0 +1,150 @@
+#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;
+            
+            /*!
+             * 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 rewards for this choice under selected reward models.
+             */
+            std::vector<ValueType> const& getChoiceRewards() const;
+            
+            /*!
+             * Retrieves whether the choice is Markovian.
+             */
+            bool isMarkovian() const;
+            
+            /*!
+             * 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 values associated with this choice.
+            std::vector<ValueType> choiceRewards;
+            
+            // 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/CompressedState.cpp

@@ -0,0 +1,23 @@
+#include "src/generator/CompressedState.h"
+
+#include "src/generator/VariableInformation.h"
+#include "src/storage/expressions/ExpressionEvaluator.h"
+
+namespace storm {
+    namespace generator {
+        
+        template<typename ValueType>
+        void unpackStateIntoEvaluator(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<ValueType>& evaluator) {
+            for (auto const& booleanVariable : variableInformation.booleanVariables) {
+                evaluator.setBooleanValue(booleanVariable.variable, state.get(booleanVariable.bitOffset));
+            }
+            for (auto const& integerVariable : variableInformation.integerVariables) {
+                evaluator.setIntegerValue(integerVariable.variable, state.getAsInt(integerVariable.bitOffset, integerVariable.bitWidth) + integerVariable.lowerBound);
+            }
+
+        }
+
+        template void unpackStateIntoEvaluator<double>(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<double>& evaluator);
+        template void unpackStateIntoEvaluator<storm::RationalFunction>(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<storm::RationalFunction>& evaluator);
+    }
+}

src/generator/CompressedState.h

@@ -0,0 +1,30 @@
+#ifndef STORM_GENERATOR_COMPRESSEDSTATE_H_
+#define STORM_GENERATOR_COMPRESSEDSTATE_H_
+
+#include "src/storage/BitVector.h"
+
+namespace storm {
+    namespace expressions {
+        template<typename ValueType> class ExpressionEvaluator;
+    }
+    
+    namespace generator {
+        
+        typedef storm::storage::BitVector CompressedState;
+
+        class VariableInformation;
+        
+        /*!
+         * Unpacks the compressed state into the evaluator.
+         *
+         * @param state The state to unpack.
+         * @param variableInformation The information about how the variables are packed with the state.
+         * @param evaluator The evaluator into which to load the state.
+         */
+        template<typename ValueType>
+        void unpackStateIntoEvaluator(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<ValueType>& evaluator);
+    }
+}
+
+#endif /* STORM_GENERATOR_COMPRESSEDSTATE_H_ */
+

src/generator/NextStateGenerator.h

@@ -0,0 +1,24 @@
+#ifndef STORM_GENERATOR_NEXTSTATEGENERATOR_H_
+#define STORM_GENERATOR_NEXTSTATEGENERATOR_H_
+
+#include <vector>
+#include <cstdint>
+
+#include "src/generator/CompressedState.h"
+#include "src/generator/StateBehavior.h"
+
+namespace storm {
+    namespace generator {
+        template<typename ValueType, typename StateType = uint32_t>
+        class NextStateGenerator {
+        public:
+            typedef std::function<StateType (CompressedState const&)> StateToIdCallback;
+
+            virtual bool isDeterministicModel() const = 0;
+            virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) = 0;
+            virtual StateBehavior<ValueType, StateType> expand(CompressedState const& state, StateToIdCallback const& stateToIdCallback) = 0;
+        };
+    }
+}
+
+#endif /* STORM_GENERATOR_NEXTSTATEGENERATOR_H_ */

src/generator/PrismNextStateGenerator.cpp

@@ -0,0 +1,404 @@
+#include "src/generator/PrismNextStateGenerator.h"
+
+#include <boost/container/flat_map.hpp>
+
+#include "src/utility/constants.h"
+#include "src/utility/macros.h"
+#include "src/exceptions/WrongFormatException.h"
+
+namespace storm {
+    namespace generator {
+        
+        template<typename ValueType, typename StateType>
+        PrismNextStateGenerator<ValueType, StateType>::PrismNextStateGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation, bool buildChoiceLabeling) : program(program), selectedRewardModels(), buildChoiceLabeling(buildChoiceLabeling), variableInformation(variableInformation), evaluator(program.getManager()), comparator() {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType, typename StateType>
+        void PrismNextStateGenerator<ValueType, StateType>::addRewardModel(storm::prism::RewardModel const& rewardModel) {
+            selectedRewardModels.push_back(rewardModel);
+            hasStateActionRewards |= rewardModel.hasStateActionRewards();
+        }
+        
+        template<typename ValueType, typename StateType>
+        void PrismNextStateGenerator<ValueType, StateType>::setTerminalExpression(storm::expressions::Expression const& terminalExpression) {
+            this->terminalExpression = terminalExpression;
+        }
+        
+        template<typename ValueType, typename StateType>
+        bool PrismNextStateGenerator<ValueType, StateType>::isDeterministicModel() const {
+            return program.isDeterministicModel();
+        }
+        
+        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.
+            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>
+        StateBehavior<ValueType, StateType> PrismNextStateGenerator<ValueType, StateType>::expand(CompressedState const& state, StateToIdCallback const& stateToIdCallback) {
+            // Since almost all subsequent operations are based on the evaluator, we load the state into it now.
+            unpackStateIntoEvaluator(state, variableInformation, evaluator);
+
+            // Prepare the result, in case we return early.
+            StateBehavior<ValueType, StateType> result;
+            
+            // First, construct the state rewards, as we may return early if there are no choices later and we already
+            // need the state rewards then.
+            for (auto const& rewardModel : selectedRewardModels) {
+                ValueType stateRewardValue = storm::utility::zero<ValueType>();
+                if (rewardModel.get().hasStateRewards()) {
+                    for (auto const& stateReward : rewardModel.get().getStateRewards()) {
+                        if (evaluator.asBool(stateReward.getStatePredicateExpression())) {
+                            stateRewardValue += ValueType(evaluator.asRational(stateReward.getRewardValueExpression()));
+                        }
+                    }
+                }
+                result.addStateReward(stateRewardValue);
+            }
+            
+            // If a terminal expression was set and we must not expand this state, return now.
+            if (terminalExpression && evaluator.asBool(terminalExpression.get())) {
+                return result;
+            }
+            
+            // Get all choices for the state.
+            std::vector<Choice<ValueType>> allChoices = getUnlabeledChoices(state, stateToIdCallback);
+            std::vector<Choice<ValueType>> allLabeledChoices = getLabeledChoices(state, stateToIdCallback);
+            for (auto& choice : allLabeledChoices) {
+                allChoices.push_back(std::move(choice));
+            }
+            
+            std::size_t totalNumberOfChoices = allChoices.size();
+            
+            // If there is not a single choice, we return immediately, because the state has no behavior (other than
+            // the state reward).
+            if (totalNumberOfChoices == 0) {
+                return result;
+            }
+            
+            // If the model is a deterministic model, we need to fuse the choices into one.
+            if (program.isDeterministicModel() && totalNumberOfChoices > 1) {
+                Choice<ValueType> globalChoice;
+                
+                // For CTMCs, we need to keep track of the total exit rate to scale the action rewards later. For DTMCs
+                // this is equal to the number of choices, which is why we initialize it like this here.
+                ValueType totalExitRate = program.isDiscreteTimeModel() ? static_cast<ValueType>(totalNumberOfChoices) : storm::utility::zero<ValueType>();
+                
+                // Iterate over all choices and combine the probabilities/rates into one choice.
+                for (auto const& choice : allChoices) {
+                    for (auto const& stateProbabilityPair : choice) {
+                        if (program.isDiscreteTimeModel()) {
+                            globalChoice.addProbability(stateProbabilityPair.first, stateProbabilityPair.second / totalNumberOfChoices);
+                        } else {
+                            globalChoice.addProbability(stateProbabilityPair.first, stateProbabilityPair.second);
+                        }
+                    }
+                    
+                    if (hasStateActionRewards && !program.isDiscreteTimeModel()) {
+                        totalExitRate += choice.getTotalMass();
+                    }
+                    
+                    if (buildChoiceLabeling) {
+                        globalChoice.addChoiceLabels(choice.getChoiceLabels());
+                    }
+                }
+                
+                // Now construct the state-action reward for all selected reward models.
+                for (auto const& rewardModel : selectedRewardModels) {
+                    ValueType stateActionRewardValue = storm::utility::zero<ValueType>();
+                    if (rewardModel.get().hasStateActionRewards()) {
+                        for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) {
+                            for (auto const& choice : allChoices) {
+                                if (stateActionReward.getActionIndex() == choice.getActionIndex() && evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
+                                    stateActionRewardValue += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass() / totalExitRate;
+                                }
+                            }
+                            
+                        }
+                    }
+                    globalChoice.addChoiceReward(stateActionRewardValue);
+                }
+                
+                // Move the newly fused choice in place.
+                allChoices.clear();
+                allChoices.push_back(std::move(globalChoice));
+            }
+            
+            // Move all remaining choices in place.
+            for (auto& choice : allChoices) {
+                result.addChoice(std::move(choice));
+            }
+            
+            result.setExpanded();
+            return result;
+        }
+        
+        template<typename ValueType, typename StateType>
+        CompressedState PrismNextStateGenerator<ValueType, StateType>::applyUpdate(CompressedState const& state, storm::prism::Update const& update) {
+            CompressedState newState(state);
+            
+            auto assignmentIt = update.getAssignments().begin();
+            auto assignmentIte = update.getAssignments().end();
+            
+            // Iterate over all boolean assignments and carry them out.
+            auto boolIt = variableInformation.booleanVariables.begin();
+            for (; assignmentIt != assignmentIte && assignmentIt->getExpression().hasBooleanType(); ++assignmentIt) {
+                while (assignmentIt->getVariable() != boolIt->variable) {
+                    ++boolIt;
+                }
+                newState.set(boolIt->bitOffset, evaluator.asBool(assignmentIt->getExpression()));
+            }
+            
+            // Iterate over all integer assignments and carry them out.
+            auto integerIt = variableInformation.integerVariables.begin();
+            for (; assignmentIt != assignmentIte && assignmentIt->getExpression().hasIntegerType(); ++assignmentIt) {
+                while (assignmentIt->getVariable() != integerIt->variable) {
+                    ++integerIt;
+                }
+                int_fast64_t assignedValue = evaluator.asInt(assignmentIt->getExpression());
+                STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'.");
+                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>
+        boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> PrismNextStateGenerator<ValueType, StateType>::getActiveCommandsByActionIndex(uint_fast64_t const& actionIndex) {
+            boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> result((std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>()));
+            
+            // Iterate over all modules.
+            for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
+                storm::prism::Module const& module = program.getModule(i);
+                
+                // If the module has no command labeled with the given action, we can skip this module.
+                if (!module.hasActionIndex(actionIndex)) {
+                    continue;
+                }
+                
+                std::set<uint_fast64_t> const& commandIndices = module.getCommandIndicesByActionIndex(actionIndex);
+                
+                // If the module contains the action, but there is no command in the module that is labeled with
+                // this action, we don't have any feasible command combinations.
+                if (commandIndices.empty()) {
+                    return boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>>();
+                }
+                
+                std::vector<std::reference_wrapper<storm::prism::Command const>> commands;
+                
+                // Look up commands by their indices and add them if the guard evaluates to true in the given state.
+                for (uint_fast64_t commandIndex : commandIndices) {
+                    storm::prism::Command const& command = module.getCommand(commandIndex);
+                    if (evaluator.asBool(command.getGuardExpression())) {
+                        commands.push_back(command);
+                    }
+                }
+                
+                // If there was no enabled command although the module has some command with the required action label,
+                // we must not return anything.
+                if (commands.size() == 0) {
+                    return boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>>();
+                }
+                
+                result.get().push_back(std::move(commands));
+            }
+            
+            return result;
+        }
+        
+        template<typename ValueType, typename StateType>
+        std::vector<Choice<ValueType>> PrismNextStateGenerator<ValueType, StateType>::getUnlabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback) {
+            std::vector<Choice<ValueType>> result;
+            
+            // Iterate over all modules.
+            for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
+                storm::prism::Module const& module = program.getModule(i);
+                
+                // Iterate over all commands.
+                for (uint_fast64_t j = 0; j < module.getNumberOfCommands(); ++j) {
+                    storm::prism::Command const& command = module.getCommand(j);
+                    
+                    // Only consider unlabeled commands.
+                    if (command.isLabeled()) continue;
+                    
+                    // Skip the command, if it is not enabled.
+                    if (!evaluator.asBool(command.getGuardExpression())) {
+                        continue;
+                    }
+                    
+                    result.push_back(Choice<ValueType>(command.getActionIndex()));
+                    Choice<ValueType>& choice = result.back();
+                    
+                    // Remember the command labels only if we were asked to.
+                    if (buildChoiceLabeling) {
+                        choice.addChoiceLabel(command.getGlobalIndex());
+                    }
+                    
+                    // Iterate over all updates of the current command.
+                    ValueType probabilitySum = storm::utility::zero<ValueType>();
+                    for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) {
+                        storm::prism::Update const& update = command.getUpdate(k);
+                        
+                        // Obtain target state index and add it to the list of known states. If it has not yet been
+                        // seen, we also add it to the set of states that have yet to be explored.
+                        StateType stateIndex = stateToIdCallback(applyUpdate(state, update));
+                        
+                        // Update the choice by adding the probability/target state to it.
+                        ValueType probability = evaluator.asRational(update.getLikelihoodExpression());
+                        choice.addProbability(stateIndex, probability);
+                        probabilitySum += probability;
+                    }
+                    
+                    // Create the state-action reward for the newly created choice.
+                    for (auto const& rewardModel : selectedRewardModels) {
+                        ValueType stateActionRewardValue = storm::utility::zero<ValueType>();
+                        if (rewardModel.get().hasStateActionRewards()) {
+                            for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) {
+                                if (stateActionReward.getActionIndex() == choice.getActionIndex() && evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
+                                    stateActionRewardValue += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass();
+                                }
+                            }
+                        }
+                        choice.addChoiceReward(stateActionRewardValue);
+                    }
+                    
+                    // Check that the resulting distribution is in fact a distribution.
+                    STORM_LOG_THROW(!program.isDiscreteTimeModel() || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (actually sum to " << probabilitySum << ").");
+                }
+            }
+            
+            return result;
+        }
+        
+        template<typename ValueType, typename StateType>
+        std::vector<Choice<ValueType>> PrismNextStateGenerator<ValueType, StateType>::getLabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback) {
+            std::vector<Choice<ValueType>> result;
+            
+            for (uint_fast64_t actionIndex : program.getSynchronizingActionIndices()) {
+                boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> optionalActiveCommandLists = getActiveCommandsByActionIndex(actionIndex);
+                
+                // Only process this action label, if there is at least one feasible solution.
+                if (optionalActiveCommandLists) {
+                    std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>> const& activeCommandList = optionalActiveCommandLists.get();
+                    std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>::const_iterator> iteratorList(activeCommandList.size());
+                    
+                    // Initialize the list of iterators.
+                    for (size_t i = 0; i < activeCommandList.size(); ++i) {
+                        iteratorList[i] = activeCommandList[i].cbegin();
+                    }
+                    
+                    // As long as there is one feasible combination of commands, keep on expanding it.
+                    bool done = false;
+                    while (!done) {
+                        boost::container::flat_map<CompressedState, ValueType>* currentTargetStates = new boost::container::flat_map<CompressedState, ValueType>();
+                        boost::container::flat_map<CompressedState, ValueType>* newTargetStates = new boost::container::flat_map<CompressedState, ValueType>();
+                        
+                        currentTargetStates->emplace(state, storm::utility::one<ValueType>());
+                        
+                        for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
+                            storm::prism::Command const& command = *iteratorList[i];
+                            
+                            for (uint_fast64_t j = 0; j < command.getNumberOfUpdates(); ++j) {
+                                storm::prism::Update const& update = command.getUpdate(j);
+                                
+                                for (auto const& stateProbabilityPair : *currentTargetStates) {
+                                    // Compute the new state under the current update and add it to the set of new target states.
+                                    CompressedState newTargetState = applyUpdate(stateProbabilityPair.first, update);
+                                    newTargetStates->emplace(newTargetState, stateProbabilityPair.second * evaluator.asRational(update.getLikelihoodExpression()));
+                                }
+                            }
+                            
+                            // If there is one more command to come, shift the target states one time step back.
+                            if (i < iteratorList.size() - 1) {
+                                delete currentTargetStates;
+                                currentTargetStates = newTargetStates;
+                                newTargetStates = new boost::container::flat_map<CompressedState, ValueType>();
+                            }
+                        }
+                        
+                        // At this point, we applied all commands of the current command combination and newTargetStates
+                        // contains all target states and their respective probabilities. That means we are now ready to
+                        // add the choice to the list of transitions.
+                        result.push_back(Choice<ValueType>(actionIndex));
+                        
+                        // Now create the actual distribution.
+                        Choice<ValueType>& choice = result.back();
+                        
+                        // Remember the command labels only if we were asked to.
+                        if (buildChoiceLabeling) {
+                            // Add the labels of all commands to this choice.
+                            for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
+                                choice.addChoiceLabel(iteratorList[i]->get().getGlobalIndex());
+                            }
+                        }
+                        
+                        // Add the probabilities/rates to the newly created choice.
+                        ValueType probabilitySum = storm::utility::zero<ValueType>();
+                        for (auto const& stateProbabilityPair : *newTargetStates) {
+                            StateType actualIndex = stateToIdCallback(stateProbabilityPair.first);
+                            choice.addProbability(actualIndex, stateProbabilityPair.second);
+                            probabilitySum += stateProbabilityPair.second;
+                        }
+                        
+                        // Check that the resulting distribution is in fact a distribution.
+                        STORM_LOG_THROW(!program.isDiscreteTimeModel() || !comparator.isConstant(probabilitySum) || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not some to one for some command (actually sum to " << probabilitySum << ").");
+                        
+                        // Create the state-action reward for the newly created choice.
+                        for (auto const& rewardModel : selectedRewardModels) {
+                            ValueType stateActionRewardValue = storm::utility::zero<ValueType>();
+                            if (rewardModel.get().hasStateActionRewards()) {
+                                for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) {
+                                    if (stateActionReward.getActionIndex() == choice.getActionIndex() && evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
+                                        stateActionRewardValue += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass();
+                                    }
+                                }
+                            }
+                            choice.addChoiceReward(stateActionRewardValue);
+                        }
+                        
+                        // Dispose of the temporary maps.
+                        delete currentTargetStates;
+                        delete newTargetStates;
+                        
+                        // Now, check whether there is one more command combination to consider.
+                        bool movedIterator = false;
+                        for (int_fast64_t j = iteratorList.size() - 1; j >= 0; --j) {
+                            ++iteratorList[j];
+                            if (iteratorList[j] != activeCommandList[j].end()) {
+                                movedIterator = true;
+                            } else {
+                                // Reset the iterator to the beginning of the list.
+                                iteratorList[j] = activeCommandList[j].begin();
+                            }
+                        }
+                        
+                        done = !movedIterator;
+                    }
+                }
+            }
+            
+            return result;
+        }
+        
+        template class PrismNextStateGenerator<double>;
+        template class PrismNextStateGenerator<storm::RationalFunction>;
+    }
+}

src/generator/PrismNextStateGenerator.h

@@ -0,0 +1,108 @@
+#ifndef STORM_GENERATOR_PRISMNEXTSTATEGENERATOR_H_
+#define STORM_GENERATOR_PRISMNEXTSTATEGENERATOR_H_
+
+#include "src/generator/NextStateGenerator.h"
+#include "src/generator/VariableInformation.h"
+
+#include "src/storage/prism/Program.h"
+#include "src/storage/expressions/ExpressionEvaluator.h"
+
+#include "src/utility/ConstantsComparator.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, VariableInformation const& variableInformation, bool buildChoiceLabeling);
+            
+            /*!
+             * Adds a reward model to the list of selected reward models ()
+             */
+            void addRewardModel(storm::prism::RewardModel const& rewardModel);
+            
+            /*!
+             * Sets an expression such that if it evaluates to true in a state, prevents the exploration.
+             */
+            void setTerminalExpression(storm::expressions::Expression const& terminalExpression);
+            
+            virtual bool isDeterministicModel() const override;
+            virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) override;
+            virtual StateBehavior<ValueType, StateType> expand(CompressedState const& state, StateToIdCallback const& stateToIdCallback) 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::prism::Update const& update);
+            
+            /*!
+             * Retrieves all commands that are labeled with the given label and enabled in the given state, grouped by
+             * modules.
+             *
+             * This function will iterate over all modules and retrieve all commands that are labeled with the given
+             * action and active (i.e. enabled) in the current state. The result is a list of lists of commands in which
+             * the inner lists contain all commands of exactly one module. If a module does not have *any* (including
+             * disabled) commands, there will not be a list of commands of that module in the result. If, however, the
+             * module has a command with a relevant label, but no enabled one, nothing is returned to indicate that there
+             * is no legal transition possible.
+             *
+             * @param The program in which to search for active commands.
+             * @param state The current state.
+             * @param actionIndex The index of the action label to select.
+             * @return A list of lists of active commands or nothing.
+             */
+            boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> getActiveCommandsByActionIndex(uint_fast64_t const& actionIndex);
+            
+            /*!
+             * Retrieves all unlabeled choices possible from the given state.
+             *
+             * @param state The state for which to retrieve the unlabeled choices.
+             * @return The unlabeled choices of the state.
+             */
+            std::vector<Choice<ValueType>> getUnlabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback);
+            
+            /*!
+             * Retrieves all labeled choices possible from the given state.
+             *
+             * @param state The state for which to retrieve the unlabeled choices.
+             * @return The labeled choices of the state.
+             */
+            std::vector<Choice<ValueType>> getLabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback);
+            
+            // The program used for the generation of next states.
+            storm::prism::Program const& program;
+            
+            // The reward models that need to be considered.
+            std::vector<std::reference_wrapper<storm::prism::RewardModel const>> selectedRewardModels;
+            
+            // A flag that stores whether at least one of the selected reward models has state-action rewards.
+            bool hasStateActionRewards;
+            
+            // A flag that stores whether or not to build the choice labeling.
+            bool buildChoiceLabeling;
+            
+            // An optional expression that governs which states must not be explored.
+            boost::optional<storm::expressions::Expression> terminalExpression;
+
+            // Information about how the variables are packed.
+            VariableInformation const& variableInformation;
+            
+            // An evaluator used to evaluate expressions.
+            storm::expressions::ExpressionEvaluator<ValueType> evaluator;
+            
+            // A comparator used to compare constants.
+            storm::utility::ConstantsComparator<ValueType> comparator;
+        };
+        
+    }
+}
+
+#endif /* STORM_GENERATOR_PRISMNEXTSTATEGENERATOR_H_ */

src/generator/PrismStateLabelingGenerator.cpp

@@ -0,0 +1,50 @@
+#include "src/generator/PrismStateLabelingGenerator.h"
+
+#include "src/generator/CompressedState.h"
+
+#include "src/storage/expressions/ExpressionEvaluator.h"
+
+namespace storm {
+    namespace generator {
+        
+        template<typename ValueType, typename StateType>
+        PrismStateLabelingGenerator<ValueType, StateType>::PrismStateLabelingGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation) : program(program), variableInformation(variableInformation) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType, typename StateType>
+        storm::models::sparse::StateLabeling PrismStateLabelingGenerator<ValueType, StateType>::generate(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices) {
+            std::vector<storm::prism::Label> const& labels = program.getLabels();
+            
+            storm::expressions::ExpressionEvaluator<ValueType> evaluator(program.getManager());
+            storm::models::sparse::StateLabeling result(states.size());
+            
+            // Initialize labeling.
+            for (auto const& label : labels) {
+                result.addLabel(label.getName());
+            }
+            for (auto const& stateIndexPair : states) {
+                unpackStateIntoEvaluator(stateIndexPair.first, variableInformation, evaluator);
+                
+                for (auto const& label : labels) {
+                    // Add label to state, if the corresponding expression is true.
+                    if (evaluator.asBool(label.getStatePredicateExpression())) {
+                        result.addLabelToState(label.getName(), stateIndexPair.second);
+                    }
+                }
+            }
+            
+            // Also label the initial state with the special label "init".
+            result.addLabel("init");
+            for (auto index : initialStateIndices) {
+                result.addLabelToState("init", index);
+            }
+            
+            return result;
+        }
+        
+        template class PrismStateLabelingGenerator<double, uint32_t>;
+        template class PrismStateLabelingGenerator<storm::RationalFunction, uint32_t>;
+
+    }
+}

src/generator/PrismStateLabelingGenerator.h

@@ -0,0 +1,31 @@
+#ifndef STORM_GENERATOR_PRISMSTATELABELINGGENERATOR_H_
+#define STORM_GENERATOR_PRISMSTATELABELINGGENERATOR_H_
+
+#include "src/generator/StateLabelingGenerator.h"
+
+#include "src/generator/VariableInformation.h"
+
+#include "src/storage/prism/Program.h"
+
+namespace storm {
+    namespace generator {
+        
+        template<typename ValueType, typename StateType = uint32_t>
+        class PrismStateLabelingGenerator : public StateLabelingGenerator<StateType> {
+        public:
+            PrismStateLabelingGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation);
+            
+            virtual storm::models::sparse::StateLabeling generate(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}) override;
+            
+        private:
+            // The program for which to generate the labels.
+            storm::prism::Program const& program;
+            
+            // Information about how the variables are packed.
+            VariableInformation const& variableInformation;
+        };
+        
+    }
+}
+
+#endif /* STORM_GENERATOR_PRISMSTATELABELINGGENERATOR_H_ */

src/generator/StateBehavior.cpp

@@ -0,0 +1,57 @@
+#include "src/generator/StateBehavior.h"
+
+#include "src/adapters/CarlAdapter.h"
+
+namespace storm {
+    namespace generator {
+
+        template<typename ValueType, typename StateType>
+        StateBehavior<ValueType, StateType>::StateBehavior() : expanded(false) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType, typename StateType>
+        void StateBehavior<ValueType, StateType>::addChoice(Choice<ValueType, StateType>&& choice) {
+            choices.push_back(std::move(choice));
+        }
+        
+        template<typename ValueType, typename StateType>
+        void StateBehavior<ValueType, StateType>::addStateReward(ValueType const& stateReward) {
+            stateRewards.push_back(stateReward);
+        }
+        
+        template<typename ValueType, typename StateType>
+        void StateBehavior<ValueType, StateType>::setExpanded(bool newValue) {
+            this->expanded = newValue;
+        }
+        
+        template<typename ValueType, typename StateType>
+        bool StateBehavior<ValueType, StateType>::wasExpanded() const {
+            return expanded;
+        }
+        
+        template<typename ValueType, typename StateType>
+        bool StateBehavior<ValueType, StateType>::empty() const {
+            return choices.empty();
+        }
+        
+        template<typename ValueType, typename StateType>
+        typename std::vector<Choice<ValueType, StateType>>::const_iterator StateBehavior<ValueType, StateType>::begin() const {
+            return choices.begin();
+        }
+        
+        template<typename ValueType, typename StateType>
+        typename std::vector<Choice<ValueType, StateType>>::const_iterator StateBehavior<ValueType, StateType>::end() const {
+            return choices.end();
+        }
+        
+        template<typename ValueType, typename StateType>
+        std::vector<ValueType> const& StateBehavior<ValueType, StateType>::getStateRewards() const {
+            return stateRewards;
+        }
+        
+        template class StateBehavior<double>;
+        template class StateBehavior<storm::RationalFunction>;
+
+    }
+}

src/generator/StateBehavior.h

@@ -0,0 +1,73 @@
+#ifndef STORM_GENERATOR_PRISM_STATEBEHAVIOR_H_
+#define STORM_GENERATOR_PRISM_STATEBEHAVIOR_H_
+
+#include <cstdint>
+
+#include "src/generator/Choice.h"
+
+namespace storm {
+    namespace generator {
+        
+        template<typename ValueType, typename StateType = uint32_t>
+        class StateBehavior {
+        public:
+            /*!
+             * Creates an empty behavior, i.e. the state was not yet expanded.
+             */
+            StateBehavior();
+            
+            /*!
+             * Adds the given choice to the behavior of the state.
+             */
+            void addChoice(Choice<ValueType, StateType>&& choice);
+            
+            /*!
+             * Adds the given state reward to the behavior of the state.
+             */
+            void addStateReward(ValueType const& stateReward);
+            
+            /*!
+             * Sets whether the state was expanded.
+             */
+            void setExpanded(bool newValue = true);
+            
+            /*!
+             * Retrieves whether the state was expanded.
+             */
+            bool wasExpanded() const;
+            
+            /*!
+             * Retrieves whether the behavior is empty in the sense that there are no available choices.
+             */
+            bool empty() const;
+            
+            /*!
+             * Retrieves an iterator to the choices available in the behavior.
+             */
+            typename std::vector<Choice<ValueType, StateType>>::const_iterator begin() const;
+
+            /*!
+             * Retrieves an iterator past the choices available in the behavior.
+             */
+            typename std::vector<Choice<ValueType, StateType>>::const_iterator end() const;
+
+            /*!
+             * Retrieves the list of state rewards under selected reward models.
+             */
+            std::vector<ValueType> const& getStateRewards() const;
+            
+        private:
+            // The choices available in the state.
+            std::vector<Choice<ValueType, StateType>> choices;
+            
+            // The state rewards (under the different, selected reward models) of the state.
+            std::vector<ValueType> stateRewards;
+            
+            // A flag indicating whether the state was actually expanded.
+            bool expanded;
+        };
+        
+    }
+}
+
+#endif /* STORM_GENERATOR_PRISM_STATEBEHAVIOR_H_ */

src/generator/StateLabelingGenerator.h

@@ -0,0 +1,20 @@
+#ifndef STORM_GENERATOR_STATELABELINGGENERATOR_H_
+#define STORM_GENERATOR_STATELABELINGGENERATOR_H_
+
+#include "src/models/sparse/StateLabeling.h"
+
+#include "src/storage/BitVectorHashMap.h"
+
+namespace storm {
+    namespace generator {
+        
+        template<typename StateType = uint32_t>
+        class StateLabelingGenerator {
+        public:
+            virtual storm::models::sparse::StateLabeling generate(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}) = 0;
+        };
+        
+    }
+}
+
+#endif /* STORM_GENERATOR_STATELABELINGGENERATOR_H_ */

src/generator/VariableInformation.cpp

@@ -0,0 +1,77 @@
+#include "src/generator/VariableInformation.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) {
+            // 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::prism::Program const& program) : totalBitOffset(0) {
+            for (auto const& booleanVariable : program.getGlobalBooleanVariables()) {
+                booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), booleanVariable.getInitialValueExpression().evaluateAsBool(), 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);
+                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);
+                    ++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);
+                    totalBitOffset += bitwidth;
+                    integerVariableToIndexMap[integerVariable.getExpressionVariable()] = integerVariables.size() - 1;
+                }
+            }
+        }
+        
+        uint_fast64_t VariableInformation::getTotalBitOffset(bool roundTo64Bit) const {
+            uint_fast64_t result = totalBitOffset;
+            if (roundTo64Bit) {
+                result = ((result >> 6) + 1) << 6;
+            }
+            return result;
+        }
+        
+        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/VariableInformation.h

@@ -0,0 +1,75 @@
+#ifndef STORM_GENERATOR_VARIABLEINFORMATION_H_
+#define STORM_GENERATOR_VARIABLEINFORMATION_H_
+
+#include <vector>
+#include <boost/container/flat_map.hpp>
+
+#include "src/storage/expressions/Variable.h"
+#include "src/storage/prism/Program.h"
+
+namespace storm {
+    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);
+            
+            // 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() = default;
+            VariableInformation(storm::prism::Program const& program);
+            uint_fast64_t getTotalBitOffset(bool roundTo64Bit = false) const;
+            
+            // 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 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;
+        };
+        
+    }
+}
+
+#endif /* STORM_GENERATOR_VARIABLEINFORMATION_H_ */

src/logic/BinaryBooleanStateFormula.cpp

@@ -2,10 +2,13 @@
 
 #include "src/logic/FormulaVisitor.h"
 
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidPropertyException.h"
+
 namespace storm {
     namespace logic {
         BinaryBooleanStateFormula::BinaryBooleanStateFormula(OperatorType operatorType, std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula) : BinaryStateFormula(leftSubformula, rightSubformula), operatorType(operatorType) {
-            // Intentionally left empty.
+            STORM_LOG_THROW(this->getLeftSubformula().hasQualitativeResult() && this->getRightSubformula().hasQualitativeResult(), storm::exceptions::InvalidPropertyException, "Boolean formula must have subformulas with qualitative result.");
         }
         
         bool BinaryBooleanStateFormula::isBinaryBooleanStateFormula() const {

src/logic/BinaryBooleanStateFormula.h

@@ -25,7 +25,7 @@ namespace storm {
             
             virtual bool isAnd() const;
             virtual bool isOr() const;
-            
+                        
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
             virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;

src/logic/BinaryPathFormula.cpp

@@ -32,5 +32,13 @@ namespace storm {
             this->getLeftSubformula().gatherReferencedRewardModels(referencedRewardModels);
             this->getRightSubformula().gatherReferencedRewardModels(referencedRewardModels);
         }
+        
+        bool BinaryPathFormula::hasQualitativeResult() const {
+            return false;
+        }
+        
+        bool BinaryPathFormula::hasQuantitativeResult() const {
+            return true;
+        }
     }
 }

src/logic/BinaryPathFormula.h

@@ -24,6 +24,9 @@ namespace storm {
             virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
             virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
             
+            virtual bool hasQualitativeResult() const override;
+            virtual bool hasQuantitativeResult() const override;
+            
         private:
             std::shared_ptr<Formula const> leftSubformula;
             std::shared_ptr<Formula const> rightSubformula;

src/logic/ConditionalFormula.cpp

@@ -49,6 +49,14 @@ namespace storm {
             this->getConditionFormula().gatherReferencedRewardModels(referencedRewardModels);
         }
         
+        bool ConditionalFormula::hasQualitativeResult() const {
+            return false;
+        }
+        
+        bool ConditionalFormula::hasQuantitativeResult() const {
+            return true;
+        }
+        
         std::ostream& ConditionalFormula::writeToStream(std::ostream& out) const {
             this->getSubformula().writeToStream(out);
             out << " || ";

src/logic/ConditionalFormula.h

@@ -32,6 +32,9 @@ namespace storm {
             virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
             virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
             
+            virtual bool hasQualitativeResult() const override;
+            virtual bool hasQuantitativeResult() const override;
+
         private:
             std::shared_ptr<Formula const> subformula;
             std::shared_ptr<Formula const> conditionFormula;

src/logic/EventuallyFormula.cpp

@@ -7,10 +7,14 @@
 namespace storm {
     namespace logic {
         EventuallyFormula::EventuallyFormula(std::shared_ptr<Formula const> const& subformula, FormulaContext context) : UnaryPathFormula(subformula), context(context) {
-            STORM_LOG_THROW(context == FormulaContext::Probability || context == FormulaContext::Reward || context == FormulaContext::ExpectedTime, storm::exceptions::InvalidPropertyException, "Invalid context for formula.");
+            STORM_LOG_THROW(context == FormulaContext::Probability || context == FormulaContext::Reward || context == FormulaContext::Time, storm::exceptions::InvalidPropertyException, "Invalid context for formula.");
         }
         
         bool EventuallyFormula::isEventuallyFormula() const {
+            return true;
+        }
+        
+        bool EventuallyFormula::isReachabilityProbabilityFormula() const {
             return context == FormulaContext::Probability;
         }
         
@@ -18,8 +22,8 @@ namespace storm {
             return context == FormulaContext::Reward;
         }
         
-        bool EventuallyFormula::isReachbilityExpectedTimeFormula() const {
-            return context == FormulaContext::ExpectedTime;
+        bool EventuallyFormula::isReachabilityTimeFormula() const {
+            return context == FormulaContext::Time;
         }
         
         bool EventuallyFormula::isProbabilityPathFormula() const {
@@ -30,8 +34,8 @@ namespace storm {
             return this->isReachabilityRewardFormula();
         }
         
-        bool EventuallyFormula::isExpectedTimePathFormula() const {
-            return this->isReachbilityExpectedTimeFormula();
+        bool EventuallyFormula::isTimePathFormula() const {
+            return this->isReachabilityTimeFormula();
         }
         
         boost::any EventuallyFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {

src/logic/EventuallyFormula.h

@@ -15,11 +15,12 @@ namespace storm {
             }
             
             virtual bool isEventuallyFormula() const override;
+            virtual bool isReachabilityProbabilityFormula() const override;
             virtual bool isReachabilityRewardFormula() const override;
-            virtual bool isReachbilityExpectedTimeFormula() const override;
+            virtual bool isReachabilityTimeFormula() const override;
             virtual bool isProbabilityPathFormula() const override;
             virtual bool isRewardPathFormula() const override;
-            virtual bool isExpectedTimePathFormula() const override;
+            virtual bool isTimePathFormula() const override;
             
             virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
 

src/logic/ExpectedTimeOperatorFormula.cpp

@@ -1,45 +0,0 @@
-#include "src/logic/ExpectedTimeOperatorFormula.h"
-
-#include "src/logic/FormulaVisitor.h"
-
-namespace storm {
-    namespace logic {
-        ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(std::shared_ptr<Formula const> const& subformula) : ExpectedTimeOperatorFormula(boost::none, boost::none, subformula) {
-            // Intentionally left empty.
-        }
-        
-        ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula) : ExpectedTimeOperatorFormula(boost::none, bound, subformula) {
-            // Intentionally left empty.
-        }
-        
-        ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula) : ExpectedTimeOperatorFormula(boost::optional<OptimizationDirection>(optimalityType), bound, subformula) {
-            // Intentionally left empty.
-        }
-        
-        ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr<Formula const> const& subformula) : ExpectedTimeOperatorFormula(boost::optional<OptimizationDirection>(optimalityType), boost::none, subformula) {
-            // Intentionally left empty.
-        }
-        
-        bool ExpectedTimeOperatorFormula::isExpectedTimeOperatorFormula() const {
-            return true;
-        }
-        
-        boost::any ExpectedTimeOperatorFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
-            return visitor.visit(*this, data);
-        }
-        
-        ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(boost::optional<OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula) : OperatorFormula(optimalityType, bound, subformula) {
-            // Intentionally left empty.
-        }
-        
-        std::shared_ptr<Formula> ExpectedTimeOperatorFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return std::make_shared<ExpectedTimeOperatorFormula>(this->optimalityType, this->bound, this->getSubformula().substitute(substitution));
-        }
-        
-        std::ostream& ExpectedTimeOperatorFormula::writeToStream(std::ostream& out) const {
-            out << "ET";
-            OperatorFormula::writeToStream(out);
-            return out;
-        }
-    }
-}

src/logic/ExpectedTimeOperatorFormula.h

@@ -1,33 +0,0 @@
-#ifndef STORM_LOGIC_EXPECTEDTIMEOPERATORFORMULA_H_
-#define STORM_LOGIC_EXPECTEDTIMEOPERATORFORMULA_H_
-
-#include "src/logic/OperatorFormula.h"
-
-#include "src/logic/FormulaVisitor.h"
-
-namespace storm {
-    namespace logic {
-        class ExpectedTimeOperatorFormula : public OperatorFormula {
-        public:
-            ExpectedTimeOperatorFormula(std::shared_ptr<Formula const> const& subformula);
-            ExpectedTimeOperatorFormula(Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula);
-            ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula);
-            ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr<Formula const> const& subformula);
-            ExpectedTimeOperatorFormula(boost::optional<OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula);
-            
-            virtual ~ExpectedTimeOperatorFormula() {
-                // Intentionally left empty.
-            }
-            
-            virtual bool isExpectedTimeOperatorFormula() const override;
-
-            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
-            
-            virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
-            
-            virtual std::ostream& writeToStream(std::ostream& out) const override;
-        };
-    }
-}
-
-#endif /* STORM_LOGIC_EXPECTEDTIMEOPERATORFORMULA_H_ */

src/logic/Formula.cpp

@@ -62,6 +62,10 @@ namespace storm {
             return false;
         }
         
+        bool Formula::isReachabilityProbabilityFormula() const {
+            return false;
+        }
+        
         bool Formula::isGloballyFormula() const {
             return false;
         }
@@ -90,7 +94,7 @@ namespace storm {
             return false;
         }
         
-        bool Formula::isExpectedTimePathFormula() const {
+        bool Formula::isTimePathFormula() const {
             return false;
         }
         
@@ -102,7 +106,7 @@ namespace storm {
             return false;
         }
         
-        bool Formula::isExpectedTimeOperatorFormula() const {
+        bool Formula::isTimeOperatorFormula() const {
             return false;
         }
         
@@ -122,7 +126,7 @@ namespace storm {
             return false;
         }
         
-        bool Formula::isReachbilityExpectedTimeFormula() const {
+        bool Formula::isReachabilityTimeFormula() const {
             return false;
         }
         
@@ -138,6 +142,14 @@ namespace storm {
             return false;
         }
         
+        bool Formula::hasQualitativeResult() const {
+            return true;
+        }
+        
+        bool Formula::hasQuantitativeResult() const {
+            return false;
+        }
+        
         bool Formula::isInFragment(FragmentSpecification const& fragment) const {
             FragmentChecker checker;
             return checker.conformsToSpecification(*this, fragment);
@@ -264,6 +276,22 @@ namespace storm {
             return dynamic_cast<EventuallyFormula const&>(*this);
         }
         
+        EventuallyFormula& Formula::asReachabilityProbabilityFormula() {
+            return dynamic_cast<EventuallyFormula&>(*this);
+        }
+        
+        EventuallyFormula const& Formula::asReachabilityProbabilityFormula() const {
+            return dynamic_cast<EventuallyFormula const&>(*this);
+        }
+        
+        EventuallyFormula& Formula::asReachabilityTimeFormula() {
+            return dynamic_cast<EventuallyFormula&>(*this);
+        }
+
+        EventuallyFormula const& Formula::asReachabilityTimeFormula() const {
+            return dynamic_cast<EventuallyFormula const&>(*this);
+        }
+        
         GloballyFormula& Formula::asGloballyFormula() {
             return dynamic_cast<GloballyFormula&>(*this);
         }
@@ -304,12 +332,12 @@ namespace storm {
             return dynamic_cast<LongRunAverageOperatorFormula const&>(*this);
         }
         
-        ExpectedTimeOperatorFormula& Formula::asExpectedTimeOperatorFormula() {
-            return dynamic_cast<ExpectedTimeOperatorFormula&>(*this);
+        TimeOperatorFormula& Formula::asTimeOperatorFormula() {
+            return dynamic_cast<TimeOperatorFormula&>(*this);
         }
         
-        ExpectedTimeOperatorFormula const& Formula::asExpectedTimeOperatorFormula() const {
-            return dynamic_cast<ExpectedTimeOperatorFormula const&>(*this);
+        TimeOperatorFormula const& Formula::asTimeOperatorFormula() const {
+            return dynamic_cast<TimeOperatorFormula const&>(*this);
         }
         
         CumulativeRewardFormula& Formula::asCumulativeRewardFormula() {

src/logic/Formula.h

@@ -42,7 +42,7 @@ namespace storm {
             
             virtual bool isProbabilityPathFormula() const;
             virtual bool isRewardPathFormula() const;
-            virtual bool isExpectedTimePathFormula() const;
+            virtual bool isTimePathFormula() const;
 
             virtual bool isBinaryBooleanStateFormula() const;
             virtual bool isUnaryBooleanStateFormula() const;
@@ -50,7 +50,7 @@ namespace storm {
             // Operator formulas.
             virtual bool isOperatorFormula() const;
             virtual bool isLongRunAverageOperatorFormula() const;
-            virtual bool isExpectedTimeOperatorFormula() const;
+            virtual bool isTimeOperatorFormula() const;
             virtual bool isProbabilityOperatorFormula() const;
             virtual bool isRewardOperatorFormula() const;
 
@@ -65,8 +65,9 @@ namespace storm {
             virtual bool isNextFormula() const;
             virtual bool isUntilFormula() const;
             virtual bool isBoundedUntilFormula() const;
-            virtual bool isEventuallyFormula() const;
             virtual bool isGloballyFormula() const;
+            virtual bool isEventuallyFormula() const;
+            virtual bool isReachabilityProbabilityFormula() const;
 
             // Reward formulas.
             virtual bool isCumulativeRewardFormula() const;
@@ -75,7 +76,7 @@ namespace storm {
             virtual bool isLongRunAverageRewardFormula() const;
             
             // Expected time formulas.
-            virtual bool isReachbilityExpectedTimeFormula() const;
+            virtual bool isReachabilityTimeFormula() const;
             
             // Type checks for abstract intermediate classes.
             virtual bool isBinaryPathFormula() const;
@@ -83,6 +84,10 @@ namespace storm {
             virtual bool isUnaryPathFormula() const;
             virtual bool isUnaryStateFormula() const;
 
+            // Accessors for the return type of a formula.
+            virtual bool hasQualitativeResult() const;
+            virtual bool hasQuantitativeResult() const;
+            
             bool isInFragment(FragmentSpecification const& fragment) const;
             FormulaInformation info() const;
             
@@ -126,8 +131,14 @@ namespace storm {
             EventuallyFormula& asEventuallyFormula();
             EventuallyFormula const& asEventuallyFormula() const;
             
+            EventuallyFormula& asReachabilityProbabilityFormula();
+            EventuallyFormula const& asReachabilityProbabilityFormula() const;
+            
             EventuallyFormula& asReachabilityRewardFormula();
             EventuallyFormula const& asReachabilityRewardFormula() const;
+
+            EventuallyFormula& asReachabilityTimeFormula();
+            EventuallyFormula const& asReachabilityTimeFormula() const;
             
             GloballyFormula& asGloballyFormula();
             GloballyFormula const& asGloballyFormula() const;
@@ -147,8 +158,8 @@ namespace storm {
             LongRunAverageOperatorFormula& asLongRunAverageOperatorFormula();
             LongRunAverageOperatorFormula const& asLongRunAverageOperatorFormula() const;
 
-            ExpectedTimeOperatorFormula& asExpectedTimeOperatorFormula();
-            ExpectedTimeOperatorFormula const& asExpectedTimeOperatorFormula() const;
+            TimeOperatorFormula& asTimeOperatorFormula();
+            TimeOperatorFormula const& asTimeOperatorFormula() const;
             
             CumulativeRewardFormula& asCumulativeRewardFormula();
             CumulativeRewardFormula const& asCumulativeRewardFormula() const;

src/logic/FormulaContext.h

@@ -4,7 +4,7 @@
 namespace storm {
     namespace logic {
         
-        enum class FormulaContext { Undefined, Probability, Reward, LongRunAverage, ExpectedTime };
+        enum class FormulaContext { Undefined, Probability, Reward, LongRunAverage, Time };
         
     }
 }

src/logic/FormulaInformationVisitor.cpp

@@ -41,7 +41,7 @@ namespace storm {
             return f.getSubformula().accept(*this);
         }
         
-        boost::any FormulaInformationVisitor::visit(ExpectedTimeOperatorFormula const& f, boost::any const& data) const {
+        boost::any FormulaInformationVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const {
             return f.getSubformula().accept(*this);
         }
         

src/logic/FormulaInformationVisitor.h

@@ -19,7 +19,7 @@ namespace storm {
             virtual boost::any visit(ConditionalFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override;
-            virtual boost::any visit(ExpectedTimeOperatorFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override;

src/logic/FormulaVisitor.h

@@ -18,7 +18,7 @@ namespace storm {
             virtual boost::any visit(ConditionalFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const = 0;
-            virtual boost::any visit(ExpectedTimeOperatorFormula const& f, boost::any const& data) const = 0;
+            virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const = 0;

src/logic/Formulas.h

@@ -18,7 +18,7 @@
 #include "src/logic/RewardOperatorFormula.h"
 #include "src/logic/StateFormula.h"
 #include "src/logic/LongRunAverageOperatorFormula.h"
-#include "src/logic/ExpectedTimeOperatorFormula.h"
+#include "src/logic/TimeOperatorFormula.h"
 #include "src/logic/UnaryBooleanStateFormula.h"
 #include "src/logic/UnaryPathFormula.h"
 #include "src/logic/UnaryStateFormula.h"

src/logic/FormulasForwardDeclarations.h

@@ -15,7 +15,7 @@ namespace storm {
         class ConditionalFormula;
         class CumulativeRewardFormula;
         class EventuallyFormula;
-        class ExpectedTimeOperatorFormula;
+        class TimeOperatorFormula;
         class GloballyFormula;
         class InstantaneousRewardFormula;
         class LongRunAverageOperatorFormula;

src/logic/FragmentChecker.cpp

@@ -73,7 +73,7 @@ namespace storm {
             }
             if (inherited.getSpecification().areOnlyEventuallyFormuluasInConditionalFormulasAllowed()) {
                 if (f.isConditionalProbabilityFormula()) {
-                    result = result && f.getSubformula().isEventuallyFormula() && f.getConditionFormula().isEventuallyFormula();
+                    result = result && f.getSubformula().isReachabilityProbabilityFormula() && f.getConditionFormula().isReachabilityProbabilityFormula();
                 } else if (f.isConditionalRewardFormula()) {
                     result = result && f.getSubformula().isReachabilityRewardFormula() && f.getConditionFormula().isEventuallyFormula();
                 }
@@ -91,26 +91,29 @@ namespace storm {
         boost::any FragmentChecker::visit(EventuallyFormula const& f, boost::any const& data) const {
             InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
             bool result = true;
-            if (f.isEventuallyFormula()) {
-                result = inherited.getSpecification().areEventuallyFormulasAllowed();
+            if (f.isReachabilityProbabilityFormula()) {
+                result = inherited.getSpecification().areReachabilityProbabilityFormulasAllowed();
                 if (!inherited.getSpecification().areNestedPathFormulasAllowed()) {
                     result = result && !f.getSubformula().isPathFormula();
                 }
             } else if (f.isReachabilityRewardFormula()) {
                 result = result && inherited.getSpecification().areReachabilityRewardFormulasAllowed();
                 result = result && f.getSubformula().isStateFormula();
-            } else if (f.isReachbilityExpectedTimeFormula()) {
-                result = result && inherited.getSpecification().areReachbilityExpectedTimeFormulasAllowed();
+            } else if (f.isReachabilityTimeFormula()) {
+                result = result && inherited.getSpecification().areReachbilityTimeFormulasAllowed();
                 result = result && f.getSubformula().isStateFormula();
             }
             result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, data));
             return result;
         }
         
-        boost::any FragmentChecker::visit(ExpectedTimeOperatorFormula const& f, boost::any const& data) const {
+        boost::any FragmentChecker::visit(TimeOperatorFormula const& f, boost::any const& data) const {
             InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
-            bool result = inherited.getSpecification().areExpectedTimeOperatorsAllowed();
-            result = result && f.getSubformula().isExpectedTimePathFormula();
+            bool result = inherited.getSpecification().areTimeOperatorsAllowed();
+            result = result && (!f.hasQualitativeResult() || inherited.getSpecification().areQualitativeOperatorResultsAllowed());
+            result = result && (!f.hasQuantitativeResult() || inherited.getSpecification().areQuantitativeOperatorResultsAllowed());
+            result = result && f.getSubformula().isTimePathFormula();
+            result = result && (inherited.getSpecification().isVarianceMeasureTypeAllowed() || f.getMeasureType() == RewardMeasureType::Expectation);
             if (!inherited.getSpecification().areNestedOperatorsAllowed()) {
                 result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, InheritedInformation(inherited.getSpecification().copy().setOperatorsAllowed(false))));
             } else {
@@ -164,6 +167,8 @@ namespace storm {
         boost::any FragmentChecker::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const {
             InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
             bool result = inherited.getSpecification().areProbabilityOperatorsAllowed();
+            result = result && (!f.hasQualitativeResult() || inherited.getSpecification().areQualitativeOperatorResultsAllowed());
+            result = result && (!f.hasQuantitativeResult() || inherited.getSpecification().areQuantitativeOperatorResultsAllowed());
             result = result && (f.getSubformula().isProbabilityPathFormula() || f.getSubformula().isConditionalProbabilityFormula());
             if (!inherited.getSpecification().areNestedOperatorsAllowed()) {
                 result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, InheritedInformation(inherited.getSpecification().copy().setOperatorsAllowed(false))));
@@ -176,7 +181,10 @@ namespace storm {
         boost::any FragmentChecker::visit(RewardOperatorFormula const& f, boost::any const& data) const {
             InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
             bool result = inherited.getSpecification().areRewardOperatorsAllowed();
+            result = result && (!f.hasQualitativeResult() || inherited.getSpecification().areQualitativeOperatorResultsAllowed());
+            result = result && (!f.hasQuantitativeResult() || inherited.getSpecification().areQuantitativeOperatorResultsAllowed());
             result = result && (f.getSubformula().isRewardPathFormula() || f.getSubformula().isConditionalRewardFormula());
+            result = result && (inherited.getSpecification().isVarianceMeasureTypeAllowed() || f.getMeasureType() == RewardMeasureType::Expectation);
             if (!inherited.getSpecification().areNestedOperatorsAllowed()) {
                 result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, InheritedInformation(inherited.getSpecification().copy().setOperatorsAllowed(false))));
             } else {

src/logic/FragmentChecker.h

@@ -20,7 +20,7 @@ namespace storm {
             virtual boost::any visit(ConditionalFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override;
-            virtual boost::any visit(ExpectedTimeOperatorFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override;

src/logic/FragmentSpecification.cpp

@@ -22,7 +22,7 @@ namespace storm {
             
             pctl.setProbabilityOperatorsAllowed(true);
             pctl.setGloballyFormulasAllowed(true);
-            pctl.setEventuallyFormulasAllowed(true);
+            pctl.setReachabilityProbabilityFormulasAllowed(true);
             pctl.setNextFormulasAllowed(true);
             pctl.setUntilFormulasAllowed(true);
             pctl.setBoundedUntilFormulasAllowed(true);
@@ -70,7 +70,7 @@ namespace storm {
             longRunAverageOperator = false;
             
             globallyFormula = false;
-            eventuallyFormula = false;
+            reachabilityProbabilityFormula = false;
             nextFormula = false;
             untilFormula = false;
             boundedUntilFormula = false;
@@ -89,13 +89,17 @@ namespace storm {
             conditionalProbabilityFormula = false;
             conditionalRewardFormula = false;
             
-            reachabilityExpectedTimeFormula = false;
+            reachabilityTimeFormula = false;
             
             nestedOperators = true;
             nestedPathFormulas = false;
             onlyEventuallyFormuluasInConditionalFormulas = true;
             stepBoundedUntilFormulas = false;
             timeBoundedUntilFormulas = false;
+            varianceAsMeasureType = false;
+            
+            qualitativeOperatorResults = true;
+            quantitativeOperatorResults = true;
         }
         
         FragmentSpecification FragmentSpecification::copy() const {
@@ -120,11 +124,11 @@ namespace storm {
             return *this;
         }
         
-        bool FragmentSpecification::areExpectedTimeOperatorsAllowed() const {
+        bool FragmentSpecification::areTimeOperatorsAllowed() const {
             return expectedTimeOperator;
         }
         
-        FragmentSpecification& FragmentSpecification::setExpectedTimeOperatorsAllowed(bool newValue) {
+        FragmentSpecification& FragmentSpecification::setTimeOperatorsAllowed(bool newValue) {
             this->expectedTimeOperator = newValue;
             return *this;
         }
@@ -147,12 +151,12 @@ namespace storm {
             return *this;
         }
         
-        bool FragmentSpecification::areEventuallyFormulasAllowed() const {
-            return eventuallyFormula;
+        bool FragmentSpecification::areReachabilityProbabilityFormulasAllowed() const {
+            return reachabilityProbabilityFormula;
         }
         
-        FragmentSpecification& FragmentSpecification::setEventuallyFormulasAllowed(bool newValue) {
-            this->eventuallyFormula = newValue;
+        FragmentSpecification& FragmentSpecification::setReachabilityProbabilityFormulasAllowed(bool newValue) {
+            this->reachabilityProbabilityFormula = newValue;
             return *this;
         }
         
@@ -282,12 +286,12 @@ namespace storm {
             return *this;
         }
         
-        bool FragmentSpecification::areReachbilityExpectedTimeFormulasAllowed() const {
-            return reachabilityExpectedTimeFormula;
+        bool FragmentSpecification::areReachbilityTimeFormulasAllowed() const {
+            return reachabilityTimeFormula;
         }
             
-        FragmentSpecification& FragmentSpecification::setReachbilityExpectedTimeFormulasAllowed(bool newValue) {
-            this->reachabilityExpectedTimeFormula = newValue;
+        FragmentSpecification& FragmentSpecification::setReachbilityTimeFormulasAllowed(bool newValue) {
+            this->reachabilityTimeFormula = newValue;
             return *this;
         }
         
@@ -340,13 +344,13 @@ namespace storm {
             this->setProbabilityOperatorsAllowed(newValue);
             this->setRewardOperatorsAllowed(newValue);
             this->setLongRunAverageOperatorsAllowed(newValue);
-            this->setExpectedTimeOperatorsAllowed(newValue);
+            this->setTimeOperatorsAllowed(newValue);
             return *this;
         }
         
-        FragmentSpecification& FragmentSpecification::setExpectedTimeAllowed(bool newValue) {
-            this->setExpectedTimeOperatorsAllowed(newValue);
-            this->setReachbilityExpectedTimeFormulasAllowed(newValue);
+        FragmentSpecification& FragmentSpecification::setTimeAllowed(bool newValue) {
+            this->setTimeOperatorsAllowed(newValue);
+            this->setReachbilityTimeFormulasAllowed(newValue);
             return *this;
         }
         
@@ -355,5 +359,33 @@ namespace storm {
             return *this;
         }
         
+        bool FragmentSpecification::isVarianceMeasureTypeAllowed() const {
+            return varianceAsMeasureType;
+        }
+        
+        FragmentSpecification& FragmentSpecification::setVarianceMeasureTypeAllowed(bool newValue) {
+            this->varianceAsMeasureType = newValue;
+            return *this;
+        }
+     
+        bool FragmentSpecification::areQuantitativeOperatorResultsAllowed() const {
+            return this->quantitativeOperatorResults;
+        }
+        
+        FragmentSpecification& FragmentSpecification::setQuantitativeOperatorResultsAllowed(bool newValue) {
+            this->quantitativeOperatorResults = newValue;
+            return *this;
+        }
+        
+        bool FragmentSpecification::areQualitativeOperatorResultsAllowed() const {
+            return this->qualitativeOperatorResults;
+        }
+        
+        FragmentSpecification& FragmentSpecification::setQualitativeOperatorResultsAllowed(bool newValue) {
+            this->qualitativeOperatorResults = newValue;
+            return *this;
+        }
+
+        
     }
 }

src/logic/FragmentSpecification.h

@@ -19,8 +19,8 @@ namespace storm {
             bool areRewardOperatorsAllowed() const;
             FragmentSpecification& setRewardOperatorsAllowed(bool newValue);
             
-            bool areExpectedTimeOperatorsAllowed() const;
-            FragmentSpecification& setExpectedTimeOperatorsAllowed(bool newValue);
+            bool areTimeOperatorsAllowed() const;
+            FragmentSpecification& setTimeOperatorsAllowed(bool newValue);
 
             bool areLongRunAverageOperatorsAllowed() const;
             FragmentSpecification& setLongRunAverageOperatorsAllowed(bool newValue);
@@ -28,8 +28,8 @@ namespace storm {
             bool areGloballyFormulasAllowed() const;
             FragmentSpecification& setGloballyFormulasAllowed(bool newValue);
 
-            bool areEventuallyFormulasAllowed() const;
-            FragmentSpecification& setEventuallyFormulasAllowed(bool newValue);
+            bool areReachabilityProbabilityFormulasAllowed() const;
+            FragmentSpecification& setReachabilityProbabilityFormulasAllowed(bool newValue);
 
             bool areNextFormulasAllowed() const;
             FragmentSpecification& setNextFormulasAllowed(bool newValue);
@@ -73,8 +73,8 @@ namespace storm {
             bool areConditionalRewardFormulasFormulasAllowed() const;
             FragmentSpecification& setConditionalRewardFormulasAllowed(bool newValue);
 
-            bool areReachbilityExpectedTimeFormulasAllowed() const;
-            FragmentSpecification& setReachbilityExpectedTimeFormulasAllowed(bool newValue);
+            bool areReachbilityTimeFormulasAllowed() const;
+            FragmentSpecification& setReachbilityTimeFormulasAllowed(bool newValue);
 
             bool areNestedOperatorsAllowed() const;
             FragmentSpecification& setNestedOperatorsAllowed(bool newValue);
@@ -91,8 +91,17 @@ namespace storm {
             bool areTimeBoundedUntilFormulasAllowed() const;
             FragmentSpecification& setTimeBoundedUntilFormulasAllowed(bool newValue);
             
+            bool isVarianceMeasureTypeAllowed() const;
+            FragmentSpecification& setVarianceMeasureTypeAllowed(bool newValue);
+            
+            bool areQuantitativeOperatorResultsAllowed() const;
+            FragmentSpecification& setQuantitativeOperatorResultsAllowed(bool newValue);
+
+            bool areQualitativeOperatorResultsAllowed() const;
+            FragmentSpecification& setQualitativeOperatorResultsAllowed(bool newValue);
+            
             FragmentSpecification& setOperatorsAllowed(bool newValue);
-            FragmentSpecification& setExpectedTimeAllowed(bool newValue);
+            FragmentSpecification& setTimeAllowed(bool newValue);
             FragmentSpecification& setLongRunAverageProbabilitiesAllowed(bool newValue);
             
         private:
@@ -103,7 +112,7 @@ namespace storm {
             bool longRunAverageOperator;
             
             bool globallyFormula;
-            bool eventuallyFormula;
+            bool reachabilityProbabilityFormula;
             bool nextFormula;
             bool untilFormula;
             bool boundedUntilFormula;
@@ -122,7 +131,7 @@ namespace storm {
             bool conditionalProbabilityFormula;
             bool conditionalRewardFormula;
             
-            bool reachabilityExpectedTimeFormula;
+            bool reachabilityTimeFormula;
             
             // Members that indicate certain restrictions.
             bool nestedOperators;
@@ -130,6 +139,9 @@ namespace storm {
             bool onlyEventuallyFormuluasInConditionalFormulas;
             bool stepBoundedUntilFormulas;
             bool timeBoundedUntilFormulas;
+            bool varianceAsMeasureType;
+            bool quantitativeOperatorResults;
+            bool qualitativeOperatorResults;
         };
         
         // Propositional.

src/logic/LongRunAverageOperatorFormula.cpp

@@ -2,24 +2,15 @@
 
 #include "src/logic/FormulaVisitor.h"
 
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidPropertyException.h"
+
 namespace storm {
     namespace logic {
-        LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(std::shared_ptr<Formula const> const& subformula) : LongRunAverageOperatorFormula(boost::none, boost::none, subformula) {
-            // Intentionally left empty.
-        }
-        
-        LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula) : LongRunAverageOperatorFormula(boost::none, bound, subformula) {
-            // Intentionally left empty.
-        }
-        
-        LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(OptimizationDirection optimalityType, Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula) : LongRunAverageOperatorFormula(boost::optional<OptimizationDirection>(optimalityType), bound, subformula) {
+        LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(std::shared_ptr<Formula const> const& subformula, OperatorInformation const& operatorInformation) : OperatorFormula(subformula, operatorInformation) {
             // Intentionally left empty.
         }
         
-        LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr<Formula const> const& subformula) : LongRunAverageOperatorFormula(boost::optional<OptimizationDirection>(optimalityType), boost::none, subformula) {
-            // Intentionally left empty.
-        }
-                
         bool LongRunAverageOperatorFormula::isLongRunAverageOperatorFormula() const {
             return true;
         }
@@ -28,12 +19,8 @@ namespace storm {
             return visitor.visit(*this, data);
         }
         
-        LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(boost::optional<OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula) : OperatorFormula(optimalityType, bound, subformula) {
-            // Intentionally left empty.
-        }
-        
         std::shared_ptr<Formula> LongRunAverageOperatorFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return std::make_shared<LongRunAverageOperatorFormula>(this->optimalityType, this->bound, this->getSubformula().substitute(substitution));
+            return std::make_shared<LongRunAverageOperatorFormula>(this->getSubformula().substitute(substitution), this->operatorInformation);
         }
         
         std::ostream& LongRunAverageOperatorFormula::writeToStream(std::ostream& out) const {

src/logic/LongRunAverageOperatorFormula.h

@@ -7,11 +7,7 @@ namespace storm {
     namespace logic {
         class LongRunAverageOperatorFormula : public OperatorFormula {
         public:
-            LongRunAverageOperatorFormula(std::shared_ptr<Formula const> const& subformula);
-            LongRunAverageOperatorFormula(Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula);
-            LongRunAverageOperatorFormula(OptimizationDirection optimalityType, Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula);
-            LongRunAverageOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr<Formula const> const& subformula);
-            LongRunAverageOperatorFormula(boost::optional<OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula);
+            LongRunAverageOperatorFormula(std::shared_ptr<Formula const> const& subformula, OperatorInformation const& operatorInformation = OperatorInformation());
             
             virtual ~LongRunAverageOperatorFormula() {
                 // Intentionally left empty.

src/logic/OperatorFormula.cpp

@@ -2,50 +2,62 @@
 
 namespace storm {
     namespace logic {
-        OperatorFormula::OperatorFormula(boost::optional<storm::solver::OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula) : UnaryStateFormula(subformula), bound(bound), optimalityType(optimalityType) {
+        OperatorInformation::OperatorInformation(boost::optional<storm::solver::OptimizationDirection> const& optimizationDirection, boost::optional<Bound<double>> const& bound) : optimalityType(optimizationDirection), bound(bound) {
+            // Intentionally left empty.
+        }
+        
+        OperatorFormula::OperatorFormula(std::shared_ptr<Formula const> const& subformula, OperatorInformation const& operatorInformation) : UnaryStateFormula(subformula), operatorInformation(operatorInformation) {
             // Intentionally left empty.
         }
         
         bool OperatorFormula::hasBound() const {
-            return static_cast<bool>(bound);
+            return static_cast<bool>(operatorInformation.bound);
         }
         
         ComparisonType OperatorFormula::getComparisonType() const {
-            return bound.get().comparisonType;
+            return operatorInformation.bound.get().comparisonType;
         }
         
         void OperatorFormula::setComparisonType(ComparisonType newComparisonType) {
-            bound.get().comparisonType = newComparisonType;
+            operatorInformation.bound.get().comparisonType = newComparisonType;
         }
         
         double OperatorFormula::getThreshold() const {
-            return bound.get().threshold;
+            return operatorInformation.bound.get().threshold;
         }
         
         void OperatorFormula::setThreshold(double newThreshold) {
-            bound.get().threshold = newThreshold;
+            operatorInformation.bound.get().threshold = newThreshold;
         }
         
         Bound<double> const& OperatorFormula::getBound() const {
-            return bound.get();
+            return operatorInformation.bound.get();
         }
         
         void OperatorFormula::setBound(Bound<double> const& newBound) {
-            bound = newBound;
+            operatorInformation.bound = newBound;
         }
         
         bool OperatorFormula::hasOptimalityType() const {
-            return static_cast<bool>(optimalityType);
+            return static_cast<bool>(operatorInformation.optimalityType);
         }
         
         OptimizationDirection const& OperatorFormula::getOptimalityType() const {
-            return optimalityType.get();
+            return operatorInformation.optimalityType.get();
         }
         
         bool OperatorFormula::isOperatorFormula() const {
             return true;
         }
         
+        bool OperatorFormula::hasQualitativeResult() const {
+            return this->hasBound();
+        }
+        
+        bool OperatorFormula::hasQuantitativeResult() const {
+            return !this->hasBound();
+        }
+        
         std::ostream& OperatorFormula::writeToStream(std::ostream& out) const {
             if (hasOptimalityType()) {
                 out << (getOptimalityType() == OptimizationDirection::Minimize ? "min" : "max");

src/logic/OperatorFormula.h

@@ -8,15 +8,23 @@
 #include "src/solver/OptimizationDirection.h"
 
 namespace storm {
-    namespace logic {
+    namespace logic {        
+        struct OperatorInformation {
+            OperatorInformation(boost::optional<storm::solver::OptimizationDirection> const& optimizationDirection = boost::none, boost::optional<Bound<double>> const& bound = boost::none);
+
+            boost::optional<storm::solver::OptimizationDirection> optimalityType;
+            boost::optional<Bound<double>> bound;
+        };
+        
         class OperatorFormula : public UnaryStateFormula {
         public:
-            OperatorFormula(boost::optional<storm::solver::OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula);
+            OperatorFormula(std::shared_ptr<Formula const> const& subformula, OperatorInformation const& operatorInformation = OperatorInformation());
             
             virtual ~OperatorFormula() {
                 // Intentionally left empty.
             }
-            
+
+            // Bound-related accessors.
             bool hasBound() const;
             ComparisonType getComparisonType() const;
             void setComparisonType(ComparisonType newComparisonType);
@@ -24,16 +32,19 @@ namespace storm {
             void setThreshold(double newThreshold);
             Bound<double> const& getBound() const;
             void setBound(Bound<double> const& newBound);
+            
+            // Optimality-type-related accessors.
             bool hasOptimalityType() const;
             storm::solver::OptimizationDirection const& getOptimalityType() const;
             virtual bool isOperatorFormula() const override;
+                        
+            virtual bool hasQualitativeResult() const override;
+            virtual bool hasQuantitativeResult() const override;
             
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
         protected:
-            std::string operatorSymbol;
-            boost::optional<Bound<double>> bound;
-            boost::optional<storm::solver::OptimizationDirection> optimalityType;
+            OperatorInformation operatorInformation;
         };
     }
 }

src/logic/ProbabilityOperatorFormula.cpp

@@ -2,21 +2,12 @@
 
 #include "src/logic/FormulaVisitor.h"
 
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidPropertyException.h"
+
 namespace storm {
     namespace logic {
-        ProbabilityOperatorFormula::ProbabilityOperatorFormula(std::shared_ptr<Formula const> const& subformula) : ProbabilityOperatorFormula(boost::none, boost::none, subformula) {
-            // Intentionally left empty.
-        }
-        
-        ProbabilityOperatorFormula::ProbabilityOperatorFormula(Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula) : ProbabilityOperatorFormula(boost::none, bound, subformula) {
-            // Intentionally left empty.
-        }
-        
-        ProbabilityOperatorFormula::ProbabilityOperatorFormula(OptimizationDirection optimalityType, Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula) : ProbabilityOperatorFormula(boost::optional<OptimizationDirection>(optimalityType), bound, subformula) {
-            // Intentionally left empty.
-        }
-        
-        ProbabilityOperatorFormula::ProbabilityOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr<Formula const> const& subformula) : ProbabilityOperatorFormula(boost::optional<OptimizationDirection>(optimalityType), boost::none, subformula) {
+        ProbabilityOperatorFormula::ProbabilityOperatorFormula(std::shared_ptr<Formula const> const& subformula, OperatorInformation const& operatorInformation) : OperatorFormula(subformula, operatorInformation) {
             // Intentionally left empty.
         }
         
@@ -27,13 +18,9 @@ namespace storm {
         boost::any ProbabilityOperatorFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
             return visitor.visit(*this, data);
         }
-                
-        ProbabilityOperatorFormula::ProbabilityOperatorFormula(boost::optional<OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula) : OperatorFormula(optimalityType, bound, subformula) {
-            // Intentionally left empty.
-        }
         
         std::shared_ptr<Formula> ProbabilityOperatorFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return std::make_shared<ProbabilityOperatorFormula>(this->optimalityType, this->bound, this->getSubformula().substitute(substitution));
+            return std::make_shared<ProbabilityOperatorFormula>(this->getSubformula().substitute(substitution), this->operatorInformation);
         }
         
         std::ostream& ProbabilityOperatorFormula::writeToStream(std::ostream& out) const {

src/logic/ProbabilityOperatorFormula.h

@@ -7,11 +7,7 @@ namespace storm {
     namespace logic {
         class ProbabilityOperatorFormula : public OperatorFormula {
         public:
-            ProbabilityOperatorFormula(std::shared_ptr<Formula const> const& subformula);
-            ProbabilityOperatorFormula(Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula);
-            ProbabilityOperatorFormula(OptimizationDirection optimalityType, Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula);
-            ProbabilityOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr<Formula const> const& subformula);
-            ProbabilityOperatorFormula(boost::optional<OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula);
+            ProbabilityOperatorFormula(std::shared_ptr<Formula const> const& subformula, OperatorInformation const& operatorInformation = OperatorInformation());
 
             virtual ~ProbabilityOperatorFormula() {
                 // Intentionally left empty.

src/logic/RewardMeasureType.cpp

@@ -0,0 +1,19 @@
+#include "src/logic/RewardMeasureType.h"
+
+namespace storm {
+    namespace logic {
+        
+        std::ostream& operator<<(std::ostream& out, RewardMeasureType const& type) {
+            switch (type) {
+                case RewardMeasureType::Expectation:
+                    out << "exp";
+                    break;
+                case RewardMeasureType::Variance:
+                    out << "var";
+                    break;
+            }
+            return out;
+        }
+        
+    }
+}

src/logic/RewardMeasureType.h

@@ -0,0 +1,16 @@
+#ifndef STORM_LOGIC_REWARDMEASURETYPE_H_
+#define STORM_LOGIC_REWARDMEASURETYPE_H_
+
+#include <iostream>
+
+namespace storm {
+    namespace logic {
+        
+        enum class RewardMeasureType { Expectation, Variance };
+
+        std::ostream& operator<<(std::ostream& out, RewardMeasureType const& type);
+
+    }
+}
+
+#endif /* STORM_LOGIC_REWARDMEASURETYPE_H_ */

src/logic/RewardOperatorFormula.cpp

@@ -2,21 +2,12 @@
 
 #include "src/logic/FormulaVisitor.h"
 
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidPropertyException.h"
+
 namespace storm {
     namespace logic {
-        RewardOperatorFormula::RewardOperatorFormula(boost::optional<std::string> const& rewardModelName, std::shared_ptr<Formula const> const& subformula) : RewardOperatorFormula(rewardModelName, boost::none, boost::none, subformula) {
-            // Intentionally left empty.
-        }
-        
-        RewardOperatorFormula::RewardOperatorFormula(boost::optional<std::string> const& rewardModelName, Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula) : RewardOperatorFormula(rewardModelName, boost::none, bound, subformula) {
-            // Intentionally left empty.
-        }
-        
-        RewardOperatorFormula::RewardOperatorFormula(boost::optional<std::string> const& rewardModelName, OptimizationDirection optimalityType, Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula) : RewardOperatorFormula(rewardModelName, boost::optional<OptimizationDirection>(optimalityType), bound, subformula) {
-            // Intentionally left empty.
-        }
-        
-        RewardOperatorFormula::RewardOperatorFormula(boost::optional<std::string> const& rewardModelName, OptimizationDirection optimalityType, std::shared_ptr<Formula const> const& subformula) : RewardOperatorFormula(rewardModelName, boost::optional<OptimizationDirection>(optimalityType), boost::none, subformula) {
+        RewardOperatorFormula::RewardOperatorFormula(std::shared_ptr<Formula const> const& subformula, boost::optional<std::string> const& rewardModelName, OperatorInformation const& operatorInformation, RewardMeasureType rewardMeasureType) : OperatorFormula(subformula, operatorInformation), rewardModelName(rewardModelName), rewardMeasureType(rewardMeasureType) {
             // Intentionally left empty.
         }
         
@@ -49,16 +40,17 @@ namespace storm {
             this->getSubformula().gatherReferencedRewardModels(referencedRewardModels);
         }
         
-        RewardOperatorFormula::RewardOperatorFormula(boost::optional<std::string> const& rewardModelName, boost::optional<OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula) : OperatorFormula(optimalityType, bound, subformula), rewardModelName(rewardModelName) {
-            // Intentionally left empty.
+        std::shared_ptr<Formula> RewardOperatorFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
+            return std::make_shared<RewardOperatorFormula>(this->getSubformula().substitute(substitution), this->rewardModelName, this->operatorInformation, this->rewardMeasureType);
         }
         
-        std::shared_ptr<Formula> RewardOperatorFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return std::make_shared<RewardOperatorFormula>(this->rewardModelName, this->optimalityType, this->bound, this->getSubformula().substitute(substitution));
+        RewardMeasureType RewardOperatorFormula::getMeasureType() const {
+            return rewardMeasureType;
         }
         
         std::ostream& RewardOperatorFormula::writeToStream(std::ostream& out) const {
             out << "R";
+            out << "[" << rewardMeasureType << "]";
             if (this->hasRewardModelName()) {
                 out << "{\"" << this->getRewardModelName() << "\"}";
             }

src/logic/RewardOperatorFormula.h

@@ -1,18 +1,14 @@
 #ifndef STORM_LOGIC_REWARDOPERATORFORMULA_H_
 #define STORM_LOGIC_REWARDOPERATORFORMULA_H_
 
-#include <set>
 #include "src/logic/OperatorFormula.h"
+#include "src/logic/RewardMeasureType.h"
 
 namespace storm {
     namespace logic {
         class RewardOperatorFormula : public OperatorFormula {
         public:
-            RewardOperatorFormula(boost::optional<std::string> const& rewardModelName, std::shared_ptr<Formula const> const& subformula);
-            RewardOperatorFormula(boost::optional<std::string> const& rewardModelName, Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula);
-            RewardOperatorFormula(boost::optional<std::string> const& rewardModelName, OptimizationDirection optimalityType, Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula);
-            RewardOperatorFormula(boost::optional<std::string> const& rewardModelName, OptimizationDirection optimalityType, std::shared_ptr<Formula const> const& subformula);
-            RewardOperatorFormula(boost::optional<std::string> const& rewardModelName, boost::optional<OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula);
+            RewardOperatorFormula(std::shared_ptr<Formula const> const& subformula, boost::optional<std::string> const& rewardModelName = boost::none, OperatorInformation const& operatorInformation = OperatorInformation(), RewardMeasureType rewardMeasureType = RewardMeasureType::Expectation);
 
             virtual ~RewardOperatorFormula() {
                 // Intentionally left empty.
@@ -48,11 +44,21 @@ namespace storm {
              */
             std::string const& getRewardModelName() const;
             
+            /*!
+             * Retrieves the measure type of the operator.
+             *
+             * @return The measure type.
+             */
+            RewardMeasureType getMeasureType() const;
+            
             virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
             
         private:
             // The (optional) name of the reward model this property refers to.
             boost::optional<std::string> rewardModelName;
+            
+            // The measure type of the operator.
+            RewardMeasureType rewardMeasureType;
         };
     }
 }

src/logic/TimeOperatorFormula.cpp

@@ -0,0 +1,37 @@
+#include "src/logic/TimeOperatorFormula.h"
+
+#include "src/logic/FormulaVisitor.h"
+
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidPropertyException.h"
+
+namespace storm {
+    namespace logic {
+        TimeOperatorFormula::TimeOperatorFormula(std::shared_ptr<Formula const> const& subformula, OperatorInformation const& operatorInformation, RewardMeasureType rewardMeasureType) : OperatorFormula(subformula, operatorInformation), rewardMeasureType(rewardMeasureType) {
+            // Intentionally left empty.
+        }
+        
+        bool TimeOperatorFormula::isTimeOperatorFormula() const {
+            return true;
+        }
+        
+        boost::any TimeOperatorFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
+        }
+        
+        std::shared_ptr<Formula> TimeOperatorFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
+            return std::make_shared<TimeOperatorFormula>(this->getSubformula().substitute(substitution), this->operatorInformation, this->rewardMeasureType);
+        }
+        
+        RewardMeasureType TimeOperatorFormula::getMeasureType() const {
+            return rewardMeasureType;
+        }
+        
+        std::ostream& TimeOperatorFormula::writeToStream(std::ostream& out) const {
+            out << "T";
+            out << "[" << rewardMeasureType << "]";
+            OperatorFormula::writeToStream(out);
+            return out;
+        }
+    }
+}

src/logic/TimeOperatorFormula.h

@@ -0,0 +1,40 @@
+#ifndef STORM_LOGIC_EXPECTEDTIMEOPERATORFORMULA_H_
+#define STORM_LOGIC_EXPECTEDTIMEOPERATORFORMULA_H_
+
+#include "src/logic/OperatorFormula.h"
+#include "src/logic/FormulaVisitor.h"
+#include "src/logic/RewardMeasureType.h"
+
+namespace storm {
+    namespace logic {
+        class TimeOperatorFormula : public OperatorFormula {
+        public:
+            TimeOperatorFormula(std::shared_ptr<Formula const> const& subformula, OperatorInformation const& operatorInformation = OperatorInformation(), RewardMeasureType rewardMeasureType = RewardMeasureType::Expectation);
+            
+            virtual ~TimeOperatorFormula() {
+                // Intentionally left empty.
+            }
+            
+            virtual bool isTimeOperatorFormula() const override;
+
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
+            
+            virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
+            
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            
+            /*!
+             * Retrieves the measure type of the operator.
+             *
+             * @return The measure type of the operator.
+             */
+            RewardMeasureType getMeasureType() const;
+            
+        private:
+            // The measure type of the operator.
+            RewardMeasureType rewardMeasureType;
+        };
+    }
+}
+
+#endif /* STORM_LOGIC_EXPECTEDTIMEOPERATORFORMULA_H_ */

src/logic/UnaryBooleanStateFormula.cpp

@@ -2,10 +2,13 @@
 
 #include "src/logic/FormulaVisitor.h"
 
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidPropertyException.h"
+
 namespace storm {
     namespace logic {
         UnaryBooleanStateFormula::UnaryBooleanStateFormula(OperatorType operatorType, std::shared_ptr<Formula const> const& subformula) : UnaryStateFormula(subformula), operatorType(operatorType) {
-            // Intentionally left empty.
+            STORM_LOG_THROW(this->getSubformula().hasQualitativeResult(), storm::exceptions::InvalidPropertyException, "Boolean formula must have subformulas with qualitative result.");
         }
         
         bool UnaryBooleanStateFormula::isUnaryBooleanStateFormula() const {

src/logic/UnaryPathFormula.cpp

@@ -25,5 +25,14 @@ namespace storm {
         void UnaryPathFormula::gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const {
             this->getSubformula().gatherReferencedRewardModels(referencedRewardModels);
         }
+        
+        bool UnaryPathFormula::hasQualitativeResult() const {
+            return false;
+        }
+        
+        bool UnaryPathFormula::hasQuantitativeResult() const {
+            return true;
+        }
+
     }
 }

src/logic/UnaryPathFormula.h

@@ -23,6 +23,9 @@ namespace storm {
             virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
             virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
             
+            virtual bool hasQualitativeResult() const override;
+            virtual bool hasQuantitativeResult() const override;
+
         private:
             std::shared_ptr<Formula const> subformula;
         };

src/modelchecker/AbstractModelChecker.cpp

@@ -16,16 +16,6 @@ namespace storm {
             STORM_LOG_THROW(this->canHandle(formula), storm::exceptions::InvalidArgumentException, "The model checker is not able to check the formula '" << formula << "'.");
             if (formula.isStateFormula()) {
                 return this->checkStateFormula(checkTask.substituteFormula(formula.asStateFormula()));
-            } else if (formula.isPathFormula()) {
-                if (formula.isProbabilityPathFormula()) {
-                    return this->computeProbabilities(checkTask);
-                } else if (formula.isRewardPathFormula()) {
-                    return this->computeRewards(checkTask);
-                }
-            } else if (formula.isConditionalProbabilityFormula()) {
-                return this->computeConditionalProbabilities(checkTask.substituteFormula(formula.asConditionalFormula()));
-            } else if (formula.isConditionalRewardFormula()) {
-                return this->computeConditionalRewards(checkTask.substituteFormula(formula.asConditionalFormula()));
             }
             STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid.");
         }
@@ -34,8 +24,8 @@ namespace storm {
             storm::logic::Formula const& formula = checkTask.getFormula();
             if (formula.isBoundedUntilFormula()) {
                 return this->computeBoundedUntilProbabilities(checkTask.substituteFormula(formula.asBoundedUntilFormula()));
-            } else if (formula.isEventuallyFormula()) {
-                return this->computeEventuallyProbabilities(checkTask.substituteFormula(formula.asEventuallyFormula()));
+            } else if (formula.isReachabilityProbabilityFormula()) {
+                return this->computeReachabilityProbabilities(checkTask.substituteFormula(formula.asReachabilityProbabilityFormula()));
             } else if (formula.isGloballyFormula()) {
                 return this->computeGloballyProbabilities(checkTask.substituteFormula(formula.asGloballyFormula()));
             } else if (formula.isUntilFormula()) {
@@ -56,7 +46,7 @@ namespace storm {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
         }
         
-        std::unique_ptr<CheckResult> AbstractModelChecker::computeEventuallyProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> AbstractModelChecker::computeReachabilityProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
             storm::logic::EventuallyFormula const& pathFormula = checkTask.getFormula();
             storm::logic::UntilFormula newFormula(storm::logic::Formula::getTrueFormula(), pathFormula.getSubformula().asSharedPointer());
             return this->computeUntilProbabilities(checkTask.substituteFormula(newFormula));
@@ -74,39 +64,39 @@ namespace storm {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
         }
         
-        std::unique_ptr<CheckResult> AbstractModelChecker::computeRewards(CheckTask<storm::logic::Formula> const& checkTask) {
+        std::unique_ptr<CheckResult> AbstractModelChecker::computeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::Formula> const& checkTask) {
             storm::logic::Formula const& rewardFormula = checkTask.getFormula();
             if (rewardFormula.isCumulativeRewardFormula()) {
-                return this->computeCumulativeRewards(checkTask.substituteFormula(rewardFormula.asCumulativeRewardFormula()));
+                return this->computeCumulativeRewards(rewardMeasureType, checkTask.substituteFormula(rewardFormula.asCumulativeRewardFormula()));
             } else if (rewardFormula.isInstantaneousRewardFormula()) {
-                return this->computeInstantaneousRewards(checkTask.substituteFormula(rewardFormula.asInstantaneousRewardFormula()));
+                return this->computeInstantaneousRewards(rewardMeasureType, checkTask.substituteFormula(rewardFormula.asInstantaneousRewardFormula()));
             } else if (rewardFormula.isReachabilityRewardFormula()) {
-                return this->computeReachabilityRewards(checkTask.substituteFormula(rewardFormula.asEventuallyFormula()));
+                return this->computeReachabilityRewards(rewardMeasureType, checkTask.substituteFormula(rewardFormula.asReachabilityRewardFormula()));
             } else if (rewardFormula.isLongRunAverageRewardFormula()) {
-                return this->computeLongRunAverageRewards(checkTask.substituteFormula(rewardFormula.asLongRunAverageRewardFormula()));
+                return this->computeLongRunAverageRewards(rewardMeasureType, checkTask.substituteFormula(rewardFormula.asLongRunAverageRewardFormula()));
             } else if (rewardFormula.isConditionalRewardFormula()) {
-                return this->computeConditionalRewards(checkTask.substituteFormula(rewardFormula.asConditionalFormula()));
+                return this->computeConditionalRewards(rewardMeasureType, checkTask.substituteFormula(rewardFormula.asConditionalFormula()));
             }
             STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << rewardFormula << "' is invalid.");
         }
         
-        std::unique_ptr<CheckResult> AbstractModelChecker::computeConditionalRewards(CheckTask<storm::logic::ConditionalFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> AbstractModelChecker::computeConditionalRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::ConditionalFormula> const& checkTask) {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
         }
         
-        std::unique_ptr<CheckResult> AbstractModelChecker::computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> AbstractModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
         }
         
-        std::unique_ptr<CheckResult> AbstractModelChecker::computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> AbstractModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
         }
         
-        std::unique_ptr<CheckResult> AbstractModelChecker::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> AbstractModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
         }
         
-        std::unique_ptr<CheckResult> AbstractModelChecker::computeLongRunAverageRewards(CheckTask<storm::logic::LongRunAverageRewardFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> AbstractModelChecker::computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula> const& checkTask) {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
         }
         
@@ -114,7 +104,15 @@ namespace storm {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
         }
         
-        std::unique_ptr<CheckResult> AbstractModelChecker::computeExpectedTimes(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> AbstractModelChecker::computeTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::Formula> const& checkTask) {
+            storm::logic::Formula const& timeFormula = checkTask.getFormula();
+            if (timeFormula.isReachabilityTimeFormula()) {
+                return this->computeReachabilityTimes(rewardMeasureType, checkTask.substituteFormula(timeFormula.asReachabilityTimeFormula()));
+            }
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
+        }
+        
+        std::unique_ptr<CheckResult> AbstractModelChecker::computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
         }
         
@@ -130,8 +128,8 @@ namespace storm {
                 return this->checkProbabilityOperatorFormula(checkTask.substituteFormula(stateFormula.asProbabilityOperatorFormula()));
             } else if (stateFormula.isRewardOperatorFormula()) {
                 return this->checkRewardOperatorFormula(checkTask.substituteFormula(stateFormula.asRewardOperatorFormula()));
-            } else if (stateFormula.isExpectedTimeOperatorFormula()) {
-                return this->checkExpectedTimeOperatorFormula(checkTask.substituteFormula(stateFormula.asExpectedTimeOperatorFormula()));
+            } else if (stateFormula.isTimeOperatorFormula()) {
+                return this->checkTimeOperatorFormula(checkTask.substituteFormula(stateFormula.asTimeOperatorFormula()));
             } else if (stateFormula.isLongRunAverageOperatorFormula()) {
                 return this->checkLongRunAverageOperatorFormula(checkTask.substituteFormula(stateFormula.asLongRunAverageOperatorFormula()));
             } else if (stateFormula.isAtomicExpressionFormula()) {
@@ -193,7 +191,7 @@ namespace storm {
         
         std::unique_ptr<CheckResult> AbstractModelChecker::checkRewardOperatorFormula(CheckTask<storm::logic::RewardOperatorFormula> const& checkTask) {
             storm::logic::RewardOperatorFormula const& stateFormula = checkTask.getFormula();
-            std::unique_ptr<CheckResult> result = this->computeRewards(checkTask.substituteFormula(stateFormula.getSubformula()));
+            std::unique_ptr<CheckResult> result = this->computeRewards(stateFormula.getMeasureType(), checkTask.substituteFormula(stateFormula.getSubformula()));
             
             if (checkTask.isBoundSet()) {
                 STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result.");
@@ -203,11 +201,11 @@ namespace storm {
             }
         }
         
-		std::unique_ptr<CheckResult> AbstractModelChecker::checkExpectedTimeOperatorFormula(CheckTask<storm::logic::ExpectedTimeOperatorFormula> const& checkTask) {
-            storm::logic::ExpectedTimeOperatorFormula const& stateFormula = checkTask.getFormula();
-			STORM_LOG_THROW(stateFormula.getSubformula().isReachbilityExpectedTimeFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
+		std::unique_ptr<CheckResult> AbstractModelChecker::checkTimeOperatorFormula(CheckTask<storm::logic::TimeOperatorFormula> const& checkTask) {
+            storm::logic::TimeOperatorFormula const& stateFormula = checkTask.getFormula();
+			STORM_LOG_THROW(stateFormula.getSubformula().isReachabilityTimeFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
             
-            std::unique_ptr<CheckResult> result = this->computeExpectedTimes(checkTask.substituteFormula(stateFormula.getSubformula().asEventuallyFormula()));
+            std::unique_ptr<CheckResult> result = this->computeTimes(stateFormula.getMeasureType(), checkTask.substituteFormula(stateFormula.getSubformula()));
             
             if (checkTask.isBoundSet()) {
                 STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result.");

src/modelchecker/AbstractModelChecker.h

@@ -11,6 +11,8 @@ namespace storm {
     namespace modelchecker {
         class CheckResult;
         
+        enum class RewardType { Expectation, Variance };
+        
         class AbstractModelChecker {
         public:
             virtual ~AbstractModelChecker() {
@@ -38,22 +40,23 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeProbabilities(CheckTask<storm::logic::Formula> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(CheckTask<storm::logic::ConditionalFormula> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula> const& checkTask);
-            virtual std::unique_ptr<CheckResult> computeEventuallyProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask);
+            virtual std::unique_ptr<CheckResult> computeReachabilityProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeNextProbabilities(CheckTask<storm::logic::NextFormula> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask);
             
             // The methods to compute the rewards for path formulas.
-            virtual std::unique_ptr<CheckResult> computeRewards(CheckTask<storm::logic::Formula> const& checkTask);
-            virtual std::unique_ptr<CheckResult> computeConditionalRewards(CheckTask<storm::logic::ConditionalFormula> const& checkTask);
-            virtual std::unique_ptr<CheckResult> computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask);
-            virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask);
-            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask);
-            virtual std::unique_ptr<CheckResult> computeLongRunAverageRewards(CheckTask<storm::logic::LongRunAverageRewardFormula> const& checkTask);
+            virtual std::unique_ptr<CheckResult> computeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::Formula> const& checkTask);
+            virtual std::unique_ptr<CheckResult> computeConditionalRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::ConditionalFormula> const& checkTask);
+            virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask);
+            virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask);
+            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask);
+            virtual std::unique_ptr<CheckResult> computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula> const& checkTask);
             
-            // The methods to compute the long-run average and expected time.
+            // The methods to compute the long-run average probabilities and timing measures.
             virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula> const& checkTask);
-            virtual std::unique_ptr<CheckResult> computeExpectedTimes(CheckTask<storm::logic::EventuallyFormula> const& checkTask);
+            virtual std::unique_ptr<CheckResult> computeTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::Formula> const& checkTask);
+            virtual std::unique_ptr<CheckResult> computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask);
             
             // The methods to check state formulas.
             virtual std::unique_ptr<CheckResult> checkStateFormula(CheckTask<storm::logic::StateFormula> const& stateFormula);
@@ -63,7 +66,7 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> checkBooleanLiteralFormula(CheckTask<storm::logic::BooleanLiteralFormula> const& checkTask);
             virtual std::unique_ptr<CheckResult> checkProbabilityOperatorFormula(CheckTask<storm::logic::ProbabilityOperatorFormula> const& checkTask);
             virtual std::unique_ptr<CheckResult> checkRewardOperatorFormula(CheckTask<storm::logic::RewardOperatorFormula> const& checkTask);
-            virtual std::unique_ptr<CheckResult> checkExpectedTimeOperatorFormula(CheckTask<storm::logic::ExpectedTimeOperatorFormula> const& checkTask);
+            virtual std::unique_ptr<CheckResult> checkTimeOperatorFormula(CheckTask<storm::logic::TimeOperatorFormula> const& checkTask);
             virtual std::unique_ptr<CheckResult> checkLongRunAverageOperatorFormula(CheckTask<storm::logic::LongRunAverageOperatorFormula> const& checkTask);
             virtual std::unique_ptr<CheckResult> checkUnaryBooleanStateFormula(CheckTask<storm::logic::UnaryBooleanStateFormula> const& checkTask);
         };

src/modelchecker/csl/HybridCtmcCslModelChecker.cpp

@@ -56,7 +56,7 @@ namespace storm {
         }
         
         template<storm::dd::DdType DdType, class ValueType>
-        std::unique_ptr<CheckResult> HybridCtmcCslModelChecker<DdType, ValueType>::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> HybridCtmcCslModelChecker<DdType, ValueType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
             storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
             std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
             SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>();
@@ -85,13 +85,13 @@ namespace storm {
         }
         
         template<storm::dd::DdType DdType, class ValueType>
-        std::unique_ptr<CheckResult> HybridCtmcCslModelChecker<DdType, ValueType>::computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> HybridCtmcCslModelChecker<DdType, ValueType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
             storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula();
             return storm::modelchecker::helper::HybridCtmcCslHelper<DdType, ValueType>::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory);
         }
 
         template<storm::dd::DdType DdType, class ValueType>
-        std::unique_ptr<CheckResult> HybridCtmcCslModelChecker<DdType, ValueType>::computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> HybridCtmcCslModelChecker<DdType, ValueType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
             storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
             return storm::modelchecker::helper::HybridCtmcCslHelper<DdType, ValueType>::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory);
         }

src/modelchecker/csl/HybridCtmcCslModelChecker.h

@@ -21,9 +21,9 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeNextProbabilities(CheckTask<storm::logic::NextFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula> const& checkTask) override;
 
         protected:

src/modelchecker/csl/SparseCtmcCslModelChecker.cpp

@@ -79,21 +79,21 @@ namespace storm {
         }
         
         template <typename SparseCtmcModelType>
-        std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
             storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula();
             std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseCtmcCslHelper<ValueType>::computeInstantaneousRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory);
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
         }
                 
         template <typename SparseCtmcModelType>
-        std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
             storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
             std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseCtmcCslHelper<ValueType>::computeCumulativeRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory);
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
         }
                 
         template <typename SparseCtmcModelType>
-        std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
             storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
             std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
             ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();

src/modelchecker/csl/SparseCtmcCslModelChecker.h

@@ -24,9 +24,9 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeNextProbabilities(CheckTask<storm::logic::NextFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeExpectedTimes(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
 

src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp

@@ -33,7 +33,7 @@ namespace storm {
         bool SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const {
             storm::logic::Formula const& formula = checkTask.getFormula();
             storm::logic::FragmentSpecification fragment = storm::logic::csl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setReachabilityRewardFormulasAllowed(true);
-            fragment.setExpectedTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true);
+            fragment.setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true);
             return formula.isInFragment(fragment);
         }
         
@@ -71,7 +71,7 @@ namespace storm {
         }
                 
         template<typename SparseMarkovAutomatonModelType>
-        std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
             storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
             STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
             STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute reachability rewards in non-closed Markov automaton.");
@@ -96,14 +96,14 @@ namespace storm {
         }
                 
         template<typename SparseMarkovAutomatonModelType>
-        std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::computeExpectedTimes(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
             storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
             STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
             STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute expected times in non-closed Markov automaton.");
             std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
             ExplicitQualitativeCheckResult& subResult = subResultPointer->asExplicitQualitativeCheckResult();
 
-            std::vector<ValueType> result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper<ValueType>::computeExpectedTimes(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory);
+            std::vector<ValueType> result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper<ValueType>::computeTimes(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory);
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(result)));
         }
                 

src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h

@@ -23,9 +23,9 @@ namespace storm {
             virtual bool canHandle(CheckTask<storm::logic::Formula> const& checkTask) const override;
             virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeExpectedTimes(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
             
         private:
             // An object that is used for retrieving solvers for systems of linear equations that are the result of nondeterministic choices.

src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp

@@ -363,7 +363,7 @@ namespace storm {
                 STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive.");
                 
                 storm::storage::SparseMatrix<ValueType> uniformizedMatrix = computeUniformizedMatrix(rateMatrix, storm::storage::BitVector(numberOfStates, true), uniformizationRate, exitRateVector);
-                
+
                 // Compute the total state reward vector.
                 std::vector<ValueType> totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, exitRateVector);
                 

src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp

@@ -345,7 +345,7 @@ namespace storm {
             }
             
             template <typename ValueType>
-            std::vector<ValueType> SparseMarkovAutomatonCslHelper<ValueType>::computeExpectedTimes(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
+            std::vector<ValueType> SparseMarkovAutomatonCslHelper<ValueType>::computeTimes(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
                  uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount();
                 std::vector<ValueType> rewardValues(numberOfStates, storm::utility::zero<ValueType>());
                 storm::utility::vector::setVectorValues(rewardValues, markovianStates, storm::utility::one<ValueType>());

src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h

@@ -24,7 +24,7 @@ namespace storm {
                 
                 static std::vector<ValueType> computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
                 
-                static std::vector<ValueType> computeExpectedTimes(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
+                static std::vector<ValueType> computeTimes(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
                 
             private:
                 static void computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& exitRates, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector<ValueType>& markovianNonGoalValues, std::vector<ValueType>& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);

src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp

@@ -79,21 +79,21 @@ namespace storm {
         }
                 
         template<storm::dd::DdType DdType, typename ValueType>
-        std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
             storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
             STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound.");
             return storm::modelchecker::helper::HybridDtmcPrctlHelper<DdType, ValueType>::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory);
         }
                 
         template<storm::dd::DdType DdType, typename ValueType>
-        std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
             storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula();
             STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound.");
             return storm::modelchecker::helper::HybridDtmcPrctlHelper<DdType, ValueType>::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory);
         }
         
         template<storm::dd::DdType DdType, typename ValueType>
-        std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
             storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
             std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
             SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>();

src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h

@@ -22,9 +22,9 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeNextProbabilities(CheckTask<storm::logic::NextFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula> const& checkTask) override;
 
         protected:

src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp

@@ -77,7 +77,7 @@ namespace storm {
         }
         
         template<storm::dd::DdType DdType, typename ValueType>
-        std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
             storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
             STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
             STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
@@ -85,7 +85,7 @@ namespace storm {
         }
                 
         template<storm::dd::DdType DdType, typename ValueType>
-        std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
             storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula();
             STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
             STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
@@ -93,7 +93,7 @@ namespace storm {
         }
                 
         template<storm::dd::DdType DdType, typename ValueType>
-        std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
             storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
             STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
             std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());

src/modelchecker/prctl/HybridMdpPrctlModelChecker.h

@@ -29,9 +29,9 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeNextProbabilities(CheckTask<storm::logic::NextFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
             
         protected:
             storm::models::symbolic::Mdp<DdType, ValueType> const& getModel() const override;

src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp

@@ -82,7 +82,7 @@ namespace storm {
         }
         
         template<typename SparseDtmcModelType>
-        std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
             storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
             STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
             std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeCumulativeRewards(this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *linearEquationSolverFactory);
@@ -90,7 +90,7 @@ namespace storm {
         }
         
         template<typename SparseDtmcModelType>
-        std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
             storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula();
             STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
             std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeInstantaneousRewards(this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *linearEquationSolverFactory);
@@ -98,7 +98,7 @@ namespace storm {
         }
         
         template<typename SparseDtmcModelType>
-        std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
             storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
             std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
             ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
@@ -131,7 +131,7 @@ namespace storm {
         }
         
         template<typename SparseDtmcModelType>
-        std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeConditionalRewards(CheckTask<storm::logic::ConditionalFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeConditionalRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::ConditionalFormula> const& checkTask) {
             storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula();
             STORM_LOG_THROW(conditionalFormula.getSubformula().isReachabilityRewardFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula.");
             STORM_LOG_THROW(conditionalFormula.getConditionFormula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula.");

src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h

@@ -27,10 +27,10 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(CheckTask<storm::logic::ConditionalFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula> const& checkTask) override;
 
-            virtual std::unique_ptr<CheckResult> computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeConditionalRewards(CheckTask<storm::logic::ConditionalFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeConditionalRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::ConditionalFormula> const& checkTask) override;
 
         private:
             // An object that is used for retrieving linear equation solvers.

src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@@ -109,7 +109,7 @@ namespace storm {
         }
         
         template<typename SparseMdpModelType>
-        std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
             storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
             STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
             STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound.");
@@ -118,7 +118,7 @@ namespace storm {
         }
         
         template<typename SparseMdpModelType>
-        std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
             storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula();
             STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
             STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound.");
@@ -127,7 +127,7 @@ namespace storm {
         }
                 
         template<typename SparseMdpModelType>
-        std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
             storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
             STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
             std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());

src/modelchecker/prctl/SparseMdpPrctlModelChecker.h

@@ -23,9 +23,9 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(CheckTask<storm::logic::ConditionalFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula> const& checkTask) override;
             
         private:

src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp

@@ -80,7 +80,7 @@ namespace storm {
         }
         
         template<storm::dd::DdType DdType, typename ValueType>
-        std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<DdType, ValueType>::computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<DdType, ValueType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
             storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
             STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
             storm::dd::Add<DdType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory);
@@ -88,7 +88,7 @@ namespace storm {
         }
         
         template<storm::dd::DdType DdType, typename ValueType>
-        std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<DdType, ValueType>::computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<DdType, ValueType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
             storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula();
             STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
             storm::dd::Add<DdType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory);
@@ -96,7 +96,7 @@ namespace storm {
         }
         
         template<storm::dd::DdType DdType, typename ValueType>
-        std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
             storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
             std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
             SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>();

src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h

@@ -19,9 +19,9 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeNextProbabilities(CheckTask<storm::logic::NextFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
             
         protected:
             storm::models::symbolic::Dtmc<DdType, ValueType> const& getModel() const override;

src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp

@@ -79,7 +79,7 @@ namespace storm {
         }
         
         template<storm::dd::DdType DdType, typename ValueType>
-        std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
             storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
             STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
             STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
@@ -87,7 +87,7 @@ namespace storm {
         }
         
         template<storm::dd::DdType DdType, typename ValueType>
-        std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
             storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula();
             STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
             STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
@@ -95,7 +95,7 @@ namespace storm {
         }
         
         template<storm::dd::DdType DdType, typename ValueType>
-        std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
             storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
             STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
             std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());

src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h

@@ -21,9 +21,9 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeNextProbabilities(CheckTask<storm::logic::NextFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
             
             protected:
             storm::models::symbolic::Mdp<DdType, ValueType> const& getModel() const override;

src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp

@@ -153,7 +153,7 @@ namespace storm {
         }
         
         template<typename SparseDtmcModelType>
-        std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeLongRunAverageRewards(CheckTask<storm::logic::LongRunAverageRewardFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula> const& checkTask) {
             // Do some sanity checks to establish some required properties.
             RewardModelType const& rewardModel = this->getModel().getRewardModel(checkTask.isRewardModelSet() ? checkTask.getRewardModel() : "");
             STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::IllegalArgumentException, "Input model does not have a reward model.");
@@ -535,7 +535,7 @@ namespace storm {
         }
         
         template<typename SparseDtmcModelType>
-        std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
             storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
             
             // Retrieve the appropriate bitvectors by model checking the subformulas.

src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h

@@ -41,8 +41,8 @@ namespace storm {
             virtual bool canHandle(CheckTask<storm::logic::Formula> const& checkTask) const override;
             virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeLongRunAverageRewards(CheckTask<storm::logic::LongRunAverageRewardFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(CheckTask<storm::logic::ConditionalFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula> const& checkTask) override;
            

src/parser/FormulaParser.cpp

@@ -88,6 +88,17 @@ namespace storm {
             // A parser used for recognizing the optimality operators.
             optimalityOperatorStruct optimalityOperator_;
             
+            struct rewardMeasureTypeStruct : qi::symbols<char, storm::logic::RewardMeasureType> {
+                rewardMeasureTypeStruct() {
+                    add
+                    ("exp", storm::logic::RewardMeasureType::Expectation)
+                    ("var", storm::logic::RewardMeasureType::Variance);
+                }
+            };
+
+            // A parser used for recognizing the reward measure types.
+            rewardMeasureTypeStruct rewardMeasureType_;
+            
             // Parser and manager used for recognizing expressions.
             storm::parser::ExpressionParser expressionParser;
             
@@ -97,10 +108,11 @@ namespace storm {
             
             qi::rule<Iterator, std::vector<std::shared_ptr<storm::logic::Formula>>(), Skipper> start;
             
-            qi::rule<Iterator, std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>>(), qi::locals<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>>, Skipper> operatorInformation;
+            qi::rule<Iterator, storm::logic::OperatorInformation(), qi::locals<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>>, Skipper> operatorInformation;
+            qi::rule<Iterator, storm::logic::RewardMeasureType(), Skipper> rewardMeasureType;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> probabilityOperator;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> rewardOperator;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> expectedTimeOperator;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> timeOperator;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> longRunAverageOperator;
             
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> simpleFormula;
@@ -147,11 +159,11 @@ namespace storm {
             std::shared_ptr<storm::logic::Formula> createNextFormula(std::shared_ptr<storm::logic::Formula> const& subformula) const;
             std::shared_ptr<storm::logic::Formula> createUntilFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, std::shared_ptr<storm::logic::Formula> const& rightSubformula);
             std::shared_ptr<storm::logic::Formula> createConditionalFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula, storm::logic::FormulaContext context) const;
-            std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> createOperatorInformation(boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<storm::logic::ComparisonType> const& comparisonType, boost::optional<double> const& threshold) const;
-            std::shared_ptr<storm::logic::Formula> createLongRunAverageOperatorFormula(std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
-            std::shared_ptr<storm::logic::Formula> createRewardOperatorFormula(boost::optional<std::string> const& rewardModelName, std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
-            std::shared_ptr<storm::logic::Formula> createExpectedTimeOperatorFormula(std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
-            std::shared_ptr<storm::logic::Formula> createProbabilityOperatorFormula(std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula);
+            storm::logic::OperatorInformation createOperatorInformation(boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<storm::logic::ComparisonType> const& comparisonType, boost::optional<double> const& threshold) const;
+            std::shared_ptr<storm::logic::Formula> createLongRunAverageOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
+            std::shared_ptr<storm::logic::Formula> createRewardOperatorFormula(boost::optional<storm::logic::RewardMeasureType> const& rewardMeasureType, boost::optional<std::string> const& rewardModelName, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
+            std::shared_ptr<storm::logic::Formula> createTimeOperatorFormula(boost::optional<storm::logic::RewardMeasureType> const& rewardMeasureType, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
+            std::shared_ptr<storm::logic::Formula> createProbabilityOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula);
             std::shared_ptr<storm::logic::Formula> createBinaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType);
             std::shared_ptr<storm::logic::Formula> createUnaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula> const& subformula, boost::optional<storm::logic::UnaryBooleanStateFormula::OperatorType> const& operatorType);
             
@@ -301,6 +313,9 @@ namespace storm {
             pathFormula = conditionalFormula(qi::_r1);
             pathFormula.name("path formula");
             
+            rewardMeasureType = qi::lit("[") >> rewardMeasureType_ >> qi::lit("]");
+            rewardMeasureType.name("reward measure type");
+            
             operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > qi::double_[qi::_c = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::bind(&FormulaParserGrammar::createOperatorInformation, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)];
             operatorInformation.name("operator information");
             
@@ -310,11 +325,11 @@ namespace storm {
             rewardModelName = qi::lit("{\"") > label > qi::lit("\"}");
             rewardModelName.name("reward model name");
             
-            rewardOperator = (qi::lit("R") > -rewardModelName > operatorInformation > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createRewardOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)];
+            rewardOperator = (qi::lit("R") > -rewardMeasureType > -rewardModelName > operatorInformation > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createRewardOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)];
             rewardOperator.name("reward operator");
             
-            expectedTimeOperator = (qi::lit("ET") > operatorInformation > qi::lit("[") > eventuallyFormula(storm::logic::FormulaContext::ExpectedTime) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createExpectedTimeOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
-            expectedTimeOperator.name("expected time operator");
+            timeOperator = (qi::lit("T") > -rewardMeasureType > operatorInformation > qi::lit("[") > eventuallyFormula(storm::logic::FormulaContext::Time) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)];
+            timeOperator.name("time operator");
             
             probabilityOperator = (qi::lit("P") > operatorInformation > qi::lit("[") > pathFormula(storm::logic::FormulaContext::Probability) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProbabilityOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
             probabilityOperator.name("probability operator");
@@ -461,28 +476,36 @@ namespace storm {
             return std::shared_ptr<storm::logic::Formula>(new storm::logic::ConditionalFormula(leftSubformula, rightSubformula, context));
         }
         
-        std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> FormulaParserGrammar::createOperatorInformation(boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<storm::logic::ComparisonType> const& comparisonType, boost::optional<double> const& threshold) const {
+        storm::logic::OperatorInformation FormulaParserGrammar::createOperatorInformation(boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<storm::logic::ComparisonType> const& comparisonType, boost::optional<double> const& threshold) const {
             if (comparisonType && threshold) {
-                return std::make_pair(optimizationDirection, storm::logic::Bound<double>(comparisonType.get(), threshold.get()));
+                return storm::logic::OperatorInformation(optimizationDirection, storm::logic::Bound<double>(comparisonType.get(), threshold.get()));
             } else {
-                return std::make_pair(optimizationDirection, boost::none);
+                return storm::logic::OperatorInformation(optimizationDirection, boost::none);
             }
         }
         
-        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createLongRunAverageOperatorFormula(std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
-            return std::shared_ptr<storm::logic::Formula>(new storm::logic::LongRunAverageOperatorFormula(operatorInformation.first, operatorInformation.second, subformula));
+        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createLongRunAverageOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::LongRunAverageOperatorFormula(subformula, operatorInformation));
         }
         
-        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createRewardOperatorFormula(boost::optional<std::string> const& rewardModelName, std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
-            return std::shared_ptr<storm::logic::Formula>(new storm::logic::RewardOperatorFormula(rewardModelName, operatorInformation.first, operatorInformation.second, subformula));
+        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createRewardOperatorFormula(boost::optional<storm::logic::RewardMeasureType> const& rewardMeasureType, boost::optional<std::string> const& rewardModelName, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
+            storm::logic::RewardMeasureType measureType = storm::logic::RewardMeasureType::Expectation;
+            if (rewardMeasureType) {
+                measureType = rewardMeasureType.get();
+            }
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::RewardOperatorFormula(subformula, rewardModelName, operatorInformation, measureType));
         }
         
-        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createExpectedTimeOperatorFormula(std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
-            return std::shared_ptr<storm::logic::Formula>(new storm::logic::ExpectedTimeOperatorFormula(operatorInformation.first, operatorInformation.second, subformula));
+        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createTimeOperatorFormula(boost::optional<storm::logic::RewardMeasureType> const& rewardMeasureType, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
+            storm::logic::RewardMeasureType measureType = storm::logic::RewardMeasureType::Expectation;
+            if (rewardMeasureType) {
+                measureType = rewardMeasureType.get();
+            }
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::TimeOperatorFormula(subformula, operatorInformation, measureType));
         }
         
-        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createProbabilityOperatorFormula(std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) {
-            return std::shared_ptr<storm::logic::Formula>(new storm::logic::ProbabilityOperatorFormula(operatorInformation.first, operatorInformation.second, subformula));
+        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createProbabilityOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) {
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::ProbabilityOperatorFormula(subformula, operatorInformation));
         }
         
         std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createBinaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType) {

src/parser/PrismParser.cpp

@@ -11,7 +11,7 @@ namespace storm {
     namespace parser {
         storm::prism::Program PrismParser::parse(std::string const& filename) {
             // Open file and initialize result.
-            std::ifstream inputFileStream(filename, std::ios::in);
+            std::ifstream inputFileStream(filename);
             STORM_LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'.");
             
             storm::prism::Program result;
@@ -35,7 +35,7 @@ namespace storm {
             PositionIteratorType first(input.begin());
             PositionIteratorType iter = first;
             PositionIteratorType last(input.end());
-            assert(first != last);
+            STORM_LOG_ASSERT(first != last, "Illegal input to PRISM parser.");
             
             // Create empty result;
             storm::prism::Program result;

src/settings/ArgumentValidators.h

@@ -18,6 +18,7 @@
 #include "src/exceptions/IllegalArgumentValueException.h"
 #include "src/exceptions/IllegalFunctionCallException.h"
 
+#include <sys/stat.h>
 
 namespace storm {
 	namespace settings {
@@ -97,11 +98,16 @@ namespace storm {
              */
 			static std::function<bool (std::string const&)> existingReadableFileValidator() {
 				return [] (std::string const fileName) -> bool {
-					std::ifstream targetFile(fileName);
-					bool isFileGood = targetFile.good();
-
-                    STORM_LOG_THROW(isFileGood, storm::exceptions::IllegalArgumentValueException, "The file " << fileName << " does not exist or is not readable.");
-					return isFileGood;
+                    // First check existence as ifstream::good apparently als returns true for directories.
+                    struct stat info;
+                    stat(fileName.c_str(), &info);
+                    STORM_LOG_THROW(info.st_mode & S_IFREG, storm::exceptions::IllegalArgumentValueException, "Unable to read from non-existing file '" << fileName << "'.");
+                    
+                    // Now that we know it's a file, we can check its readability.
+                    std::ifstream istream(fileName);
+                    STORM_LOG_THROW(istream.good(), storm::exceptions::IllegalArgumentValueException, "Unable to read from file '" << fileName << "'.");
+                    
+                    return true;
 				};
 			}
 

src/settings/modules/GeneralSettings.cpp

@@ -32,6 +32,8 @@ namespace storm {
             const std::string GeneralSettings::explicitOptionShortName = "exp";
             const std::string GeneralSettings::symbolicOptionName = "symbolic";
             const std::string GeneralSettings::symbolicOptionShortName = "s";
+            const std::string GeneralSettings::explorationOrderOptionName = "explorder";
+            const std::string GeneralSettings::explorationOrderOptionShortName = "eo";
             const std::string GeneralSettings::propertyOptionName = "prop";
             const std::string GeneralSettings::propertyOptionShortName = "prop";
             const std::string GeneralSettings::transitionRewardsOptionName = "transrew";
@@ -83,6 +85,11 @@ namespace storm {
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("labeling filename", "The name of the file from which to read the state labeling.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, symbolicOptionName, false, "Parses the model given in a symbolic representation.").setShortName(symbolicOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the symbolic model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
+
+                std::vector<std::string> explorationOrders = {"dfs", "bfs"};
+                this->addOption(storm::settings::OptionBuilder(moduleName, explorationOrderOptionName, false, "Sets which exploration order to use.").setShortName(explorationOrderOptionShortName)
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the exploration order to choose. Available are: dfs and bfs.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(explorationOrders)).setDefaultValueString("bfs").build()).build());
+
                 this->addOption(storm::settings::OptionBuilder(moduleName, propertyOptionName, false, "Specifies the formulas to be checked on the model.").setShortName(propertyOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("formula or filename", "The formula or the file containing the formulas.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, counterexampleOptionName, false, "Generates a counterexample for the given PRCTL formulas if not satisfied by the model")
@@ -186,6 +193,20 @@ namespace storm {
                 return this->getOption(symbolicOptionName).getArgumentByName("filename").getValueAsString();
             }
             
+            bool GeneralSettings::isExplorationOrderSet() const {
+                return this->getOption(explorationOrderOptionName).getHasOptionBeenSet();
+            }
+            
+            storm::builder::ExplorationOrder GeneralSettings::getExplorationOrder() const {
+                std::string explorationOrderAsString = this->getOption(explorationOrderOptionName).getArgumentByName("name").getValueAsString();
+                if (explorationOrderAsString == "dfs") {
+                    return storm::builder::ExplorationOrder::Dfs;
+                } else if (explorationOrderAsString == "bfs") {
+                    return storm::builder::ExplorationOrder::Bfs;
+                }
+                STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown exploration order '" << explorationOrderAsString << "'.");
+            }
+            
             bool GeneralSettings::isPropertySet() const {
                 return this->getOption(propertyOptionName).getHasOptionBeenSet();
             }

src/settings/modules/GeneralSettings.h

@@ -4,6 +4,8 @@
 #include "storm-config.h"
 #include "src/settings/modules/ModuleSettings.h"
 
+#include "src/builder/ExplorationOrder.h"
+
 namespace storm {
     namespace solver {
         enum class EquationSolverType;
@@ -25,7 +27,6 @@ namespace storm {
             class GeneralSettings : public ModuleSettings {
             public:
                 // An enumeration of all engines.
-
                 enum class Engine {
                     Sparse, Hybrid, Dd, AbstractionRefinement
                 };
@@ -138,6 +139,20 @@ namespace storm {
                  * @return The name of the file that contains the symbolic model specification.
                  */
                 std::string getSymbolicModelFilename() const;
+                
+                /*!
+                 * Retrieves whether the model exploration order was set.
+                 *
+                 * @return True if the model exploration option was set.
+                 */
+                bool isExplorationOrderSet() const;
+                
+                /*!
+                 * Retrieves the exploration order if it was set.
+                 *
+                 * @return The chosen exploration order.
+                 */
+                storm::builder::ExplorationOrder getExplorationOrder() const;
 
                 /*!
                  * Retrieves whether the property option was set.
@@ -389,6 +404,8 @@ namespace storm {
                 static const std::string explicitOptionShortName;
                 static const std::string symbolicOptionName;
                 static const std::string symbolicOptionShortName;
+                static const std::string explorationOrderOptionName;
+                static const std::string explorationOrderOptionShortName;
                 static const std::string propertyOptionName;
                 static const std::string propertyOptionShortName;
                 static const std::string transitionRewardsOptionName;

src/storage/BitVector.cpp

@@ -66,11 +66,11 @@ namespace storm {
             return currentIndex == other.currentIndex;
         }
 
-        BitVector::BitVector() : bitCount(0), bucketVector() {
+        BitVector::BitVector() : bitCount(0), buckets(nullptr) {
             // Intentionally left empty.
         }
 
-        BitVector::BitVector(uint_fast64_t length, bool init) : bitCount(length) {
+        BitVector::BitVector(uint_fast64_t length, bool init) : bitCount(length), buckets(nullptr) {
             // Compute the correct number of buckets needed to store the given number of bits.
             uint_fast64_t bucketCount = length >> 6;
             if ((length & mod64mask) != 0) {
@@ -79,10 +79,17 @@ namespace storm {
 
             // Initialize the storage with the required values.
             if (init) {
-                bucketVector = std::vector<uint64_t>(bucketCount, -1ll);
+                buckets = new uint64_t[bucketCount];
+                std::fill_n(buckets, bucketCount, -1ull);
                 truncateLastBucket();
             } else {
-                bucketVector = std::vector<uint64_t>(bucketCount, 0);
+                buckets = new uint64_t[bucketCount]();
+            }
+        }
+        
+        BitVector::~BitVector() {
+            if (buckets != nullptr) {
+                delete buckets;
             }
             
         }
@@ -96,23 +103,22 @@ namespace storm {
             // Intentionally left empty.
         }
 
-        BitVector::BitVector(uint_fast64_t bucketCount, uint_fast64_t bitCount) : bitCount(bitCount), bucketVector(bucketCount) {
+        BitVector::BitVector(uint_fast64_t bucketCount, uint_fast64_t bitCount) : bitCount(bitCount), buckets(nullptr) {
             STORM_LOG_ASSERT((bucketCount << 6) == bitCount, "Bit count does not match number of buckets.");
+            buckets = new uint64_t[bucketCount]();
         }
 
-        BitVector::BitVector(BitVector const& other) : bitCount(other.bitCount), bucketVector(other.bucketVector) {
-            // Intentionally left empty.
+        BitVector::BitVector(BitVector const& other) : bitCount(other.bitCount), buckets(nullptr) {
+            buckets = new uint64_t[other.bucketCount()];
+            std::copy_n(other.buckets, other.bucketCount(), buckets);
         }
 
-        //BitVector::BitVector(BitVector&& other) : bitCount(other.bitCount), bucketVector(std::move(other.bucketVector)) {
-        // Intentionally left empty.
-        //}
-
         BitVector& BitVector::operator=(BitVector const& other) {
             // Only perform the assignment if the source and target are not identical.
             if (this != &other) {
                 bitCount = other.bitCount;
-                bucketVector = std::vector<uint64_t>(other.bucketVector);
+                buckets = new uint64_t[other.bucketCount()];
+                std::copy_n(other.buckets, other.bucketCount(), buckets);
             }
             return *this;
         }
@@ -124,9 +130,9 @@ namespace storm {
                 return false;
             }
 
-            std::vector<uint64_t>::const_iterator first1 = this->bucketVector.begin();
-            std::vector<uint64_t>::const_iterator last1 = this->bucketVector.end();
-            std::vector<uint64_t>::const_iterator first2 = other.bucketVector.begin();
+            uint64_t* first1 = this->buckets;
+            uint64_t* last1 = this->buckets + this->bucketCount();
+            uint64_t* first2 = other.buckets;
 
             for (; first1 != last1; ++first1, ++first2) {
                 if (*first1 < *first2) {
@@ -137,12 +143,18 @@ namespace storm {
             }
             return false;
         }
+        
+        BitVector::BitVector(BitVector&& other) : bitCount(other.bitCount), buckets(other.buckets) {
+            other.bitCount = 0;
+            other.buckets = nullptr;
+        }
 
         BitVector& BitVector::operator=(BitVector&& other) {
             // Only perform the assignment if the source and target are not identical.
             if (this != &other) {
                 bitCount = other.bitCount;
-                bucketVector = std::move(other.bucketVector);
+                this->buckets = other.buckets;
+                other.buckets = nullptr;
             }
 
             return *this;
@@ -153,14 +165,7 @@ namespace storm {
             if (this->bitCount != other.bitCount) return false;
 
             // If the lengths match, we compare the buckets one by one.
-            for (std::vector<uint64_t>::const_iterator it1 = bucketVector.begin(), it2 = other.bucketVector.begin(); it1 != bucketVector.end(); ++it1, ++it2) {
-                if (*it1 != *it2) {
-                    return false;
-                }
-            }
-
-            // All buckets were equal, so the bit vectors are equal.
-            return true;
+            return std::equal(this->buckets, this->buckets + this->bucketCount(), other.buckets);
         }
 
         bool BitVector::operator!=(BitVector const& other) const {
@@ -173,9 +178,9 @@ namespace storm {
 
             uint64_t mask = 1ull << (63 - (index & mod64mask));
             if (value) {
-                bucketVector[bucket] |= mask;
+                buckets[bucket] |= mask;
             } else {
-                bucketVector[bucket] &= ~mask;
+                buckets[bucket] &= ~mask;
             }
         }
 
@@ -189,7 +194,7 @@ namespace storm {
         bool BitVector::operator[](uint_fast64_t index) const {
             uint64_t bucket = index >> 6;
             uint64_t mask = 1ull << (63 - (index & mod64mask));
-            return (this->bucketVector[bucket] & mask) == mask;
+            return (this->buckets[bucket] & mask) == mask;
         }
 
         bool BitVector::get(uint_fast64_t index) const {
@@ -204,89 +209,80 @@ namespace storm {
                     ++newBucketCount;
                 }
 
-                if (newBucketCount > bucketVector.size()) {
+                if (newBucketCount > this->bucketCount()) {
+                    uint64_t* newBuckets = new uint64_t[newBucketCount];
+                    std::copy_n(buckets, this->bucketCount(), newBuckets);
                     if (init) {
-                        bucketVector.back() |= ((1ull << (64 - (bitCount & mod64mask))) - 1ull);
-                        bucketVector.resize(newBucketCount, -1ull);
+                        newBuckets[this->bucketCount() - 1] |= ((1ull << (64 - (bitCount & mod64mask))) - 1ull);
+                        std::fill_n(newBuckets + this->bucketCount(), newBucketCount - this->bucketCount(), -1ull);
                     } else {
-                        bucketVector.resize(newBucketCount, 0);
+                        std::fill_n(newBuckets + this->bucketCount(), newBucketCount - this->bucketCount(), 0);
+                    }
+                    if (buckets != nullptr) {
+                        delete buckets;
                     }
+                    buckets = newBuckets;
                     bitCount = newLength;
                 } else {
                     // If the underlying storage does not need to grow, we have to insert the missing bits.
                     if (init) {
-                        bucketVector.back() |= ((1ull << (64 - (bitCount & mod64mask))) - 1ull);
+                        buckets[this->bucketCount() - 1] |= ((1ull << (64 - (bitCount & mod64mask))) - 1ull);
                     }
                     bitCount = newLength;
                 }
                 truncateLastBucket();
             } else {
-                bitCount = newLength;
                 uint_fast64_t newBucketCount = newLength >> 6;
                 if ((newLength & mod64mask) != 0) {
                     ++newBucketCount;
                 }
 
-                bucketVector.resize(newBucketCount);
+                // If the number of buckets needs to be reduced, we resize it now. Otherwise, we can just truncate the
+                // last bucket.
+                if (newBucketCount < this->bucketCount()) {
+                    uint64_t* newBuckets = new uint64_t[newBucketCount];
+                    std::copy_n(buckets, newBucketCount, newBuckets);
+                    if (buckets != nullptr) {
+                        delete buckets;
+                    }
+                    buckets = newBuckets;
+                    bitCount = newLength;
+                }
+                bitCount = newLength;
                 truncateLastBucket();
             }
         }
 
         BitVector BitVector::operator&(BitVector const& other) const {
             STORM_LOG_ASSERT(bitCount == other.bitCount, "Length of the bit vectors does not match.");
-
             BitVector result(bitCount);
-            std::vector<uint64_t>::iterator it = result.bucketVector.begin();
-            for (std::vector<uint64_t>::const_iterator it1 = bucketVector.begin(), it2 = other.bucketVector.begin(); it != result.bucketVector.end(); ++it1, ++it2, ++it) {
-                *it = *it1 & *it2;
-            }
-
+            std::transform(this->buckets, this->buckets + this->bucketCount(), other.buckets, result.buckets, [] (uint64_t const& a, uint64_t const& b) { return a & b; });
             return result;
         }
 
         BitVector& BitVector::operator&=(BitVector const& other) {
             STORM_LOG_ASSERT(bitCount == other.bitCount, "Length of the bit vectors does not match.");
-
-            std::vector<uint64_t>::iterator it = bucketVector.begin();
-            for (std::vector<uint64_t>::const_iterator otherIt = other.bucketVector.begin(); it != bucketVector.end() && otherIt != other.bucketVector.end(); ++it, ++otherIt) {
-                *it &= *otherIt;
-            }
-
+            std::transform(this->buckets, this->buckets + this->bucketCount(), other.buckets, this->buckets, [] (uint64_t const& a, uint64_t const& b) { return a & b; });
             return *this;
         }
 
         BitVector BitVector::operator|(BitVector const& other) const {
             STORM_LOG_ASSERT(bitCount == other.bitCount, "Length of the bit vectors does not match.");
-
             BitVector result(bitCount);
-            std::vector<uint64_t>::iterator it = result.bucketVector.begin();
-            for (std::vector<uint64_t>::const_iterator it1 = bucketVector.begin(), it2 = other.bucketVector.begin(); it != result.bucketVector.end(); ++it1, ++it2, ++it) {
-                *it = *it1 | *it2;
-            }
-
+            std::transform(this->buckets, this->buckets + this->bucketCount(), other.buckets, result.buckets, [] (uint64_t const& a, uint64_t const& b) { return a | b; });
             return result;
         }
 
         BitVector& BitVector::operator|=(BitVector const& other) {
             STORM_LOG_ASSERT(bitCount == other.bitCount, "Length of the bit vectors does not match.");
-
-            std::vector<uint64_t>::iterator it = bucketVector.begin();
-            for (std::vector<uint64_t>::const_iterator otherIt = other.bucketVector.begin(); it != bucketVector.end() && otherIt != other.bucketVector.end(); ++it, ++otherIt) {
-                *it |= *otherIt;
-            }
-
+            std::transform(this->buckets, this->buckets + this->bucketCount(), other.buckets, this->buckets, [] (uint64_t const& a, uint64_t const& b) { return a | b; });
             return *this;
         }
 
         BitVector BitVector::operator^(BitVector const& other) const {
             STORM_LOG_ASSERT(bitCount == other.bitCount, "Length of the bit vectors does not match.");
-
             BitVector result(bitCount);
-            std::vector<uint64_t>::iterator it = result.bucketVector.begin();
-            for (std::vector<uint64_t>::const_iterator it1 = bucketVector.begin(), it2 = other.bucketVector.begin(); it != result.bucketVector.end(); ++it1, ++it2, ++it) {
-                *it = *it1 ^ *it2;
-            }
-
+            std::transform(this->buckets, this->buckets + this->bucketCount(), other.buckets, result.buckets, [] (uint64_t const& a, uint64_t const& b) { return a ^ b; });
             result.truncateLastBucket();
             return result;
         }
@@ -321,19 +317,13 @@ namespace storm {
 
         BitVector BitVector::operator~() const {
             BitVector result(this->bitCount);
-            std::vector<uint64_t>::iterator it = result.bucketVector.begin();
-            for (std::vector<uint64_t>::const_iterator it1 = bucketVector.begin(); it != result.bucketVector.end(); ++it1, ++it) {
-                *it = ~(*it1);
-            }
-
+            std::transform(this->buckets, this->buckets + this->bucketCount(), result.buckets, [] (uint64_t const& a) { return ~a; });
             result.truncateLastBucket();
             return result;
         }
 
         void BitVector::complement() {
-            for (auto& element : bucketVector) {
-                element = ~element;
-            }
+            std::transform(this->buckets, this->buckets + this->bucketCount(), this->buckets, [] (uint64_t const& a) { return ~a; });
             truncateLastBucket();
         }
 
@@ -341,11 +331,7 @@ namespace storm {
             STORM_LOG_ASSERT(bitCount == other.bitCount, "Length of the bit vectors does not match.");
 
             BitVector result(bitCount);
-            std::vector<uint64_t>::iterator it = result.bucketVector.begin();
-            for (std::vector<uint64_t>::const_iterator it1 = bucketVector.begin(), it2 = other.bucketVector.begin(); it != result.bucketVector.end(); ++it1, ++it2, ++it) {
-                *it = ~(*it1) | *it2;
-            }
-
+            std::transform(this->buckets, this->buckets + this->bucketCount(), other.buckets, result.buckets, [] (uint64_t const& a, uint64_t const& b) { return (~a | b); });
             result.truncateLastBucket();
             return result;
         }
@@ -353,7 +339,11 @@ namespace storm {
         bool BitVector::isSubsetOf(BitVector const& other) const {
             STORM_LOG_ASSERT(bitCount == other.bitCount, "Length of the bit vectors does not match.");
 
-            for (std::vector<uint64_t>::const_iterator it1 = bucketVector.begin(), it2 = other.bucketVector.begin(); it1 != bucketVector.end(); ++it1, ++it2) {
+            uint64_t const* it1 = buckets;
+            uint64_t const* ite1 = buckets + bucketCount();
+            uint64_t const* it2 = other.buckets;
+            
+            for (; it1 != ite1; ++it1, ++it2) {
                 if ((*it1 & *it2) != *it1) {
                     return false;
                 }
@@ -364,7 +354,11 @@ namespace storm {
         bool BitVector::isDisjointFrom(BitVector const& other) const {
             STORM_LOG_ASSERT(bitCount == other.bitCount, "Length of the bit vectors does not match.");
 
-            for (std::vector<uint64_t>::const_iterator it1 = bucketVector.begin(), it2 = other.bucketVector.begin(); it1 != bucketVector.end(); ++it1, ++it2) {
+            uint64_t const* it1 = buckets;
+            uint64_t const* ite1 = buckets + bucketCount();
+            uint64_t const* it2 = other.buckets;
+            
+            for (; it1 != ite1; ++it1, ++it2) {
                 if ((*it1 & *it2) != 0) {
                     return false;
                 }
@@ -379,9 +373,9 @@ namespace storm {
             // Compute the first bucket that needs to be checked and the number of buckets.
             uint64_t index = bitIndex >> 6;
 
-            std::vector<uint64_t>::const_iterator first1 = bucketVector.begin() + index;
-            std::vector<uint64_t>::const_iterator first2 = other.bucketVector.begin();
-            std::vector<uint64_t>::const_iterator last2 = other.bucketVector.end();
+            uint64_t const* first1 = buckets + index;
+            uint64_t const* first2 = other.buckets;
+            uint64_t const* last2 = other.buckets + other.bucketCount();
 
             for (; first2 != last2; ++first1, ++first2) {
                 if (*first1 != *first2) {
@@ -398,10 +392,10 @@ namespace storm {
             // Compute the first bucket that needs to be checked and the number of buckets.
             uint64_t index = bitIndex >> 6;
 
-            std::vector<uint64_t>::iterator first1 = bucketVector.begin() + index;
-            std::vector<uint64_t>::const_iterator first2 = other.bucketVector.begin();
-            std::vector<uint64_t>::const_iterator last2 = other.bucketVector.end();
-
+            uint64_t* first1 = buckets + index;
+            uint64_t const* first2 = other.buckets;
+            uint64_t const* last2 = other.buckets + other.bucketCount();
+            
             for (; first2 != last2; ++first1, ++first2) {
                 *first1 = *first2;
             }
@@ -413,8 +407,8 @@ namespace storm {
             STORM_LOG_ASSERT(index + numberOfBuckets <= this->bucketCount(), "Argument is out-of-range.");
 
             storm::storage::BitVector result(numberOfBuckets, numberOfBits);
-            std::copy(this->bucketVector.begin() + index, this->bucketVector.begin() + index + numberOfBuckets, result.bucketVector.begin());
-
+            std::copy(this->buckets + index, this->buckets + index + numberOfBuckets, result.buckets);
+            result.truncateLastBucket();
             return result;
         }
 
@@ -433,10 +427,10 @@ namespace storm {
             if (bitIndexInBucket + numberOfBits < 64) {
                 // If the value stops before the end of the bucket, we need to erase some lower bits.
                 mask &= ~((1ull << (64 - (bitIndexInBucket + numberOfBits))) - 1ull);
-                return (bucketVector[bucket] & mask) >> (64 - (bitIndexInBucket + numberOfBits));
+                return (buckets[bucket] & mask) >> (64 - (bitIndexInBucket + numberOfBits));
             } else if (bitIndexInBucket + numberOfBits > 64) {
                 // In this case, the integer "crosses" the bucket line.
-                uint64_t result = (bucketVector[bucket] & mask);
+                uint64_t result = (buckets[bucket] & mask);
                 ++bucket;
 
                 // Compute the remaining number of bits.
@@ -448,13 +442,13 @@ namespace storm {
                 // Strip away everything from the second bucket that is beyond the final index and add it to the
                 // intermediate result.
                 mask = ~((1ull << (64 - numberOfBits)) - 1ull);
-                uint64_t lowerBits = bucketVector[bucket] & mask;
+                uint64_t lowerBits = buckets[bucket] & mask;
                 result |= (lowerBits >> (64 - numberOfBits));
 
                 return result;
             } else {
                 // In this case, it suffices to take the current mask.
-                return bucketVector[bucket] & mask;
+                return buckets[bucket] & mask;
             }
         }
         
@@ -498,10 +492,10 @@ namespace storm {
             if (bitIndexInBucket + numberOfBits < 64) {
                 // If the value stops before the end of the bucket, we need to erase some lower bits.
                 mask &= ~((1ull << (64 - (bitIndexInBucket + numberOfBits))) - 1ull);
-                bucketVector[bucket] = (bucketVector[bucket] & ~mask) | (value << (64 - (bitIndexInBucket + numberOfBits)));
+                buckets[bucket] = (buckets[bucket] & ~mask) | (value << (64 - (bitIndexInBucket + numberOfBits)));
             } else if (bitIndexInBucket + numberOfBits > 64) {
                 // Write the part of the value that falls into the first bucket.
-                bucketVector[bucket] = (bucketVector[bucket] & ~mask) | (value >> (numberOfBits + (bitIndexInBucket - 64)));
+                buckets[bucket] = (buckets[bucket] & ~mask) | (value >> (numberOfBits + (bitIndexInBucket - 64)));
                 ++bucket;
 
                 // Compute the remaining number of bits.
@@ -512,45 +506,41 @@ namespace storm {
 
                 // Put the remaining bits in their place.
                 mask = ((1ull << (64 - numberOfBits)) - 1ull);
-                bucketVector[bucket] = (bucketVector[bucket] & mask) | value;
+                buckets[bucket] = (buckets[bucket] & mask) | value;
             } else {
-                bucketVector[bucket] = (bucketVector[bucket] & ~mask) | value;
+                buckets[bucket] = (buckets[bucket] & ~mask) | value;
             }
         }
 
         bool BitVector::empty() const {
-            for (auto& element : bucketVector) {
-                if (element != 0) {
-                    return false;
-                }
-            }
-            return true;
+            uint64_t* last = buckets + bucketCount();
+            uint64_t* it = std::find_if(buckets, last, [] (uint64_t const& a) { return a != 0; });
+            return it == last;
         }
 
         bool BitVector::full() const {
             // Check that all buckets except the last one have all bits set.
-            for (uint_fast64_t index = 0; index < bucketVector.size() - 1; ++index) {
-                if (bucketVector[index] != -1ull) {
+            uint64_t* last = buckets + bucketCount() - 1;
+            for (uint64_t const* it = buckets; it < last; ++it) {
+                if (*it != -1ull) {
                     return false;
                 }
             }
-
+            
             // Now check whether the relevant bits are set in the last bucket.
             uint64_t mask = ~((1ull << (64 - (bitCount & mod64mask))) - 1ull);
-            if ((bucketVector.back() & mask) != mask) {
+            if ((*last & mask) != mask) {
                 return false;
             }
             return true;
         }
 
         void BitVector::clear() {
-            for (auto& element : bucketVector) {
-                element = 0;
-            }
+            std::fill_n(buckets, this->bucketCount(), 0);
         }
 
         uint_fast64_t BitVector::getNumberOfSetBits() const {
-            return getNumberOfSetBitsBeforeIndex(bucketVector.size() << 6);
+            return getNumberOfSetBitsBeforeIndex(bitCount);
         }
 
         uint_fast64_t BitVector::getNumberOfSetBitsBeforeIndex(uint_fast64_t index) const {
@@ -561,14 +551,14 @@ namespace storm {
             for (uint_fast64_t i = 0; i < bucket; ++i) {
                 // Check if we are using g++ or clang++ and, if so, use the built-in function
 #if (defined (__GNUG__) || defined(__clang__))
-                result += __builtin_popcountll(bucketVector[i]);
+                result += __builtin_popcountll(buckets[i]);
 #elif defined WINDOWS
 #include <nmmintrin.h>
                 // If the target machine does not support SSE4, this will fail.
                 result += _mm_popcnt_u64(bucketVector[i]);
 #else
                 uint_fast32_t cnt;
-                uint_fast64_t bitset = bucketVector[i];
+                uint_fast64_t bitset = buckets[i];
                 for (cnt = 0; bitset; cnt++) {
                     bitset &= bitset - 1;
                 }
@@ -580,7 +570,7 @@ namespace storm {
             uint64_t tmp = index & mod64mask;
             if (tmp != 0) {
                 tmp = ~((1ll << (64 - (tmp & mod64mask))) - 1ll);
-                tmp &= bucketVector[bucket];
+                tmp &= buckets[bucket];
                 // Check if we are using g++ or clang++ and, if so, use the built-in function
 #if (defined (__GNUG__) || defined(__clang__))
                 result += __builtin_popcountll(tmp);
@@ -617,19 +607,19 @@ namespace storm {
         }
 
         std::size_t BitVector::getSizeInBytes() const {
-            return sizeof (*this) + sizeof (uint64_t) * bucketVector.size();
+            return sizeof (*this) + sizeof (uint64_t) * bucketCount();
         }
 
         BitVector::const_iterator BitVector::begin() const {
-            return const_iterator(bucketVector.data(), 0, bitCount);
+            return const_iterator(buckets, 0, bitCount);
         }
 
         BitVector::const_iterator BitVector::end() const {
-            return const_iterator(bucketVector.data(), bitCount, bitCount, false);
+            return const_iterator(buckets, bitCount, bitCount, false);
         }
 
         uint_fast64_t BitVector::getNextSetIndex(uint_fast64_t startingIndex) const {
-            return getNextSetIndex(bucketVector.data(), startingIndex, bitCount);
+            return getNextSetIndex(buckets, startingIndex, bitCount);
         }
 
         uint_fast64_t BitVector::getNextSetIndex(uint64_t const* dataPtr, uint_fast64_t startingIndex, uint_fast64_t endIndex) {
@@ -903,17 +893,21 @@ namespace storm {
 
         void BitVector::truncateLastBucket() {
             if ((bitCount & mod64mask) != 0) {
-                bucketVector.back() &= ~((1ll << (64 - (bitCount & mod64mask))) - 1ll);
+                buckets[bucketCount() - 1] &= ~((1ll << (64 - (bitCount & mod64mask))) - 1ll);
             }
         }
 
         size_t BitVector::bucketCount() const {
-            return bucketVector.size();
+            size_t result = (bitCount >> 6);
+            if ((bitCount & mod64mask) != 0) {
+                ++result;
+            }
+            return result;
         }
 
-        std::ostream& operator<<(std::ostream& out, BitVector const& bitVector) {
-            out << "bit vector(" << bitVector.getNumberOfSetBits() << "/" << bitVector.bitCount << ") [";
-            for (auto index : bitVector) {
+        std::ostream& operator<<(std::ostream& out, BitVector const& bitvector) {
+            out << "bit vector(" << bitvector.getNumberOfSetBits() << "/" << bitvector.bitCount << ") [";
+            for (auto index : bitvector) {
                 out << index << " ";
             }
             out << "]";
@@ -941,13 +935,13 @@ namespace storm {
             out << std::endl;
         }
 
-        std::size_t NonZeroBitVectorHash::operator()(storm::storage::BitVector const& bv) const {
-            STORM_LOG_ASSERT(bv.size() > 0, "Cannot hash bit vector of zero size.");
+        std::size_t NonZeroBitVectorHash::operator()(storm::storage::BitVector const& bitvector) const {
+            STORM_LOG_ASSERT(bitvector.size() > 0, "Cannot hash bit vector of zero size.");
             std::size_t result = 0;
 
-            for (uint_fast64_t index = 0; index < bv.bucketVector.size(); ++index) {
+            for (uint_fast64_t index = 0; index < bitvector.bucketCount(); ++index) {
                 result ^= result << 3;
-                result ^= result >> bv.getAsInt(index << 6, 5);
+                result ^= result >> bitvector.getAsInt(index << 6, 5);
             }
 
             // Erase the last bit and add one to definitely make this hash value non-zero.
@@ -971,7 +965,7 @@ namespace storm {
 
 namespace std {
 
-    std::size_t hash<storm::storage::BitVector>::operator()(storm::storage::BitVector const& bv) const {
-        return boost::hash_range(bv.bucketVector.begin(), bv.bucketVector.end());
+    std::size_t hash<storm::storage::BitVector>::operator()(storm::storage::BitVector const& bitvector) const {
+        return boost::hash_range(bitvector.buckets, bitvector.buckets + bitvector.bucketCount());
     }
 }

src/storage/BitVector.h

@@ -104,6 +104,11 @@ namespace storm {
              */
             BitVector();
             
+            /*
+             * Deconstructs a bit vector by deleting the underlying storage.
+             */
+            ~BitVector();
+            
             /*!
              * Constructs a bit vector which can hold the given number of bits and initializes all bits with the
              * provided truth value.
@@ -141,7 +146,7 @@ namespace storm {
              *
              * @param other The bit vector from which to move-construct.
              */
-            BitVector(BitVector&& other) = default;
+            BitVector(BitVector&& other);
             
             /*!
              * Compares the given bit vector with the current one.
@@ -537,7 +542,7 @@ namespace storm {
             uint_fast64_t bitCount;
             
             // The underlying storage of 64-bit buckets for all bits of this bit vector.
-            std::vector<uint64_t> bucketVector;
+            uint64_t* buckets;
             
             // A bit mask that can be used to reduce a modulo 64 operation to a logical "and".
             static const uint_fast64_t mod64mask = (1 << 6) - 1;

src/storage/BitVectorHashMap.cpp

@@ -42,7 +42,7 @@ namespace storm {
         std::pair<storm::storage::BitVector, ValueType> BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator::operator*() const {
             return map.getBucketAndValue(*indexIt);
         }
-        
+                
         template<class ValueType, class Hash1, class Hash2>
         BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMap(uint64_t bucketSize, uint64_t initialSize, double loadFactor) : loadFactor(loadFactor), bucketSize(bucketSize), numberOfElements(0) {
             STORM_LOG_ASSERT(bucketSize % 64 == 0, "Bucket size must be a multiple of 64.");
@@ -264,6 +264,13 @@ namespace storm {
             return std::make_pair(buckets.get(bucket * bucketSize, bucketSize), values[bucket]);
         }
         
+        template<class ValueType, class Hash1, class Hash2>
+        void BitVectorHashMap<ValueType, Hash1, Hash2>::remap(std::function<ValueType(ValueType const&)> const& remapping) {
+            for (auto pos : occupied) {
+                values[pos] = remapping(values[pos]);
+            }
+        }
+        
         template class BitVectorHashMap<uint_fast64_t>;
         template class BitVectorHashMap<uint32_t>;
     }

src/storage/BitVectorHashMap.h

@@ -55,7 +55,7 @@ namespace storm {
              * @param loadFactor The load factor that determines at which point the size of the underlying storage is
              * increased.
              */
-            BitVectorHashMap(uint64_t bucketSize, uint64_t initialSize, double loadFactor = 0.75);
+            BitVectorHashMap(uint64_t bucketSize = 64, uint64_t initialSize = 1000, double loadFactor = 0.75);
             
             /*!
              * Searches for the given key in the map. If it is found, the mapped-to value is returned. Otherwise, the
@@ -150,6 +150,13 @@ namespace storm {
              */
             std::size_t capacity() const;
             
+            /*!
+             * Performs a remapping of all values stored by applying the given remapping.
+             *
+             * @param remapping The remapping to apply.
+             */
+            void remap(std::function<ValueType(ValueType const&)> const& remapping);
+            
         private:
             /*!
              * Retrieves whether the given bucket holds a value.

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,44 @@ 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>::const_iterator Distribution<ValueType, StateType>::cbegin() const {
+            return this->begin();
+        }
+        
+        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, typename StateType>
+        typename Distribution<ValueType, StateType>::const_iterator Distribution<ValueType, StateType>::cend() const {
+            return this->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 +111,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 +127,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 = uint32_t>
         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;
             
@@ -43,7 +43,7 @@ namespace storm {
              * @param other The distribution with which the current distribution is to be compared.
              * @return True iff the two distributions are equal.
              */
-            bool equals(Distribution<ValueType> const& other, storm::utility::ConstantsComparator<ValueType> const& comparator = storm::utility::ConstantsComparator<ValueType>()) const;
+            bool equals(Distribution<ValueType, StateType> const& other, storm::utility::ConstantsComparator<ValueType> const& comparator = storm::utility::ConstantsComparator<ValueType>()) const;
             
             /*!
              * Assigns the given state the given probability under this distribution.
@@ -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,8 +72,8 @@ 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.
              *
@@ -88,6 +88,13 @@ namespace storm {
              */
             const_iterator begin() const;
             
+            /*!
+             * Retrieves an iterator to the elements in this distribution.
+             *
+             * @return The iterator to the elements in this distribution.
+             */
+            const_iterator cbegin() const;
+            
             /*!
              * Retrieves an iterator past the elements in this distribution.
              *
@@ -102,6 +109,13 @@ namespace storm {
              */
             const_iterator end() const;
             
+            /*!
+             * Retrieves an iterator past the elements in this distribution.
+             *
+             * @return The iterator past the elements in this distribution.
+             */
+            const_iterator cend() const;
+            
             /*!
              * Scales the distribution by multiplying all the probabilities with 1/p where p is the probability of moving
              * to the given state and sets the probability of moving to the given state to zero. If the probability is
@@ -109,22 +123,22 @@ 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.
              */
             std::size_t size() const;
             
-            bool less(Distribution<ValueType> const& other, storm::utility::ConstantsComparator<ValueType> const& comparator) const;
+            bool less(Distribution<ValueType, StateType> const& other, storm::utility::ConstantsComparator<ValueType> const& comparator) const;
             
         private:
             // A list of states and the probabilities that are assigned to them.
             container_type distribution;
         };
         
-        template<typename ValueType>
-        std::ostream& operator<<(std::ostream& out, Distribution<ValueType> const& distribution);
+        template<typename ValueType, typename StateType = uint32_t>
+        std::ostream& operator<<(std::ostream& out, Distribution<ValueType, StateType> const& distribution);
     }
 }
 

src/storage/SparseMatrix.cpp

@@ -80,20 +80,23 @@ namespace storm {
             if (initialEntryCountSet) {
                 columnsAndValues.reserve(initialEntryCount);
             }
-            if (initialRowGroupCountSet) {
-                rowGroupIndices.reserve(initialRowGroupCount + 1);
+            if (hasCustomRowGrouping) {
+                rowGroupIndices = std::vector<index_type>();
+            }
+            if (initialRowGroupCountSet && hasCustomRowGrouping) {
+                rowGroupIndices.get().reserve(initialRowGroupCount + 1);
             }
             rowIndications.push_back(0);
         }
         
         template<typename ValueType>
-        SparseMatrixBuilder<ValueType>::SparseMatrixBuilder(SparseMatrix<ValueType>&& matrix) :  initialRowCountSet(false), initialRowCount(0), initialColumnCountSet(false), initialColumnCount(0), initialEntryCountSet(false), initialEntryCount(0), forceInitialDimensions(false), hasCustomRowGrouping(matrix.nontrivialRowGrouping), initialRowGroupCountSet(false), initialRowGroupCount(0), rowGroupIndices(), columnsAndValues(std::move(matrix.columnsAndValues)), rowIndications(std::move(matrix.rowIndications)), currentEntryCount(matrix.entryCount), lastRow(matrix.rowCount - 1), lastColumn(columnsAndValues.back().getColumn()), highestColumn(matrix.getColumnCount() - 1), currentRowGroup() {
+        SparseMatrixBuilder<ValueType>::SparseMatrixBuilder(SparseMatrix<ValueType>&& matrix) :  initialRowCountSet(false), initialRowCount(0), initialColumnCountSet(false), initialColumnCount(0), initialEntryCountSet(false), initialEntryCount(0), forceInitialDimensions(false), hasCustomRowGrouping(!matrix.trivialRowGrouping), initialRowGroupCountSet(false), initialRowGroupCount(0), rowGroupIndices(), columnsAndValues(std::move(matrix.columnsAndValues)), rowIndications(std::move(matrix.rowIndications)), currentEntryCount(matrix.entryCount), lastRow(matrix.rowCount - 1), lastColumn(columnsAndValues.back().getColumn()), highestColumn(matrix.getColumnCount() - 1), currentRowGroup() {
             
             // If the matrix has a custom row grouping, we move it and remove the last element to make it 'open' again.
             if (hasCustomRowGrouping) {
                 rowGroupIndices = std::move(matrix.rowGroupIndices);
-                rowGroupIndices.pop_back();
-                currentRowGroup = rowGroupIndices.size() - 1;
+                rowGroupIndices.get().pop_back();
+                currentRowGroup = rowGroupIndices.get().size() - 1;
             }
             
             // Likewise, we need to 'open' the row indications again.
@@ -141,14 +144,14 @@ namespace storm {
         void SparseMatrixBuilder<ValueType>::newRowGroup(index_type startingRow) {
             STORM_LOG_THROW(hasCustomRowGrouping, storm::exceptions::InvalidStateException, "Matrix was not created to have a custom row grouping.");
             STORM_LOG_THROW(startingRow >= lastRow, storm::exceptions::InvalidStateException, "Illegal row group with negative size.");
-            rowGroupIndices.push_back(startingRow);
+            rowGroupIndices.get().push_back(startingRow);
             ++currentRowGroup;
-
+            
             // Close all rows from the most recent one to the starting row.
             for (index_type i = lastRow + 1; i <= startingRow; ++i) {
                 rowIndications.push_back(currentEntryCount);
             }
-
+            
             // Reset the most recently seen row/column to allow for proper insertion of the following elements.
             lastRow = startingRow;
             lastColumn = 0;
@@ -162,7 +165,7 @@ namespace storm {
                 rowCount = std::max(rowCount, initialRowCount);
             }
             rowCount = std::max(rowCount, overriddenRowCount);
-
+            
             // If the current row count was overridden, we may need to add empty rows.
             for (index_type i = lastRow + 1; i < rowCount; ++i) {
                 rowIndications.push_back(currentEntryCount);
@@ -186,11 +189,7 @@ namespace storm {
             }
             
             // Check whether row groups are missing some entries.
-            if (!hasCustomRowGrouping) {
-                for (index_type i = 0; i <= rowCount; ++i) {
-                    rowGroupIndices.push_back(i);
-                }
-            } else {
+            if (hasCustomRowGrouping) {
                 uint_fast64_t rowGroupCount = currentRowGroup;
                 if (initialRowGroupCountSet && forceInitialDimensions) {
                     STORM_LOG_THROW(rowGroupCount <= initialRowGroupCount, storm::exceptions::InvalidStateException, "Expected not more than " << initialRowGroupCount << " row groups, but got " << rowGroupCount << ".");
@@ -199,11 +198,11 @@ namespace storm {
                 rowGroupCount = std::max(rowGroupCount, overriddenRowGroupCount);
                 
                 for (index_type i = currentRowGroup; i <= rowGroupCount; ++i) {
-                    rowGroupIndices.push_back(rowCount);
+                    rowGroupIndices.get().push_back(rowCount);
                 }
             }
-
-            return SparseMatrix<ValueType>(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices), hasCustomRowGrouping);
+            
+            return SparseMatrix<ValueType>(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices));
         }
         
         template<typename ValueType>
@@ -283,6 +282,44 @@ namespace storm {
             }
         }
         
+        template<typename ValueType>
+        bool SparseMatrixBuilder<ValueType>::replaceColumns(std::vector<index_type> const& replacements, index_type offset) {
+            bool matrixChanged = false;
+            
+            // Walk through all rows.
+            for (index_type row = 0; row < rowIndications.size(); ++row) {
+                bool rowChanged = false;
+                index_type rowEnd = row < rowIndications.size()-1 ? rowIndications[row+1] : columnsAndValues.size();
+                
+                for (auto it = columnsAndValues.begin() + rowIndications[row], ite = columnsAndValues.begin() + rowEnd; it != ite; ++it) {
+                    if (it->getColumn() >= offset && it->getColumn() != replacements[it->getColumn() - offset]) {
+                        it->setColumn(replacements[it->getColumn() - offset]);
+                        rowChanged = true;
+                    }
+                    // Update highest column in a way that only works if the highest appearing index does not become
+                    // lower during performing the replacement.
+                    highestColumn = std::max(highestColumn, it->getColumn());
+                }
+                
+                if (rowChanged) {
+                    matrixChanged = true;
+                    
+                    // Sort the row.
+                    std::sort(columnsAndValues.begin() + rowIndications[row], columnsAndValues.begin() + rowEnd,
+                              [](MatrixEntry<index_type, value_type> const& a, MatrixEntry<index_type, value_type> const& b) {
+                                  return a.getColumn() < b.getColumn();
+                              });
+                    // Assert no equal elements
+                    STORM_LOG_ASSERT(std::is_sorted(columnsAndValues.begin() + rowIndications[row], columnsAndValues.begin() + rowEnd,
+                                                    [](MatrixEntry<index_type, value_type> const& a, MatrixEntry<index_type, value_type> const& b) {
+                                                        return a.getColumn() <= b.getColumn();
+                                                    }), "Must not have different elements with the same column in a row.");
+                }
+            }
+            
+            return matrixChanged;
+        }
+        
         template<typename ValueType>
         SparseMatrix<ValueType>::rows::rows(iterator begin, index_type entryCount) : beginIterator(begin), entryCount(entryCount) {
             // Intentionally left empty.
@@ -324,12 +361,12 @@ namespace storm {
         }
         
         template<typename ValueType>
-        SparseMatrix<ValueType>::SparseMatrix() : rowCount(0), columnCount(0), entryCount(0), nonzeroEntryCount(0), columnsAndValues(), rowIndications(), nontrivialRowGrouping(false), rowGroupIndices() {
+        SparseMatrix<ValueType>::SparseMatrix() : rowCount(0), columnCount(0), entryCount(0), nonzeroEntryCount(0), columnsAndValues(), rowIndications(), rowGroupIndices() {
             // Intentionally left empty.
         }
         
         template<typename ValueType>
-        SparseMatrix<ValueType>::SparseMatrix(SparseMatrix<ValueType> const& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), nonzeroEntryCount(other.nonzeroEntryCount), columnsAndValues(other.columnsAndValues), rowIndications(other.rowIndications), nontrivialRowGrouping(other.nontrivialRowGrouping), rowGroupIndices(other.rowGroupIndices) {
+        SparseMatrix<ValueType>::SparseMatrix(SparseMatrix<ValueType> const& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), nonzeroEntryCount(other.nonzeroEntryCount), columnsAndValues(other.columnsAndValues), rowIndications(other.rowIndications), trivialRowGrouping(other.trivialRowGrouping), rowGroupIndices(other.rowGroupIndices) {
             // Intentionally left empty.
         }
         
@@ -341,7 +378,7 @@ namespace storm {
         }
         
         template<typename ValueType>
-        SparseMatrix<ValueType>::SparseMatrix(SparseMatrix<ValueType>&& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), nonzeroEntryCount(other.nonzeroEntryCount), columnsAndValues(std::move(other.columnsAndValues)), rowIndications(std::move(other.rowIndications)), nontrivialRowGrouping(other.nontrivialRowGrouping), rowGroupIndices(std::move(other.rowGroupIndices)) {
+        SparseMatrix<ValueType>::SparseMatrix(SparseMatrix<ValueType>&& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), nonzeroEntryCount(other.nonzeroEntryCount), columnsAndValues(std::move(other.columnsAndValues)), rowIndications(std::move(other.rowIndications)), trivialRowGrouping(other.trivialRowGrouping), rowGroupIndices(std::move(other.rowGroupIndices)) {
             // Now update the source matrix
             other.rowCount = 0;
             other.columnCount = 0;
@@ -349,12 +386,12 @@ namespace storm {
         }
         
         template<typename ValueType>
-        SparseMatrix<ValueType>::SparseMatrix(index_type columnCount, std::vector<index_type> const& rowIndications, std::vector<MatrixEntry<index_type, ValueType>> const& columnsAndValues, std::vector<index_type> const& rowGroupIndices, bool nontrivialRowGrouping) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(columnsAndValues), rowIndications(rowIndications), nontrivialRowGrouping(nontrivialRowGrouping), rowGroupIndices(rowGroupIndices) {
+        SparseMatrix<ValueType>::SparseMatrix(index_type columnCount, std::vector<index_type> const& rowIndications, std::vector<MatrixEntry<index_type, ValueType>> const& columnsAndValues, boost::optional<std::vector<index_type>> const& rowGroupIndices) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(columnsAndValues), rowIndications(rowIndications), trivialRowGrouping(!rowGroupIndices), rowGroupIndices(rowGroupIndices) {
             this->updateNonzeroEntryCount();
         }
         
         template<typename ValueType>
-        SparseMatrix<ValueType>::SparseMatrix(index_type columnCount, std::vector<index_type>&& rowIndications, std::vector<MatrixEntry<index_type, ValueType>>&& columnsAndValues, std::vector<index_type>&& rowGroupIndices, bool nontrivialRowGrouping) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(std::move(columnsAndValues)), rowIndications(std::move(rowIndications)), nontrivialRowGrouping(nontrivialRowGrouping), rowGroupIndices(std::move(rowGroupIndices)) {
+        SparseMatrix<ValueType>::SparseMatrix(index_type columnCount, std::vector<index_type>&& rowIndications, std::vector<MatrixEntry<index_type, ValueType>>&& columnsAndValues, boost::optional<std::vector<index_type>>&& rowGroupIndices) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(std::move(columnsAndValues)), rowIndications(std::move(rowIndications)), trivialRowGrouping(!rowGroupIndices), rowGroupIndices(std::move(rowGroupIndices)) {
             this->updateNonzeroEntryCount();
         }
         
@@ -370,7 +407,7 @@ namespace storm {
                 columnsAndValues = other.columnsAndValues;
                 rowIndications = other.rowIndications;
                 rowGroupIndices = other.rowGroupIndices;
-                nontrivialRowGrouping = other.nontrivialRowGrouping;
+                trivialRowGrouping = other.trivialRowGrouping;
             }
             
             return *this;
@@ -388,7 +425,7 @@ namespace storm {
                 columnsAndValues = std::move(other.columnsAndValues);
                 rowIndications = std::move(other.rowIndications);
                 rowGroupIndices = std::move(other.rowGroupIndices);
-                nontrivialRowGrouping = other.nontrivialRowGrouping;
+                trivialRowGrouping = other.trivialRowGrouping;
             }
             
             return *this;
@@ -410,7 +447,11 @@ namespace storm {
             if (!equalityResult) {
                 return false;
             }
-            equalityResult &= this->getRowGroupIndices() == other.getRowGroupIndices();
+            if (!this->hasTrivialRowGrouping() && !other.hasTrivialRowGrouping()) {
+                equalityResult &= this->getRowGroupIndices() == other.getRowGroupIndices();
+            } else {
+                equalityResult &= this->hasTrivialRowGrouping() && other.hasTrivialRowGrouping();
+            }
             if (!equalityResult) {
                 return false;
             }
@@ -462,8 +503,12 @@ namespace storm {
         template<typename T>
         uint_fast64_t SparseMatrix<T>::getRowGroupEntryCount(uint_fast64_t const group) const {
             uint_fast64_t result = 0;
-            for (uint_fast64_t row = this->getRowGroupIndices()[group]; row < this->getRowGroupIndices()[group + 1]; ++row) {
-                result += (this->rowIndications[row + 1] - this->rowIndications[row]);
+            if (!this->hasTrivialRowGrouping()) {
+                for (uint_fast64_t row = this->getRowGroupIndices()[group]; row < this->getRowGroupIndices()[group + 1]; ++row) {
+                    result += (this->rowIndications[row + 1] - this->rowIndications[row]);
+                }
+            } else {
+                result += (this->rowIndications[group + 1] - this->rowIndications[group]);
             }
             return result;
         }
@@ -502,7 +547,11 @@ namespace storm {
         
         template<typename ValueType>
         typename SparseMatrix<ValueType>::index_type SparseMatrix<ValueType>::getRowGroupCount() const {
-            return rowGroupIndices.size() - 1;
+            if (!this->hasTrivialRowGrouping()) {
+                return rowGroupIndices.get().size() - 1;
+            } else {
+                return rowCount;
+            }
         }
         
         template<typename ValueType>
@@ -512,7 +561,15 @@ namespace storm {
         
         template<typename ValueType>
         std::vector<typename SparseMatrix<ValueType>::index_type> const& SparseMatrix<ValueType>::getRowGroupIndices() const {
-            return rowGroupIndices;
+            // If there is no current row grouping, we need to create it.
+            if (!this->rowGroupIndices) {
+                STORM_LOG_ASSERT(trivialRowGrouping, "Only trivial row-groupings can be constructed on-the-fly.");
+                this->rowGroupIndices = std::vector<index_type>(this->getRowCount() + 1);
+                for (uint_fast64_t group = 0; group <= this->getRowCount(); ++group) {
+                    this->rowGroupIndices.get()[group] = group;
+                }
+            }
+            return rowGroupIndices.get();
         }
 
         template<typename ValueType>
@@ -524,9 +581,15 @@ namespace storm {
         
         template<typename ValueType>
         void SparseMatrix<ValueType>::makeRowGroupsAbsorbing(storm::storage::BitVector const& rowGroupConstraint) {
-            for (auto rowGroup : rowGroupConstraint) {
-                for (index_type row = this->getRowGroupIndices()[rowGroup]; row < this->getRowGroupIndices()[rowGroup + 1]; ++row) {
-                    makeRowDirac(row, rowGroup);
+            if (!this->hasTrivialRowGrouping()) {
+                for (auto rowGroup : rowGroupConstraint) {
+                    for (index_type row = this->getRowGroupIndices()[rowGroup]; row < this->getRowGroupIndices()[rowGroup + 1]; ++row) {
+                        makeRowDirac(row, rowGroup);
+                    }
+                }
+            } else {
+                for (auto rowGroup : rowGroupConstraint) {
+                    makeRowDirac(rowGroup, rowGroup);
                 }
             }
         }
@@ -579,9 +642,15 @@ namespace storm {
         std::vector<ValueType> SparseMatrix<ValueType>::getConstrainedRowGroupSumVector(storm::storage::BitVector const& rowGroupConstraint, storm::storage::BitVector const& columnConstraint) const {
             std::vector<ValueType> result;
             result.reserve(rowGroupConstraint.getNumberOfSetBits());
-            for (auto rowGroup : rowGroupConstraint) {
-                for (index_type row = this->getRowGroupIndices()[rowGroup]; row < this->getRowGroupIndices()[rowGroup + 1]; ++row) {
-                    result.push_back(getConstrainedRowSum(row, columnConstraint));
+            if (!this->hasTrivialRowGrouping()) {
+                for (auto rowGroup : rowGroupConstraint) {
+                    for (index_type row = this->getRowGroupIndices()[rowGroup]; row < this->getRowGroupIndices()[rowGroup + 1]; ++row) {
+                        result.push_back(getConstrainedRowSum(row, columnConstraint));
+                    }
+                }
+            } else {
+                for (auto rowGroup : rowGroupConstraint) {
+                    result.push_back(getConstrainedRowSum(rowGroup, columnConstraint));
                 }
             }
             return result;
@@ -599,25 +668,30 @@ namespace storm {
                     *it = i;
                 }
                 auto res = getSubmatrix(rowConstraint, columnConstraint, fakeRowGroupIndices, insertDiagonalElements);
-
-                // Create a new row grouping that reflects the new sizes of the row groups.
-                std::vector<uint_fast64_t> newRowGroupIndices;
-                newRowGroupIndices.push_back(0);
-                auto selectedRowIt = rowConstraint.begin();
-
-                // For this, we need to count how many rows were preserved in every group.
-                for (uint_fast64_t group = 0; group < this->getRowGroupCount(); ++group) {
-                    uint_fast64_t newRowCount = 0;
-                    while (*selectedRowIt < this->getRowGroupIndices()[group + 1]) {
-                        ++selectedRowIt;
-                        ++newRowCount;
-                    }
-                    if (newRowCount > 0) {
-                        newRowGroupIndices.push_back(newRowGroupIndices.back() + newRowCount);
+                
+                // Create a new row grouping that reflects the new sizes of the row groups if the current matrix has a
+                // non trivial row-grouping.
+                if (!this->hasTrivialRowGrouping()) {
+                    std::vector<uint_fast64_t> newRowGroupIndices;
+                    newRowGroupIndices.push_back(0);
+                    auto selectedRowIt = rowConstraint.begin();
+                    
+                    // For this, we need to count how many rows were preserved in every group.
+                    for (uint_fast64_t group = 0; group < this->getRowGroupCount(); ++group) {
+                        uint_fast64_t newRowCount = 0;
+                        while (*selectedRowIt < this->getRowGroupIndices()[group + 1]) {
+                            ++selectedRowIt;
+                            ++newRowCount;
+                        }
+                        if (newRowCount > 0) {
+                            newRowGroupIndices.push_back(newRowGroupIndices.back() + newRowCount);
+                        }
                     }
+                    
+                    res.trivialRowGrouping = false;
+                    res.rowGroupIndices = newRowGroupIndices;
                 }
                 
-                res.rowGroupIndices = newRowGroupIndices;
                 return res;
             }
         }
@@ -664,13 +738,13 @@ namespace storm {
             }
             
             // Create and initialize resulting matrix.
-            SparseMatrixBuilder<ValueType> matrixBuilder(subRows, submatrixColumnCount, subEntries, true, this->hasNontrivialRowGrouping());
+            SparseMatrixBuilder<ValueType> matrixBuilder(subRows, submatrixColumnCount, subEntries, true, !this->hasTrivialRowGrouping());
             
             // Copy over selected entries.
             rowGroupCount = 0;
             index_type rowCount = 0;
             for (auto index : rowGroupConstraint) {
-                if (this->hasNontrivialRowGrouping()) {
+                if (!this->hasTrivialRowGrouping()) {
                     matrixBuilder.newRowGroup(rowCount);
                 }
                 for (index_type i = rowGroupIndices[index]; i < rowGroupIndices[index + 1]; ++i) {
@@ -706,12 +780,12 @@ namespace storm {
         template<typename ValueType>
         SparseMatrix<ValueType> SparseMatrix<ValueType>::restrictRows(storm::storage::BitVector const& rowsToKeep) const {
             // For now, we use the expensive call to submatrix.
-            assert(rowsToKeep.size() == getRowCount());
-            assert(rowsToKeep.getNumberOfSetBits() >= getRowGroupCount());
+            STORM_LOG_ASSERT(rowsToKeep.size() == this->getRowCount(), "Dimensions mismatch.");
+            STORM_LOG_ASSERT(rowsToKeep.getNumberOfSetBits() >= this->getRowGroupCount(), "Invalid dimensions.");
             SparseMatrix<ValueType> res(getSubmatrix(false, rowsToKeep, storm::storage::BitVector(getColumnCount(), true), false));
-            assert(res.getRowCount() == rowsToKeep.getNumberOfSetBits());
-            assert(res.getColumnCount() == getColumnCount());
-            assert(getRowGroupCount() == res.getRowGroupCount());
+            STORM_LOG_ASSERT(res.getRowCount() == rowsToKeep.getNumberOfSetBits(), "Invalid dimensions");
+            STORM_LOG_ASSERT(res.getColumnCount() == this->getColumnCount(), "Invalid dimensions");
+            STORM_LOG_ASSERT(this->getRowGroupCount() == res.getRowGroupCount(), "Invalid dimensions");
             return res;
         }
         
@@ -722,7 +796,7 @@ namespace storm {
             index_type subEntries = 0;
             for (index_type rowGroupIndex = 0, rowGroupIndexEnd = rowGroupToRowIndexMapping.size(); rowGroupIndex < rowGroupIndexEnd; ++rowGroupIndex) {
                 // Determine which row we need to select from the current row group.
-                index_type rowToCopy = rowGroupIndices[rowGroupIndex] + rowGroupToRowIndexMapping[rowGroupIndex];
+                index_type rowToCopy = this->getRowGroupIndices()[rowGroupIndex] + rowGroupToRowIndexMapping[rowGroupIndex];
                 
                 // Iterate through that row and count the number of slots we have to reserve for copying.
                 bool foundDiagonalElement = false;
@@ -738,12 +812,12 @@ namespace storm {
             }
             
             // Now create the matrix to be returned with the appropriate size.
-            SparseMatrixBuilder<ValueType> matrixBuilder(rowGroupIndices.size() - 1, columnCount, subEntries);
+            SparseMatrixBuilder<ValueType> matrixBuilder(rowGroupIndices.get().size() - 1, columnCount, subEntries);
             
             // Copy over the selected lines from the source matrix.
             for (index_type rowGroupIndex = 0, rowGroupIndexEnd = rowGroupToRowIndexMapping.size(); rowGroupIndex < rowGroupIndexEnd; ++rowGroupIndex) {
                 // Determine which row we need to select from the current row group.
-                index_type rowToCopy = rowGroupIndices[rowGroupIndex] + rowGroupToRowIndexMapping[rowGroupIndex];
+                index_type rowToCopy = this->getRowGroupIndices()[rowGroupIndex] + rowGroupToRowIndexMapping[rowGroupIndex];
                 
                 // Iterate through that row and copy the entries. This also inserts a zero element on the diagonal if
                 // there is no entry yet.
@@ -810,12 +884,7 @@ namespace storm {
                 }
             }
             
-            std::vector<index_type> rowGroupIndices(rowCount + 1);
-            for (index_type i = 0; i <= rowCount; ++i) {
-                rowGroupIndices[i] = i;
-            }
-            
-            storm::storage::SparseMatrix<ValueType> transposedMatrix(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices), false);
+            storm::storage::SparseMatrix<ValueType> transposedMatrix(columnCount, std::move(rowIndications), std::move(columnsAndValues), boost::none);
             
             return transposedMatrix;
         }
@@ -1065,50 +1134,66 @@ namespace storm {
         
         template<typename ValueType>
         typename SparseMatrix<ValueType>::const_rows SparseMatrix<ValueType>::getRows(index_type startRow, index_type endRow) const {
-            return const_rows(this->columnsAndValues.begin() + this->rowIndications[startRow], this->rowIndications[endRow + 1] - this->rowIndications[startRow]);
+            return const_rows(this->columnsAndValues.begin() + this->rowIndications[startRow], this->rowIndications[endRow] - this->rowIndications[startRow]);
         }
         
         template<typename ValueType>
         typename SparseMatrix<ValueType>::rows SparseMatrix<ValueType>::getRows(index_type startRow, index_type endRow) {
-            return rows(this->columnsAndValues.begin() + this->rowIndications[startRow], this->rowIndications[endRow + 1] - this->rowIndications[startRow]);
+            return rows(this->columnsAndValues.begin() + this->rowIndications[startRow], this->rowIndications[endRow] - this->rowIndications[startRow]);
         }
         
         template<typename ValueType>
         typename SparseMatrix<ValueType>::const_rows SparseMatrix<ValueType>::getRow(index_type row) const {
-            return getRows(row, row);
+            return getRows(row, row + 1);
         }
         
         template<typename ValueType>
         typename SparseMatrix<ValueType>::rows SparseMatrix<ValueType>::getRow(index_type row) {
-            return getRows(row, row);
+            return getRows(row, row + 1);
         }
         
         template<typename ValueType>
         typename SparseMatrix<ValueType>::const_rows SparseMatrix<ValueType>::getRow(index_type rowGroup, index_type offset) const {
-            assert(rowGroup < this->getRowGroupCount());
-            assert(offset < this->getRowGroupEntryCount(rowGroup));
-            return getRow(rowGroupIndices[rowGroup] + offset);
+            STORM_LOG_ASSERT(rowGroup < this->getRowGroupCount(), "Row group is out-of-bounds.");
+            STORM_LOG_ASSERT(offset < this->getRowGroupEntryCount(rowGroup), "Row offset in row-group is out-of-bounds.");
+            if (!this->hasTrivialRowGrouping()) {
+                return getRow(this->getRowGroupIndices()[rowGroup] + offset);
+            } else {
+                return getRow(this->getRowGroupIndices()[rowGroup] + offset);
+            }
         }
         
-        
         template<typename ValueType>
         typename SparseMatrix<ValueType>::rows SparseMatrix<ValueType>::getRow(index_type rowGroup, index_type offset) {
-            assert(rowGroup < this->getRowGroupCount());
-            assert(offset < this->getRowGroupEntryCount(rowGroup));
-            return getRow(rowGroupIndices[rowGroup] + offset);
+            STORM_LOG_ASSERT(rowGroup < this->getRowGroupCount(), "Row group is out-of-bounds.");
+            STORM_LOG_ASSERT(offset < this->getRowGroupEntryCount(rowGroup), "Row offset in row-group is out-of-bounds.");
+            if (!this->hasTrivialRowGrouping()) {
+                return getRow(this->getRowGroupIndices()[rowGroup] + offset);
+            } else {
+                STORM_LOG_ASSERT(offset == 0, "Invalid offset.");
+                return getRow(rowGroup + offset);
+            }
         }
         
         
         template<typename ValueType>
         typename SparseMatrix<ValueType>::const_rows SparseMatrix<ValueType>::getRowGroup(index_type rowGroup) const {
-            assert(rowGroup < this->getRowGroupCount());
-            return getRows(rowGroupIndices[rowGroup], rowGroupIndices[rowGroup + 1] - 1);
+            STORM_LOG_ASSERT(rowGroup < this->getRowGroupCount(), "Row group is out-of-bounds.");
+            if (!this->hasTrivialRowGrouping()) {
+                return getRows(this->getRowGroupIndices()[rowGroup], this->getRowGroupIndices()[rowGroup + 1]);
+            } else {
+                return getRows(rowGroup, rowGroup + 1);
+            }
         }
         
         template<typename ValueType>
         typename SparseMatrix<ValueType>::rows SparseMatrix<ValueType>::getRowGroup(index_type rowGroup) {
-            assert(rowGroup < this->getRowGroupCount());
-            return getRows(rowGroupIndices[rowGroup], rowGroupIndices[rowGroup + 1] - 1);
+            STORM_LOG_ASSERT(rowGroup < this->getRowGroupCount(), "Row group is out-of-bounds.");
+            if (!this->hasTrivialRowGrouping()) {
+                return getRows(this->getRowGroupIndices()[rowGroup], this->getRowGroupIndices()[rowGroup + 1]);
+            } else {
+                return getRows(rowGroup, rowGroup + 1);
+            }
         }
         
         template<typename ValueType>
@@ -1142,8 +1227,8 @@ namespace storm {
         }
         
         template<typename ValueType>
-        bool SparseMatrix<ValueType>::hasNontrivialRowGrouping() const {
-            return nontrivialRowGrouping;
+        bool SparseMatrix<ValueType>::hasTrivialRowGrouping() const {
+            return trivialRowGrouping;
         }
         
         template<typename ValueType>
@@ -1172,6 +1257,9 @@ namespace storm {
             // Check for matching sizes.
             if (this->getRowCount() != matrix.getRowCount()) return false;
             if (this->getColumnCount() != matrix.getColumnCount()) return false;
+            if (this->hasTrivialRowGrouping() && !matrix.hasTrivialRowGrouping()) return false;
+            if (!this->hasTrivialRowGrouping() && matrix.hasTrivialRowGrouping()) return false;
+            if (!this->hasTrivialRowGrouping() && !matrix.hasTrivialRowGrouping() && this->getRowGroupIndices() != matrix.getRowGroupIndices()) return false;
             if (this->getRowGroupIndices() != matrix.getRowGroupIndices()) return false;
             
             // Check the subset property for all rows individually.
@@ -1203,7 +1291,10 @@ namespace storm {
             // Iterate over all row groups.
             for (typename SparseMatrix<ValueType>::index_type group = 0; group < matrix.getRowGroupCount(); ++group) {
                 out << "\t---- group " << group << "/" << (matrix.getRowGroupCount() - 1) << " ---- " << std::endl;
-                for (typename SparseMatrix<ValueType>::index_type i = matrix.getRowGroupIndices()[group]; i < matrix.getRowGroupIndices()[group + 1]; ++i) {
+                typename SparseMatrix<ValueType>::index_type start = matrix.hasTrivialRowGrouping() ? group : matrix.getRowGroupIndices()[group];
+                typename SparseMatrix<ValueType>::index_type end = matrix.hasTrivialRowGrouping() ? group + 1 : matrix.getRowGroupIndices()[group + 1];
+                
+                for (typename SparseMatrix<ValueType>::index_type i = start; i < end; ++i) {
                     typename SparseMatrix<ValueType>::index_type nextIndex = matrix.rowIndications[i];
                     
                     // Print the actual row.
@@ -1239,7 +1330,7 @@ namespace storm {
                 assert(this->getRowGroupSize(group) == 1);
                 for (typename SparseMatrix<ValueType>::index_type i = this->getRowGroupIndices()[group]; i < this->getRowGroupIndices()[group + 1]; ++i) {
                     typename SparseMatrix<ValueType>::index_type nextIndex = this->rowIndications[i];
-
+                    
                     // Print the actual row.
                     out << i << "\t(";
                     typename SparseMatrix<ValueType>::index_type currentRealIndex = 0;
@@ -1266,7 +1357,9 @@ namespace storm {
             boost::hash_combine(result, this->getEntryCount());
             boost::hash_combine(result, boost::hash_range(columnsAndValues.begin(), columnsAndValues.end()));
             boost::hash_combine(result, boost::hash_range(rowIndications.begin(), rowIndications.end()));
-            boost::hash_combine(result, boost::hash_range(rowGroupIndices.begin(), rowGroupIndices.end()));
+            if (!this->hasTrivialRowGrouping()) {
+                boost::hash_combine(result, boost::hash_range(rowGroupIndices.get().begin(), rowGroupIndices.get().end()));
+            }
             
             return result;
         }
@@ -1293,7 +1386,7 @@ namespace storm {
         template std::ostream& operator<<(std::ostream& out, SparseMatrix<double> const& matrix);
         template std::vector<double> SparseMatrix<double>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<double> const& otherMatrix) const;
         template bool SparseMatrix<double>::isSubmatrixOf(SparseMatrix<double> const& matrix) const;
-
+        
         // float
         template class MatrixEntry<typename SparseMatrix<float>::index_type, float>;
         template std::ostream& operator<<(std::ostream& out, MatrixEntry<typename SparseMatrix<float>::index_type, float> const& entry);
@@ -1302,7 +1395,7 @@ namespace storm {
         template std::ostream& operator<<(std::ostream& out, SparseMatrix<float> const& matrix);
         template std::vector<float> SparseMatrix<float>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<float> const& otherMatrix) const;
         template bool SparseMatrix<float>::isSubmatrixOf(SparseMatrix<float> const& matrix) const;
-
+        
         // int
         template class MatrixEntry<typename SparseMatrix<int>::index_type, int>;
         template std::ostream& operator<<(std::ostream& out, MatrixEntry<typename SparseMatrix<int>::index_type, int> const& entry);
@@ -1310,7 +1403,7 @@ namespace storm {
         template class SparseMatrix<int>;
         template std::ostream& operator<<(std::ostream& out, SparseMatrix<int> const& matrix);
         template bool SparseMatrix<int>::isSubmatrixOf(SparseMatrix<int> const& matrix) const;
-
+        
         // state_type
         template class MatrixEntry<typename SparseMatrix<storm::storage::sparse::state_type>::index_type, storm::storage::sparse::state_type>;
         template std::ostream& operator<<(std::ostream& out, MatrixEntry<typename SparseMatrix<storm::storage::sparse::state_type>::index_type, storm::storage::sparse::state_type> const& entry);
@@ -1318,7 +1411,7 @@ namespace storm {
         template class SparseMatrix<storm::storage::sparse::state_type>;
         template std::ostream& operator<<(std::ostream& out, SparseMatrix<storm::storage::sparse::state_type> const& matrix);
         template bool SparseMatrix<int>::isSubmatrixOf(SparseMatrix<storm::storage::sparse::state_type> const& matrix) const;
-
+        
 #ifdef STORM_HAVE_CARL
         // Rat Function
         template class MatrixEntry<typename SparseMatrix<CarlRationalNumber>::index_type, CarlRationalNumber>;
@@ -1340,7 +1433,7 @@ namespace storm {
         template std::vector<storm::RationalFunction> SparseMatrix<float>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::RationalFunction> const& otherMatrix) const;
         template std::vector<storm::RationalFunction> SparseMatrix<int>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::RationalFunction> const& otherMatrix) const;
         template bool SparseMatrix<storm::RationalFunction>::isSubmatrixOf(SparseMatrix<storm::RationalFunction> const& matrix) const;
-
+        
         // Intervals
         template std::vector<storm::Interval> SparseMatrix<double>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::Interval> const& otherMatrix) const;
         template class MatrixEntry<typename SparseMatrix<Interval>::index_type, Interval>;
@@ -1350,7 +1443,7 @@ namespace storm {
         template std::ostream& operator<<(std::ostream& out, SparseMatrix<Interval> const& matrix);
         template std::vector<storm::Interval> SparseMatrix<Interval>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::Interval> const& otherMatrix) const;
         template bool SparseMatrix<storm::Interval>::isSubmatrixOf(SparseMatrix<storm::Interval> const& matrix) const;
-
+        
         template bool SparseMatrix<storm::Interval>::isSubmatrixOf(SparseMatrix<double> const& matrix) const;
 #endif
         

src/storage/SparseMatrix.h

@@ -7,9 +7,11 @@
 #include <vector>
 #include <iterator>
 
+#include <boost/functional/hash.hpp>
+#include <boost/optional.hpp>
+
 #include "src/utility/OsDetection.h"
 #include "src/adapters/CarlAdapter.h"
-#include <boost/functional/hash.hpp>
 
 // Forward declaration for adapter classes.
 namespace storm {
@@ -259,7 +261,8 @@ namespace storm {
             // The number of row groups in the matrix.
             index_type initialRowGroupCount;
             
-            std::vector<index_type> rowGroupIndices;
+            // The vector that stores the row-group indices (if they are non-trivial).
+            boost::optional<std::vector<index_type>> rowGroupIndices;
             
             // The storage for the columns and values of all entries in the matrix.
             std::vector<MatrixEntry<index_type, value_type>> columnsAndValues;
@@ -452,9 +455,8 @@ namespace storm {
              * @param rowIndications The row indications vector of the matrix to be constructed.
              * @param columnsAndValues The vector containing the columns and values of the entries in the matrix.
              * @param rowGroupIndices The vector representing the row groups in the matrix.
-             * @param hasNontrivialRowGrouping If set to true, this indicates that the row grouping is non-trivial.
              */
-            SparseMatrix(index_type columnCount, std::vector<index_type> const& rowIndications, std::vector<MatrixEntry<index_type, value_type>> const& columnsAndValues, std::vector<index_type> const& rowGroupIndices, bool hasNontrivialRowGrouping);
+            SparseMatrix(index_type columnCount, std::vector<index_type> const& rowIndications, std::vector<MatrixEntry<index_type, value_type>> const& columnsAndValues, boost::optional<std::vector<index_type>> const& rowGroupIndices);
             
             /*!
              * Constructs a sparse matrix by moving the given contents.
@@ -463,9 +465,8 @@ namespace storm {
              * @param rowIndications The row indications vector of the matrix to be constructed.
              * @param columnsAndValues The vector containing the columns and values of the entries in the matrix.
              * @param rowGroupIndices The vector representing the row groups in the matrix.
-             * @param hasNontrivialRowGrouping If set to true, this indicates that the row grouping is non-trivial.
              */
-            SparseMatrix(index_type columnCount, std::vector<index_type>&& rowIndications, std::vector<MatrixEntry<index_type, value_type>>&& columnsAndValues, std::vector<index_type>&& rowGroupIndices, bool hasNontrivialRowGrouping);
+            SparseMatrix(index_type columnCount, std::vector<index_type>&& rowIndications, std::vector<MatrixEntry<index_type, value_type>>&& columnsAndValues, boost::optional<std::vector<index_type>>&& rowGroupIndices);
 
             /*!
              * Assigns the contents of the given matrix to the current one by deep-copying its contents.
@@ -809,7 +810,7 @@ namespace storm {
              * Returns an object representing the consecutive rows given by the parameters.
              *
              * @param startRow The starting row.
-             * @param endRow The ending row (which is included in the result).
+             * @param endRow The ending row (which is *not* included in the result).
              * @return An object representing the consecutive rows given by the parameters.
              */
             const_rows getRows(index_type startRow, index_type endRow) const;
@@ -818,7 +819,7 @@ namespace storm {
              * Returns an object representing the consecutive rows given by the parameters.
              *
              * @param startRow The starting row.
-             * @param endRow The ending row (which is included in the result).
+             * @param endRow The ending row (which is *not* included in the result).
              * @return An object representing the consecutive rows given by the parameters.
              */
             rows getRows(index_type startRow, index_type endRow);
@@ -918,27 +919,28 @@ namespace storm {
             iterator end();
             
             /*!
-             * Retrieves whether the matrix has a (possibly) non-trivial row grouping.
+             * Retrieves whether the matrix has a trivial row grouping.
              *
-             * @return True iff the matrix has a (possibly) non-trivial row grouping.
+             * @return True iff the matrix has a trivial row grouping.
              */
-            bool hasNontrivialRowGrouping() const;
+            bool hasTrivialRowGrouping() const;
 
 			/*!
 			* Returns a copy of the matrix with the chosen internal data type
 			*/
 			template<typename NewValueType>
 			SparseMatrix<NewValueType> toValueType() const {
-				std::vector<MatrixEntry<SparseMatrix::index_type, NewValueType>> new_columnsAndValues;
-				std::vector<SparseMatrix::index_type> new_rowIndications(rowIndications);
-				std::vector<SparseMatrix::index_type> new_rowGroupIndices(rowGroupIndices);
+				std::vector<MatrixEntry<SparseMatrix::index_type, NewValueType>> newColumnsAndValues;
+				std::vector<SparseMatrix::index_type> newRowIndications(rowIndications);
+                boost::optional<std::vector<SparseMatrix::index_type>> newRowGroupIndices(rowGroupIndices);
 
-				new_columnsAndValues.resize(columnsAndValues.size());
-				for (size_t i = 0, size = columnsAndValues.size(); i < size; ++i) {
-					new_columnsAndValues.at(i) = MatrixEntry<SparseMatrix::index_type, NewValueType>(columnsAndValues.at(i).getColumn(), static_cast<NewValueType>(columnsAndValues.at(i).getValue()));
-				}
+				newColumnsAndValues.resize(columnsAndValues.size());
+                std::transform(columnsAndValues.begin(), columnsAndValues.end(), newColumnsAndValues.begin(),
+                               [] (MatrixEntry<SparseMatrix::index_type, ValueType> const& a) {
+                                   return MatrixEntry<SparseMatrix::index_type, NewValueType>(a.getColumn(), static_cast<NewValueType>(a.getValue()));
+                               });
 
-				return SparseMatrix<NewValueType>(columnCount, std::move(new_rowIndications), std::move(new_columnsAndValues), std::move(new_rowGroupIndices), nontrivialRowGrouping);
+				return SparseMatrix<NewValueType>(columnCount, std::move(newRowIndications), std::move(newColumnsAndValues), std::move(newRowGroupIndices));
 			}
             
         private:
@@ -977,12 +979,12 @@ namespace storm {
             // entry is not included anymore.
             std::vector<index_type> rowIndications;
             
-            // A flag that indicates whether the matrix has a non-trivial row-grouping, i.e. (possibly) more than one
-            // row per row group.
-            bool nontrivialRowGrouping;
+            // A flag indicating whether the matrix has a trivial row grouping. Note that this may be true and yet
+            // there may be row group indices, because they were requested from the outside.
+            bool trivialRowGrouping;
             
-            // A vector indicating the row groups of the matrix.
-            std::vector<index_type> rowGroupIndices;
+            // A vector indicating the row groups of the matrix. This needs to be mutible in case we create it on-the-fly.
+            mutable boost::optional<std::vector<index_type>> rowGroupIndices;
             
         };
         

src/storage/dd/Add.cpp

@@ -459,7 +459,7 @@ namespace storm {
             rowIndications[0] = 0;
             
             // Construct matrix and return result.
-            return storm::storage::SparseMatrix<ValueType>(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(trivialRowGroupIndices), false);
+            return storm::storage::SparseMatrix<ValueType>(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), boost::none);
         }
         
         template<DdType LibraryType, typename ValueType>
@@ -583,7 +583,7 @@ namespace storm {
             }
             rowIndications[0] = 0;
             
-            return storm::storage::SparseMatrix<ValueType>(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices), true);
+            return storm::storage::SparseMatrix<ValueType>(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices));
         }
 
         template<DdType LibraryType, typename ValueType>
@@ -708,7 +708,7 @@ namespace storm {
             }
             rowIndications[0] = 0;
             
-            return std::make_pair(storm::storage::SparseMatrix<ValueType>(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices), true), std::move(explicitVector));
+            return std::make_pair(storm::storage::SparseMatrix<ValueType>(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)), std::move(explicitVector));
         }
 
         template<DdType LibraryType, typename ValueType>

src/storage/prism/Program.cpp

@@ -77,6 +77,14 @@ namespace storm {
             return modelType;
         }
         
+        bool Program::isDiscreteTimeModel() const {
+            return modelType == ModelType::DTMC || modelType == ModelType::MDP;
+        }
+        
+        bool Program::isDeterministicModel() const {
+            return modelType == ModelType::DTMC || modelType == ModelType::CTMC;
+        }
+        
         bool Program::hasUndefinedConstants() const {
             for (auto const& constant : this->getConstants()) {
                 if (!constant.isDefined()) {

src/storage/prism/Program.h

@@ -66,6 +66,18 @@ namespace storm {
              * @return The type of the model.
              */
             ModelType getModelType() const;
+            
+            /*!
+             * Retrieves whether the model is a discrete-time model, i.e. a DTMC or an MDP.
+             *
+             * @return True iff the model is a discrete-time model.
+             */
+            bool isDiscreteTimeModel() const;
+            
+            /*!
+             * Retrieves whether the model is one without nondeterministic choices, i.e. a DTMC or a CTMC.
+             */
+            bool isDeterministicModel() const;
 
             /*!
              * Retrieves whether there are undefined constants of any type in the program.

src/storage/prism/RewardModel.cpp

@@ -84,7 +84,7 @@ namespace storm {
         std::ostream& operator<<(std::ostream& stream, RewardModel const& rewardModel) {
             stream << "rewards";
             if (rewardModel.getName() != "") {
-                std::cout << " \"" << rewardModel.getName() << "\"";
+                stream << " \"" << rewardModel.getName() << "\"";
             }
             stream << std::endl;
             for (auto const& reward : rewardModel.getStateRewards()) {

src/utility/constants.cpp

@@ -215,6 +215,10 @@ namespace storm {
         template bool isZero(storm::storage::sparse::state_type const& value);
         template bool isConstant(storm::storage::sparse::state_type const& value);
 
+        template uint32_t one();
+        template uint32_t zero();
+        template uint32_t infinity();
+                
         template storm::storage::sparse::state_type one();
         template storm::storage::sparse::state_type zero();
         template storm::storage::sparse::state_type infinity();

src/utility/storm.h

@@ -110,8 +110,8 @@ namespace storm {
                 options.buildCommandLabels = true;
             }
 
-            storm::builder::ExplicitPrismModelBuilder<ValueType> builder;
-            result.model = builder.translateProgram(program, options);
+            storm::builder::ExplicitPrismModelBuilder<ValueType> builder(program, options);
+            result.model = builder.translate();
             translatedProgram = builder.getTranslatedProgram();
         } else if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Dd || settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
             typename storm::builder::DdPrismModelBuilder<LibraryType>::Options options;