more bugfixes

Former-commit-id: 5afecd5a21

src/builder/DdPrismModelBuilder.cpp

@@ -336,17 +336,19 @@ namespace storm {
         }
         
         template <storm::dd::DdType Type>
-        typename DdPrismModelBuilder<Type>::ActionDecisionDiagram DdPrismModelBuilder<Type>::createActionDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, boost::optional<uint_fast64_t> synchronizationActionIndex, uint_fast64_t nondeterminismVariableOffset) {
+        typename DdPrismModelBuilder<Type>::ActionDecisionDiagram DdPrismModelBuilder<Type>::createActionDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, uint_fast64_t synchronizationActionIndex, uint_fast64_t nondeterminismVariableOffset) {
             std::vector<ActionDecisionDiagram> commandDds;
             for (storm::prism::Command const& command : module.getCommands()) {
                 
                 // Determine whether the command is relevant for the selected action.
-                bool relevant = (!synchronizationActionIndex && !command.isLabeled()) || (synchronizationActionIndex && command.isLabeled() && command.getActionIndex() == synchronizationActionIndex.get());
+                bool relevant = (synchronizationActionIndex == 0 && !command.isLabeled()) || (synchronizationActionIndex && command.isLabeled() && command.getActionIndex() == synchronizationActionIndex);
                 
                 if (!relevant) {
                     continue;
                 }
                 
+                STORM_LOG_TRACE("Translating command " << command);
+                
                 // At this point, the command is known to be relevant for the action.
                 commandDds.push_back(createCommandDecisionDiagram(generationInfo, module, command));
             }
@@ -551,12 +553,12 @@ namespace storm {
         template <storm::dd::DdType Type>
         typename DdPrismModelBuilder<Type>::ModuleDecisionDiagram DdPrismModelBuilder<Type>::createModuleDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, std::map<uint_fast64_t, uint_fast64_t> const& synchronizingActionToOffsetMap) {
             // Start by creating the action DD for the independent action.
-            ActionDecisionDiagram independentActionDd = createActionDecisionDiagram(generationInfo, module, boost::optional<uint_fast64_t>(), 0);
+            ActionDecisionDiagram independentActionDd = createActionDecisionDiagram(generationInfo, module, 0, 0);
             uint_fast64_t numberOfUsedNondeterminismVariables = independentActionDd.numberOfUsedNondeterminismVariables;
             
             // Create module DD for all synchronizing actions of the module.
             std::map<uint_fast64_t, ActionDecisionDiagram> actionIndexToDdMap;
-            for (auto const& actionIndex : module.getActionIndices()) {
+            for (auto const& actionIndex : module.getSynchronizingActionIndices()) {
                 STORM_LOG_TRACE("Creating DD for action '" << actionIndex << "'.");
                 ActionDecisionDiagram tmp = createActionDecisionDiagram(generationInfo, module, actionIndex, synchronizingActionToOffsetMap.at(actionIndex));
                 numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, tmp.numberOfUsedNondeterminismVariables);
@@ -567,12 +569,18 @@ namespace storm {
         }
         
         template <storm::dd::DdType Type>
-        storm::dd::Add<Type> DdPrismModelBuilder<Type>::getSynchronizationDecisionDiagram(GenerationInformation& generationInfo, boost::optional<uint_fast64_t> const& synchronizationAction) {
+        storm::dd::Add<Type> DdPrismModelBuilder<Type>::getSynchronizationDecisionDiagram(GenerationInformation& generationInfo, uint_fast64_t actionIndex) {
             storm::dd::Add<Type> synchronization = generationInfo.manager->getAddOne();
-            for (uint_fast64_t i = 0; i < generationInfo.synchronizationMetaVariables.size(); ++i) {
-                if (synchronizationAction && synchronizationAction.get() == i) {
-                    synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 1).toAdd();
-                } else {
+            if (actionIndex != 0) {
+                for (uint_fast64_t i = 0; i < generationInfo.synchronizationMetaVariables.size(); ++i) {
+                    if ((actionIndex - 1) == i) {
+                        synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 1).toAdd();
+                    } else {
+                        synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 0).toAdd();
+                    }
+                }
+            } else {
+                for (uint_fast64_t i = 0; i < generationInfo.synchronizationMetaVariables.size(); ++i) {
                     synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 0).toAdd();
                 }
             }
@@ -670,7 +678,7 @@ namespace storm {
                 }
                 
                 // Combine synchronizing actions.
-                for (auto const& actionIndex : currentModule.getActionIndices()) {
+                for (auto const& actionIndex : currentModule.getSynchronizingActionIndices()) {
                     if (system.hasSynchronizingAction(actionIndex)) {
                         system.synchronizingActionToDecisionDiagramMap[actionIndex] = combineSynchronizingActions(generationInfo, system.synchronizingActionToDecisionDiagramMap[actionIndex], nextModule.synchronizingActionToDecisionDiagramMap[actionIndex]);
                         numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, system.synchronizingActionToDecisionDiagramMap[actionIndex].numberOfUsedNondeterminismVariables);

src/builder/DdPrismModelBuilder.h

@@ -173,7 +173,7 @@ namespace storm {
 
             static ActionDecisionDiagram createCommandDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, storm::prism::Command const& command);
 
-            static ActionDecisionDiagram createActionDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, boost::optional<uint_fast64_t> synchronizationActionIndex, uint_fast64_t nondeterminismVariableOffset);
+            static ActionDecisionDiagram createActionDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, uint_fast64_t synchronizationActionIndex, uint_fast64_t nondeterminismVariableOffset);
 
             static ActionDecisionDiagram combineCommandsToActionDTMC(GenerationInformation& generationInfo, std::vector<ActionDecisionDiagram> const& commandDds);
 
@@ -185,7 +185,7 @@ namespace storm {
 
             static ModuleDecisionDiagram createModuleDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, std::map<uint_fast64_t, uint_fast64_t> const& synchronizingActionToOffsetMap);
 
-            static storm::dd::Add<Type> getSynchronizationDecisionDiagram(GenerationInformation& generationInfo, boost::optional<uint_fast64_t> const& synchronizationAction = boost::optional<uint_fast64_t>());
+            static storm::dd::Add<Type> getSynchronizationDecisionDiagram(GenerationInformation& generationInfo, uint_fast64_t actionIndex = 0);
             
             static storm::dd::Add<Type> createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram const& module);
             

src/builder/ExplicitPrismModelBuilder.cpp

@@ -499,7 +499,6 @@ namespace storm {
                         }
                         
                         // Check that the resulting distribution is in fact a distribution.
-                        std::cout << probabilitySum << " vs " << comparator.isOne(probabilitySum) << " // " << (probabilitySum - 1) << std::endl;
                         STORM_LOG_THROW(!discreteTimeModel || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not some to one for some command (actually sum to " << probabilitySum << ").");
                         
                         // Dispose of the temporary maps.
@@ -535,7 +534,6 @@ namespace storm {
             }
             
             // A comparator that can be used to check whether we actually have distributions.
-            std::cout << "creating comparator.. " << std::endl;
             storm::utility::ConstantsComparator<ValueType> comparator;
             
             // Initialize a queue and insert the initial state.
@@ -650,7 +648,17 @@ namespace storm {
                     if (deterministicModel) {
                         Choice<ValueType> globalChoice;
 
-                        std::unordered_map<IndexType, ValueType> stateToRewardMap;
+                        // We need to prepare the entries of those vectors that are going to be used.
+                        auto builderIt = rewardModelBuilders.begin();
+                        for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) {
+                            if (rewardModelIt->get().hasStateRewards()) {
+                                builderIt->stateRewardVector.push_back(storm::utility::zero<ValueType>());
+                            }
+                            
+                            if (rewardModelIt->get().hasStateActionRewards()) {
+                                builderIt->stateActionRewardVector.push_back(storm::utility::zero<ValueType>());
+                            }
+                        }
                         
                         // Combine all the choices and scale them with the total number of choices of the current state.
                         for (auto const& choice : allUnlabeledChoices) {
@@ -661,7 +669,6 @@ namespace storm {
                             auto builderIt = rewardModelBuilders.begin();
                             for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) {
                                 if (rewardModelIt->get().hasStateRewards()) {
-                                    builderIt->stateRewardVector.push_back(storm::utility::zero<ValueType>());
                                     for (auto const& stateReward : rewardModelIt->get().getStateRewards()) {
                                         if (evaluator.asBool(stateReward.getStatePredicateExpression())) {
                                             builderIt->stateRewardVector.back() += ValueType(evaluator.asRational(stateReward.getRewardValueExpression()));
@@ -670,7 +677,6 @@ namespace storm {
                                 }
                                 
                                 if (rewardModelIt->get().hasStateActionRewards()) {
-                                    builderIt->stateActionRewardVector.push_back(storm::utility::zero<ValueType>());
                                     for (auto const& stateActionReward : rewardModelIt->get().getStateActionRewards()) {
                                         if (!stateActionReward.isLabeled()) {
                                             if (evaluator.asBool(stateActionReward.getStatePredicateExpression())) {

src/models/symbolic/Model.cpp

@@ -1,5 +1,7 @@
 #include "src/models/symbolic/Model.h"
 
+#include <boost/algorithm/string/join.hpp>
+
 #include "src/exceptions/IllegalArgumentException.h"
 
 #include "src/adapters/AddExpressionAdapter.h"
@@ -164,11 +166,47 @@ namespace storm {
             
             template<storm::dd::DdType Type>
             void Model<Type>::printModelInformationToStream(std::ostream& out) const {
+                this->printModelInformationHeaderToStream(out);
+                this->printModelInformationFooterToStream(out);
+            }
+            
+            template<storm::dd::DdType Type>
+            void Model<Type>::printModelInformationHeaderToStream(std::ostream& out) const {
                 out << "-------------------------------------------------------------- " << std::endl;
                 out << "Model type: \t" << this->getType() << " (symbolic)" << std::endl;
                 out << "States: \t" << this->getNumberOfStates() << " (" << reachableStates.getNodeCount() << " nodes)" << std::endl;
                 out << "Transitions: \t" << this->getNumberOfTransitions() << " (" << transitionMatrix.getNodeCount() << " nodes)" << std::endl;
-                
+            }
+            
+            template<storm::dd::DdType Type>
+            void Model<Type>::printModelInformationFooterToStream(std::ostream& out) const {
+                this->printRewardModelsInformationToStream(out);
+                this->printDdVariableInformationToStream(out);
+                out << std::endl;
+                out << "Labels: \t" << this->labelToExpressionMap.size() << std::endl;
+                for (auto const& label : labelToExpressionMap) {
+                    out << "   * " << label.first << std::endl;
+                }
+                out << "Size in memory: \t" << (this->getSizeInBytes())/1024 << " kbytes" << std::endl;
+                out << "-------------------------------------------------------------- " << std::endl;
+            }
+            
+            template<storm::dd::DdType Type>
+            void Model<Type>::printRewardModelsInformationToStream(std::ostream& out) const {
+                if (this->rewardModels.size()) {
+                    std::vector<std::string> rewardModelNames;
+                    std::for_each(this->rewardModels.cbegin(), this->rewardModels.cend(),
+                                  [&rewardModelNames] (typename std::pair<std::string, RewardModelType> const& nameRewardModelPair) {
+                                      if (nameRewardModelPair.first.empty()) { rewardModelNames.push_back("(default)"); } else { rewardModelNames.push_back(nameRewardModelPair.first); }
+                                  });
+                    out << "Reward Models:  " << boost::join(rewardModelNames, ", ") << std::endl;
+                } else {
+                    out << "Reward Models:  none" << std::endl;
+                }
+            }
+
+            template<storm::dd::DdType Type>
+            void Model<Type>::printDdVariableInformationToStream(std::ostream& out) const {
                 uint_fast64_t rowVariableCount = 0;
                 for (auto const& metaVariable : this->rowVariables) {
                     rowVariableCount += this->getManager().getMetaVariable(metaVariable).getNumberOfDdVariables();
@@ -178,13 +216,7 @@ namespace storm {
                     columnVariableCount += this->getManager().getMetaVariable(metaVariable).getNumberOfDdVariables();
                 }
                 
-                out << "Variables: \t" << "rows: " << this->rowVariables.size() << " meta variables (" << rowVariableCount << " DD variables)" << ", columns: " << this->columnVariables.size() << " meta variables (" << columnVariableCount << " DD variables)" << std::endl;
-                out << "Labels: \t" << this->labelToExpressionMap.size() << std::endl;
-                for (auto const& label : labelToExpressionMap) {
-                    out << "   * " << label.first << std::endl;
-                }
-                out << "Size in memory: \t" << (this->getSizeInBytes())/1024 << " kbytes" << std::endl;
-                out << "-------------------------------------------------------------- " << std::endl;
+                out << "Variables: \t" << "rows: " << this->rowVariables.size() << " meta variables (" << rowVariableCount << " DD variables)" << ", columns: " << this->columnVariables.size() << " meta variables (" << columnVariableCount << " DD variables)";
             }
             
             template<storm::dd::DdType Type>

src/models/symbolic/Model.h

@@ -239,6 +239,35 @@ namespace storm {
                  */
                 std::map<std::string, storm::expressions::Expression> const& getLabelToExpressionMap() const;
                 
+                /*!
+                 * Prints the information header (number of states and transitions) of the model to the specified stream.
+                 *
+                 * @param out The stream the information is to be printed to.
+                 */
+                void printModelInformationHeaderToStream(std::ostream& out) const;
+                
+                /*!
+                 * Prints the information footer (reward models, labels) of the model to the
+                 * specified stream.
+                 *
+                 * @param out The stream the information is to be printed to.
+                 */
+                void printModelInformationFooterToStream(std::ostream& out) const;
+                
+                /*!
+                 * Prints information about the reward models to the specified stream.
+                 *
+                 * @param out The stream the information is to be printed to.
+                 */
+                void printRewardModelsInformationToStream(std::ostream& out) const;
+                
+                /*!
+                 * Prints information about the DD variables to the specified stream.
+                 *
+                 * @param out The stream the information is to be printed to.
+                 */
+                virtual void printDdVariableInformationToStream(std::ostream& out) const;
+                
             private:
                 // The manager responsible for the decision diagrams.
                 std::shared_ptr<storm::dd::DdManager<Type>> manager;

src/models/symbolic/NondeterministicModel.cpp

@@ -51,34 +51,21 @@ namespace storm {
             
             template<storm::dd::DdType Type>
             void NondeterministicModel<Type>::printModelInformationToStream(std::ostream& out) const {
-                out << "-------------------------------------------------------------- " << std::endl;
-                out << "Model type: \t" << this->getType() << " (symbolic)" << std::endl;
-                out << "States: \t" << this->getNumberOfStates() << " (" << this->getReachableStates().getNodeCount() << " nodes)" << std::endl;
-                out << "Transitions: \t" << this->getNumberOfTransitions() << " (" << this->getTransitionMatrix().getNodeCount() << " nodes)" << std::endl;
+                this->printModelInformationHeaderToStream(out);
                 out << "Choices: \t" << this->getNumberOfChoices() << std::endl;
-                
-                uint_fast64_t rowVariableCount = 0;
-                for (auto const& metaVariable : this->getRowVariables()) {
-                    rowVariableCount += this->getManager().getMetaVariable(metaVariable).getNumberOfDdVariables();
-                }
-                uint_fast64_t columnVariableCount = 0;
-                for (auto const& metaVariable : this->getColumnVariables()) {
-                    columnVariableCount += this->getManager().getMetaVariable(metaVariable).getNumberOfDdVariables();
-                }
+                this->printModelInformationFooterToStream(out);
+            }
+            
+            template<storm::dd::DdType Type>
+            void NondeterministicModel<Type>::printDdVariableInformationToStream(std::ostream& out) const {
                 uint_fast64_t nondeterminismVariableCount = 0;
                 for (auto const& metaVariable : this->getNondeterminismVariables()) {
                     nondeterminismVariableCount += this->getManager().getMetaVariable(metaVariable).getNumberOfDdVariables();
                 }
-                
-                out << "Variables: \t" << "rows: " << this->getRowVariables().size() << " meta variables (" << rowVariableCount << " DD variables)" << ", columns: " << this->getColumnVariables().size() << "meta variables (" << columnVariableCount << " DD variables), nondeterminism: " << this->getNondeterminismVariables().size() << " meta variables (" << nondeterminismVariableCount << " DD variables)" << std::endl;
-                out << "Labels: \t" << this->getLabelToExpressionMap().size() << std::endl;
-                for (auto const& label : this->getLabelToExpressionMap()) {
-                    out << "   * " << label.first << std::endl;
-                }
-                out << "Size in memory: \t" << (this->getSizeInBytes())/1024 << " kbytes" << std::endl;
-                out << "-------------------------------------------------------------- " << std::endl;
+                Model<Type>::printDdVariableInformationToStream(out);
+                out << ", nondeterminism: " << this->getNondeterminismVariables().size() << " meta variables (" << nondeterminismVariableCount << " DD variables)";
             }
-            
+                        
             // Explicitly instantiate the template class.
             template class NondeterministicModel<storm::dd::DdType::CUDD>;
             

src/models/symbolic/NondeterministicModel.h

@@ -80,6 +80,10 @@ namespace storm {
                 
                 virtual void printModelInformationToStream(std::ostream& out) const override;
                 
+            protected:
+            
+                virtual void printDdVariableInformationToStream(std::ostream& out) const override;
+                
             private:
                 
                 // The meta variables encoding the nondeterminism in the model.

src/storage/prism/Module.cpp

@@ -10,7 +10,7 @@ namespace storm {
             // Intentionally left empty.
         }
         
-        Module::Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, std::string const& renamedFromModule, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(moduleName), booleanVariables(booleanVariables), booleanVariableToIndexMap(), integerVariables(integerVariables), integerVariableToIndexMap(), commands(commands), actionIndices(), actionIndicesToCommandIndexMap(), renamedFromModule(renamedFromModule), renaming(renaming) {
+        Module::Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, std::string const& renamedFromModule, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(moduleName), booleanVariables(booleanVariables), booleanVariableToIndexMap(), integerVariables(integerVariables), integerVariableToIndexMap(), commands(commands), synchronizingActionIndices(), actionIndicesToCommandIndexMap(), renamedFromModule(renamedFromModule), renaming(renaming) {
             // Initialize the internal mappings for fast information retrieval.
             this->createMappings();
         }
@@ -71,12 +71,12 @@ namespace storm {
             return this->moduleName;
         }
         
-        std::set<uint_fast64_t> const& Module::getActionIndices() const {
-            return this->actionIndices;
+        std::set<uint_fast64_t> const& Module::getSynchronizingActionIndices() const {
+            return this->synchronizingActionIndices;
         }
         
         bool Module::hasActionIndex(uint_fast64_t actionIndex) const {
-            return this->actionIndices.find(actionIndex) != this->actionIndices.end();
+            return this->actionIndicesToCommandIndexMap.find(actionIndex) != this->actionIndicesToCommandIndexMap.end();
         }
         
         bool Module::isRenamedFromModule() const {
@@ -124,13 +124,17 @@ namespace storm {
                         this->actionIndicesToCommandIndexMap.emplace(actionIndex, std::set<uint_fast64_t>());
                     }
                     this->actionIndicesToCommandIndexMap[actionIndex].insert(i);
-                    this->actionIndices.insert(actionIndex);
+                    
+                    // Only take the command into the set if it's non-synchronizing.
+                    if (actionIndex != 0) {
+                        this->synchronizingActionIndices.insert(actionIndex);
+                    }
                 }
             }
             
             // For all actions that are "in the module", but for which no command exists, we add the mapping to an empty
             // set of commands.
-            for (auto const& actionIndex : this->actionIndices) {
+            for (auto const& actionIndex : this->synchronizingActionIndices) {
                 if (this->actionIndicesToCommandIndexMap.find(actionIndex) == this->actionIndicesToCommandIndexMap.end()) {
                     this->actionIndicesToCommandIndexMap[actionIndex] = std::set<uint_fast64_t>();
                 }

src/storage/prism/Module.h

@@ -141,11 +141,11 @@ namespace storm {
             std::string const& getName() const;
             
             /*!
-             * Retrieves the set of action indices present in this module.
+             * Retrieves the set of synchronizing action indices present in this module.
              *
-             * @return the set of action indices present in this module.
+             * @return the set of synchronizing action indices present in this module.
              */
-            std::set<uint_fast64_t> const& getActionIndices() const;
+            std::set<uint_fast64_t> const& getSynchronizingActionIndices() const;
             
             /*!
              * Retrieves whether or not this module contains a command labeled with the given action index.
@@ -237,7 +237,7 @@ namespace storm {
             std::vector<storm::prism::Command> commands;
             
             // The set of action indices present in this module.
-            std::set<uint_fast64_t> actionIndices;
+            std::set<uint_fast64_t> synchronizingActionIndices;
             
             // A map of actions to the set of commands labeled with this action.
             std::map<uint_fast64_t, std::set<uint_fast64_t>> actionIndicesToCommandIndexMap;

src/storage/prism/Program.cpp

@@ -403,7 +403,7 @@ namespace storm {
             for (unsigned int moduleIndex = 0; moduleIndex < this->getNumberOfModules(); moduleIndex++) {
                 Module const& module = this->getModule(moduleIndex);
                 
-                for (auto const& actionIndex : module.getActionIndices()) {
+                for (auto const& actionIndex : module.getSynchronizingActionIndices()) {
                     auto const& actionModuleIndicesPair = this->actionIndicesToModuleIndexMap.find(actionIndex);
                     if (actionModuleIndicesPair == this->actionIndicesToModuleIndexMap.end()) {
                         this->actionIndicesToModuleIndexMap[actionIndex] = std::set<uint_fast64_t>();

src/utility/constants.cpp

@@ -59,50 +59,6 @@ namespace storm {
             return value;
         }
         
-          // For floats we specialize this class and consider the comparison modulo some predefined precision.
-        template<>
-        class ConstantsComparator<float> {
-        public:
-            ConstantsComparator();
-            
-            ConstantsComparator(float precision);
-            
-            bool isOne(float const& value) const;
-            
-            bool isZero(float const& value) const;
-            
-            bool isEqual(float const& value1, float const& value2) const;
-            
-            bool isConstant(float const& value) const;
-            
-        private:
-            // The precision used for comparisons.
-            float precision;
-        };
-        
-        // For doubles we specialize this class and consider the comparison modulo some predefined precision.
-        template<>
-        class ConstantsComparator<double> {
-        public:
-            ConstantsComparator();
-            
-            ConstantsComparator(double precision);
-            
-            bool isOne(double const& value) const;
-            
-            bool isZero(double const& value) const;
-            
-            bool isInfinity(double const& value) const;
-            
-            bool isEqual(double const& value1, double const& value2) const;
-            
-            bool isConstant(double const& value) const;
-            
-        private:
-            // The precision used for comparisons.
-            double precision;
-        };
-        
 #ifdef STORM_HAVE_CARL
         template<>
         RationalFunction& simplify(RationalFunction& value);
@@ -184,7 +140,6 @@ namespace storm {
         }
         
         bool ConstantsComparator<double>::isOne(double const& value) const {
-            std::cout << std::setprecision(10) << std::abs(value - one<double>()) << " prec: " << precision << std::endl;
             return std::abs(value - one<double>()) <= precision;
         }
         
@@ -279,8 +234,8 @@ namespace storm {
             return std::move(matrixEntry);
         }
         
-		//explicit instantiations
-		//double
+		// explicit instantiations
+		// double
 		template class ConstantsComparator<double>;
 
 		template double one();
@@ -295,7 +250,7 @@ namespace storm {
 		template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& matrixEntry);
 		template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& matrixEntry);
 
-		//float
+		// float
 		template class ConstantsComparator<float>;
 
 		template float one();
@@ -310,7 +265,7 @@ namespace storm {
 		template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& matrixEntry);
 		template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>&& matrixEntry);
 
-		//int
+		// int
         template class ConstantsComparator<int>;
         
         template int one();

src/utility/constants.h

@@ -30,7 +30,6 @@ namespace storm {
         
         template<typename ValueType>
         ValueType infinity();
-     
         
         template<typename ValueType>
         ValueType pow(ValueType const& value, uint_fast64_t exponent);
@@ -53,6 +52,50 @@ namespace storm {
             bool isInfinity(ValueType const& value) const;
         };
         
+        // For floats we specialize this class and consider the comparison modulo some predefined precision.
+        template<>
+        class ConstantsComparator<float> {
+            public:
+            ConstantsComparator();
+            
+            ConstantsComparator(float precision);
+            
+            bool isOne(float const& value) const;
+            
+            bool isZero(float const& value) const;
+            
+            bool isEqual(float const& value1, float const& value2) const;
+            
+            bool isConstant(float const& value) const;
+            
+            private:
+            // The precision used for comparisons.
+            float precision;
+        };
+        
+        // For doubles we specialize this class and consider the comparison modulo some predefined precision.
+        template<>
+        class ConstantsComparator<double> {
+            public:
+            ConstantsComparator();
+            
+            ConstantsComparator(double precision);
+            
+            bool isOne(double const& value) const;
+            
+            bool isZero(double const& value) const;
+            
+            bool isInfinity(double const& value) const;
+            
+            bool isEqual(double const& value1, double const& value2) const;
+            
+            bool isConstant(double const& value) const;
+            
+            private:
+            // The precision used for comparisons.
+            double precision;
+        };
+        
         template<typename IndexType, typename ValueType>
         storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry);
 

src/utility/vector.h

@@ -165,6 +165,7 @@ namespace storm {
                     while (current < next) {
                         *targetIt += *sourceIt;
                         ++targetIt;
+                        ++current;
                     }
                 }
             }

test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp

@@ -29,6 +29,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Cluster) {
 #else
 	typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
 #endif
+    options.buildAllRewardModels = false;
     options.rewardModelsToBuild.insert("num_repairs");
     std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
     ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
@@ -111,7 +112,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Embedded) {
 #else
 	typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
 #endif
-
+    options.buildAllRewardModels = false;
     options.rewardModelsToBuild.insert("up");
     std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
     ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());

test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp

@@ -32,6 +32,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) {
 #else
 	typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
 #endif
+    options.buildAllRewardModels = false;
     options.rewardModelsToBuild.insert("num_repairs");
     std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
     ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
@@ -128,6 +129,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded) {
 #else
 	typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
 #endif
+    options.buildAllRewardModels = false;
     options.rewardModelsToBuild.insert("up");
     std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
     ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
@@ -250,6 +252,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem) {
 #else
 	typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
 #endif
+    options.buildAllRewardModels = false;
     options.rewardModelsToBuild.insert("customers");
     std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
     ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());

test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp

@@ -23,6 +23,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die) {
 #else
 	typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
 #endif
+    options.buildAllRewardModels = false;
     options.rewardModelsToBuild.insert("coin_flips");
     std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
     EXPECT_EQ(13ul, model->getNumberOfStates());
@@ -128,6 +129,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader) {
 #else
 	typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
 #endif
+    options.buildAllRewardModels = false;
     options.rewardModelsToBuild.insert("num_rounds");
     std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
     EXPECT_EQ(273ul, model->getNumberOfStates());

test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp

@@ -29,6 +29,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) {
 #else
 	typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
 #endif
+    options.buildAllRewardModels = false;
     options.rewardModelsToBuild.insert("coinflips");
     std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
     EXPECT_EQ(169ul, model->getNumberOfStates());
@@ -125,6 +126,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) {
 #else
 	typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
 #endif
+    options.buildAllRewardModels = false;
     options.rewardModelsToBuild.insert("rounds");
     std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
     EXPECT_EQ(3172ul, model->getNumberOfStates());

test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp

@@ -29,6 +29,7 @@ TEST(SparseCtmcCslModelCheckerTest, Cluster) {
 #else
 	typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
 #endif
+    options.buildAllRewardModels = false;
     options.rewardModelsToBuild.insert("num_repairs");
     std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
     ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
@@ -104,6 +105,7 @@ TEST(SparseCtmcCslModelCheckerTest, Embedded) {
 #else
 	typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
 #endif
+    options.buildAllRewardModels = false;
     options.rewardModelsToBuild.insert("up");
     std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
     ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
@@ -199,6 +201,7 @@ TEST(SparseCtmcCslModelCheckerTest, Tandem) {
 #else
 	typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
 #endif
+    options.buildAllRewardModels = false;
     options.rewardModelsToBuild.insert("customers");
     std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
     ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());

test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp

@@ -31,6 +31,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster) {
 #else
 	typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
 #endif
+    options.buildAllRewardModels = false;
     options.rewardModelsToBuild.insert("num_repairs");
     std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
     ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
@@ -119,6 +120,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded) {
 #else
 	typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
 #endif
+    options.buildAllRewardModels = false;
     options.rewardModelsToBuild.insert("up");
     std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
     ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
@@ -224,6 +226,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem) {
 #else
 	typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
 #endif
+    options.buildAllRewardModels = false;
     options.rewardModelsToBuild.insert("customers");
     std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
     ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());

test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp

@@ -24,6 +24,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die) {
 #else
 	typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
 #endif
+    options.buildAllRewardModels = false;
     options.rewardModelsToBuild.insert("coin_flips");
     std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
     EXPECT_EQ(13ul, model->getNumberOfStates());
@@ -129,6 +130,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader) {
 #else
 	typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
 #endif
+    options.buildAllRewardModels = false;
     options.rewardModelsToBuild.insert("num_rounds");
     std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
     EXPECT_EQ(273ul, model->getNumberOfStates());

test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp

@@ -27,6 +27,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) {
 #else
 	typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
 #endif
+    options.buildAllRewardModels = false;
     options.rewardModelsToBuild.insert("coinflips");
     std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
     EXPECT_EQ(169ul, model->getNumberOfStates());
@@ -123,6 +124,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) {
 #else
 	typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
 #endif
+    options.buildAllRewardModels = false;
     options.rewardModelsToBuild.insert("rounds");
     std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
     EXPECT_EQ(3172ul, model->getNumberOfStates());

test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp

@@ -22,6 +22,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die) {
 #else
     typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
 #endif
+    options.buildAllRewardModels = false;
     options.rewardModelsToBuild.insert("coin_flips");
     std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
     EXPECT_EQ(13ul, model->getNumberOfStates());
@@ -127,6 +128,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader) {
 #else
     typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
 #endif
+    options.buildAllRewardModels = false;
     options.rewardModelsToBuild.insert("num_rounds");
     std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
     EXPECT_EQ(273ul, model->getNumberOfStates());