fixed bug and added testsfor symbolic linear equation solver (rational number and rational function)

resources/3rdparty/sylvan/src/storm_wrapper.cpp

@@ -484,7 +484,7 @@ storm_rational_function_ptr storm_rational_function_divide(storm_rational_functi
     storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b;
     
     storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a);
-    *result_srf *= srf_b;
+    *result_srf /= srf_b;
     return (storm_rational_function_ptr)result_srf;
 }
 

resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c

@@ -623,7 +623,7 @@ TASK_IMPL_1(MTBDD, sylvan_storm_rational_number_minimum, MTBDD, a) {
     if (cache_get3(CACHE_MTBDD_MINIMUM_RN, a, 0, 0, &result)) return result;
     
     /* Call recursive */
-    SPAWN(mtbdd_minimum, node_getlow(a, na));
+    SPAWN(sylvan_storm_rational_number_minimum, node_getlow(a, na));
     MTBDD high = CALL(sylvan_storm_rational_number_minimum, node_gethigh(a, na));
     MTBDD low = SYNC(sylvan_storm_rational_number_minimum);
     
@@ -656,7 +656,7 @@ TASK_IMPL_1(MTBDD, sylvan_storm_rational_number_maximum, MTBDD, a)
     if (cache_get3(CACHE_MTBDD_MAXIMUM_RN, a, 0, 0, &result)) return result;
     
     /* Call recursive */
-    SPAWN(mtbdd_minimum, node_getlow(a, na));
+    SPAWN(sylvan_storm_rational_number_maximum, node_getlow(a, na));
     MTBDD high = CALL(sylvan_storm_rational_number_maximum, node_gethigh(a, na));
     MTBDD low = SYNC(sylvan_storm_rational_number_maximum);
     

src/storm/builder/DdJaniModelBuilder.cpp

@@ -133,6 +133,65 @@ namespace storm {
             labelNames.insert(labelName);
         }
 
+        template <storm::dd::DdType Type, typename ValueType>
+        class ParameterCreator {
+        public:
+            void create(storm::jani::Model const& model, storm::adapters::AddExpressionAdapter<Type, ValueType>& rowExpressionAdapter, storm::adapters::AddExpressionAdapter<Type, ValueType>& columnExpressionAdapter) {
+                // Intentionally left empty: no support for parameters for this data type.
+            }
+            
+            std::set<storm::RationalFunctionVariable> const& getParameters() const {
+                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Creating parameters for non-parametric model is not supported.");
+            }
+            
+        private:
+            
+        };
+        
+        template <storm::dd::DdType Type>
+        class ParameterCreator<Type, storm::RationalFunction> {
+        public:
+            ParameterCreator() : cache(std::make_shared<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>>()) {
+                // Intentionally left empty.
+            }
+            
+            void create(storm::jani::Model const& model, storm::adapters::AddExpressionAdapter<Type, storm::RationalFunction>& rowExpressionAdapter, storm::adapters::AddExpressionAdapter<Type, storm::RationalFunction>& columnExpressionAdapter) {
+                for (auto const& constant : model.getConstants()) {
+                    if (!constant.isDefined()) {
+                        carl::Variable carlVariable = carl::freshRealVariable(constant.getExpressionVariable().getName());
+                        parameters.insert(carlVariable);
+                        auto rf = convertVariableToPolynomial(carlVariable);
+                        rowExpressionAdapter.setValue(constant.getExpressionVariable(), rf);
+                        columnExpressionAdapter.setValue(constant.getExpressionVariable(), rf);
+                    }
+                }
+            }
+            
+            template<typename RationalFunctionType = storm::RationalFunction, typename TP = typename RationalFunctionType::PolyType, carl::EnableIf<carl::needs_cache<TP>> = carl::dummy>
+            RationalFunctionType convertVariableToPolynomial(carl::Variable const& variable) {
+                return RationalFunctionType(typename RationalFunctionType::PolyType(typename RationalFunctionType::PolyType::PolyType(variable), cache));
+            }
+            
+            template<typename RationalFunctionType = storm::RationalFunction, typename TP = typename RationalFunctionType::PolyType, carl::DisableIf<carl::needs_cache<TP>> = carl::dummy>
+            RationalFunctionType convertVariableToPolynomial(carl::Variable const& variable) {
+                return RationalFunctionType(variable);
+            }
+            
+            std::set<storm::RationalFunctionVariable> const& getParameters() const {
+                return parameters;
+            }
+            
+        private:
+            // A mapping from our variables to carl's.
+            std::unordered_map<storm::expressions::Variable, carl::Variable> variableToVariableMap;
+            
+            // The cache that is used in case the underlying type needs a cache.
+            std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache;
+            
+            // All created parameters.
+            std::set<storm::RationalFunctionVariable> parameters;
+        };
+        
         template <storm::dd::DdType Type, typename ValueType>
         struct CompositionVariables {
             CompositionVariables() : manager(std::make_shared<storm::dd::DdManager<Type>>()),
@@ -191,6 +250,9 @@ namespace storm {
             
             // A DD representing the valid ranges of the global variables.
             storm::dd::Add<Type, ValueType> globalVariableRanges;
+            
+            // The parameters that appear in the model.
+            std::set<storm::RationalFunctionVariable> parameters;
         };
         
         // A class responsible for creating the necessary variables for a subsequent composition of automata.
@@ -324,6 +386,12 @@ namespace storm {
                     result.automatonToRangeMap[automaton.getName()] = (range && globalVariableRanges).template toAdd<ValueType>();
                 }
                 
+                ParameterCreator<Type, ValueType> parameterCreator;
+                parameterCreator.create(model, *result.rowExpressionAdapter, *result.columnExpressionAdapter);
+                if (std::is_same<ValueType, storm::RationalFunction>::value) {
+                    result.parameters = parameterCreator.getParameters();
+                }
+                
                 return result;
             }
             
@@ -1631,16 +1699,22 @@ namespace storm {
         
         template <storm::dd::DdType Type, typename ValueType>
         std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> createModel(storm::jani::ModelType const& modelType, CompositionVariables<Type, ValueType> const& variables, ModelComponents<Type, ValueType> const& modelComponents) {
-            
+            std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> result;
             if (modelType == storm::jani::ModelType::DTMC) {
-                return std::make_shared<storm::models::symbolic::Dtmc<Type, ValueType>>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, modelComponents.labelToExpressionMap, modelComponents.rewardModels);
+                result = std::make_shared<storm::models::symbolic::Dtmc<Type, ValueType>>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, modelComponents.labelToExpressionMap, modelComponents.rewardModels);
             } else if (modelType == storm::jani::ModelType::CTMC) {
-                return std::make_shared<storm::models::symbolic::Ctmc<Type, ValueType>>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, modelComponents.labelToExpressionMap, modelComponents.rewardModels);
+                result = std::make_shared<storm::models::symbolic::Ctmc<Type, ValueType>>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, modelComponents.labelToExpressionMap, modelComponents.rewardModels);
             } else if (modelType == storm::jani::ModelType::MDP) {
-                return std::make_shared<storm::models::symbolic::Mdp<Type, ValueType>>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, modelComponents.labelToExpressionMap, modelComponents.rewardModels);
+                result = std::make_shared<storm::models::symbolic::Mdp<Type, ValueType>>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, modelComponents.labelToExpressionMap, modelComponents.rewardModels);
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Invalid model type.");
             }
+            
+            if (std::is_same<ValueType, storm::RationalFunction>::value) {
+                result->addParameters(variables.parameters);
+            }
+            
+            return result;
         }
         
         template <storm::dd::DdType Type, typename ValueType>

src/storm/builder/DdPrismModelBuilder.cpp

@@ -37,6 +37,13 @@ namespace storm {
             void create(storm::prism::Program const& program, storm::adapters::AddExpressionAdapter<Type, ValueType>& rowExpressionAdapter, storm::adapters::AddExpressionAdapter<Type, ValueType>& columnExpressionAdapter) {
                 // Intentionally left empty: no support for parameters for this data type.
             }
+            
+            std::set<storm::RationalFunctionVariable> const& getParameters() const {
+                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Creating parameters for non-parametric model is not supported.");
+            }
+
+        private:
+            
         };
         
         template <storm::dd::DdType Type>
@@ -50,6 +57,7 @@ namespace storm {
                 for (auto const& constant : program.getConstants()) {
                     if (!constant.isDefined()) {
                         carl::Variable carlVariable = carl::freshRealVariable(constant.getExpressionVariable().getName());
+                        parameters.insert(carlVariable);
                         auto rf = convertVariableToPolynomial(carlVariable);
                         rowExpressionAdapter.setValue(constant.getExpressionVariable(), rf);
                         columnExpressionAdapter.setValue(constant.getExpressionVariable(), rf);
@@ -67,17 +75,25 @@ namespace storm {
                 return RationalFunctionType(variable);
             }
             
+            std::set<storm::RationalFunctionVariable> const& getParameters() const {
+                return parameters;
+            }
+            
+        private:
             // A mapping from our variables to carl's.
             std::unordered_map<storm::expressions::Variable, carl::Variable> variableToVariableMap;
             
             // The cache that is used in case the underlying type needs a cache.
             std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache;
+            
+            // All created parameters.
+            std::set<storm::RationalFunctionVariable> parameters;
         };
         
         template <storm::dd::DdType Type, typename ValueType>
         class DdPrismModelBuilder<Type, ValueType>::GenerationInformation {
         public:
-            GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared<storm::dd::DdManager<Type>>()), rowMetaVariables(), variableToRowMetaVariableMap(std::make_shared<std::map<storm::expressions::Variable, storm::expressions::Variable>>()), rowExpressionAdapter(std::make_shared<storm::adapters::AddExpressionAdapter<Type, ValueType>>(manager, variableToRowMetaVariableMap)), columnMetaVariables(), variableToColumnMetaVariableMap((std::make_shared<std::map<storm::expressions::Variable, storm::expressions::Variable>>())), columnExpressionAdapter(std::make_shared<storm::adapters::AddExpressionAdapter<Type, ValueType>>(manager, variableToColumnMetaVariableMap)), rowColumnMetaVariablePairs(), nondeterminismMetaVariables(), variableToIdentityMap(), allGlobalVariables(), moduleToIdentityMap() {
+            GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared<storm::dd::DdManager<Type>>()), rowMetaVariables(), variableToRowMetaVariableMap(std::make_shared<std::map<storm::expressions::Variable, storm::expressions::Variable>>()), rowExpressionAdapter(std::make_shared<storm::adapters::AddExpressionAdapter<Type, ValueType>>(manager, variableToRowMetaVariableMap)), columnMetaVariables(), variableToColumnMetaVariableMap((std::make_shared<std::map<storm::expressions::Variable, storm::expressions::Variable>>())), columnExpressionAdapter(std::make_shared<storm::adapters::AddExpressionAdapter<Type, ValueType>>(manager, variableToColumnMetaVariableMap)), rowColumnMetaVariablePairs(), nondeterminismMetaVariables(), variableToIdentityMap(), allGlobalVariables(), moduleToIdentityMap(), parameters() {
                 
                 // Initializes variables and identity DDs.
                 createMetaVariablesAndIdentities();
@@ -85,6 +101,9 @@ namespace storm {
                 // Initialize the parameters (if any).
                 ParameterCreator<Type, ValueType> parameterCreator;
                 parameterCreator.create(this->program, *this->rowExpressionAdapter, *this->columnExpressionAdapter);
+                if (std::is_same<ValueType, storm::RationalFunction>::value) {
+                    this->parameters = parameterCreator.getParameters();
+                }
             }
             
             // The program that is currently translated.
@@ -131,11 +150,10 @@ namespace storm {
             // DDs representing the valid ranges of the variables of each module.
             std::map<std::string, storm::dd::Add<Type, ValueType>> moduleToRangeMap;
             
-        private:
-            void createParameters() {
-                
-            }
+            // The parameters appearing in the model.
+            std::set<storm::RationalFunctionVariable> parameters;
             
+        private:
             /*!
              * Creates the required meta variables and variable/module identities.
              */
@@ -1464,15 +1482,22 @@ namespace storm {
                 labelToExpressionMapping.emplace(label.getName(), label.getStatePredicateExpression());
             }
             
+            std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> result;
             if (program.getModelType() == storm::prism::Program::ModelType::DTMC) {
-                return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Dtmc<Type, ValueType>(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels));
+                result = std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Dtmc<Type, ValueType>(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels));
             } else if (program.getModelType() == storm::prism::Program::ModelType::CTMC) {
-                return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Ctmc<Type, ValueType>(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, system.stateActionDd, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels));
+                result = std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Ctmc<Type, ValueType>(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, system.stateActionDd, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels));
             } else if (program.getModelType() == storm::prism::Program::ModelType::MDP) {
-                return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Mdp<Type, ValueType>(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, generationInfo.allNondeterminismVariables, labelToExpressionMapping, rewardModels));
+                result = std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Mdp<Type, ValueType>(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, generationInfo.allNondeterminismVariables, labelToExpressionMapping, rewardModels));
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid model type.");
             }
+            
+            if (std::is_same<ValueType, storm::RationalFunction>::value) {
+                result->addParameters(generationInfo.parameters);
+            }
+            
+            return result;
         }
         
         template <storm::dd::DdType Type, typename ValueType>

src/storm/modelchecker/results/CheckResult.cpp

@@ -173,6 +173,10 @@ namespace storm {
         template SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan> const& CheckResult::asSymbolicQualitativeCheckResult() const;
         template SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>& CheckResult::asSymbolicQuantitativeCheckResult();
         template SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double> const& CheckResult::asSymbolicQuantitativeCheckResult() const;
+        template SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalNumber>& CheckResult::asSymbolicQuantitativeCheckResult();
+        template SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalNumber> const& CheckResult::asSymbolicQuantitativeCheckResult() const;
+        template SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>& CheckResult::asSymbolicQuantitativeCheckResult();
+        template SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction> const& CheckResult::asSymbolicQuantitativeCheckResult() const;
         template SymbolicParetoCurveCheckResult<storm::dd::DdType::Sylvan, double>& CheckResult::asSymbolicParetoCurveCheckResult();
         template SymbolicParetoCurveCheckResult<storm::dd::DdType::Sylvan, double> const& CheckResult::asSymbolicParetoCurveCheckResult() const;
         template HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>& CheckResult::asHybridQuantitativeCheckResult();

src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.h

@@ -37,7 +37,6 @@ namespace storm {
             virtual void filter(QualitativeCheckResult const& filter) override;
             
             virtual ValueType getMin() const override;
-            
             virtual ValueType getMax() const override;
             
             virtual ValueType average() const override;

src/storm/models/symbolic/Model.cpp

@@ -13,10 +13,10 @@
 
 #include "storm/models/symbolic/StandardRewardModel.h"
 
+#include "storm/utility/macros.h"
 #include "storm/utility/dd.h"
 
-#include "storm-config.h"
-#include "storm/adapters/CarlAdapter.h"
+#include "storm/exceptions/NotSupportedException.h"
 
 namespace storm {
     namespace models {
@@ -268,6 +268,26 @@ namespace storm {
                 return true;
             }
             
+            template<storm::dd::DdType Type, typename ValueType>
+            void Model<Type, ValueType>::addParameters(std::set<storm::RationalFunctionVariable> const& parameters) {
+                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This value type does not support parameters.");
+            }
+            
+            template<storm::dd::DdType Type, typename ValueType>
+            std::set<storm::RationalFunctionVariable> const& Model<Type, ValueType>::getParameters() const {
+                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This value type does not support parameters.");
+            }
+
+            template<>
+            void Model<storm::dd::DdType::Sylvan, storm::RationalFunction>::addParameters(std::set<storm::RationalFunctionVariable> const& parameters) {
+                this->parameters.insert(parameters.begin(), parameters.end());
+            }
+            
+            template<>
+            std::set<storm::RationalFunctionVariable> const& Model<storm::dd::DdType::Sylvan, storm::RationalFunction>::getParameters() const {
+                return parameters;
+            }
+
             // Explicitly instantiate the template class.
             template class Model<storm::dd::DdType::CUDD, double>;
             template class Model<storm::dd::DdType::Sylvan, double>;

src/storm/models/symbolic/Model.h

@@ -12,6 +12,9 @@
 #include "storm/models/ModelBase.h"
 #include "storm/utility/OsDetection.h"
 
+#include "storm-config.h"
+#include "storm/adapters/CarlAdapter.h"
+
 namespace storm {
     namespace dd {
         
@@ -267,6 +270,10 @@ namespace storm {
 
                 std::vector<std::string> getLabels() const;
                 
+                void addParameters(std::set<storm::RationalFunctionVariable> const& parameters);
+                
+                std::set<storm::RationalFunctionVariable> const& getParameters() const;
+                
             protected:
                 
                 /*!
@@ -349,6 +356,9 @@ namespace storm {
                 
                 // The reward models associated with the model.
                 std::unordered_map<std::string, RewardModelType> rewardModels;
+                
+                // The parameters. Only meaningful for models over rational functions.
+                std::set<storm::RationalFunctionVariable> parameters;
             };
             
         } // namespace symbolic

src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp

@@ -21,10 +21,18 @@ namespace storm {
                 storm::dd::DdMetaVariable<DdType> const& metaVariable = ddManager.getMetaVariable(rowVariable);
                 
                 std::vector<storm::expressions::Variable> newMetaVariables;
+                
+                // Find a suitable name for the temporary variable.
+                uint64_t counter = 0;
+                std::string newMetaVariableName = "tmp_" + metaVariable.getName();
+                while (ddManager.hasMetaVariable(newMetaVariableName + std::to_string(counter))) {
+                    ++counter;
+                }
+                
                 if (metaVariable.getType() == storm::dd::MetaVariableType::Bool) {
-                    newMetaVariables = ddManager.addMetaVariable("tmp_" + metaVariable.getName(), 3);
+                    newMetaVariables = ddManager.addMetaVariable(newMetaVariableName + std::to_string(counter), 3);
                 } else {
-                    newMetaVariables = ddManager.addMetaVariable("tmp_" + metaVariable.getName(), metaVariable.getLow(), metaVariable.getHigh(), 3);
+                    newMetaVariables = ddManager.addMetaVariable(newMetaVariableName + std::to_string(counter), metaVariable.getLow(), metaVariable.getHigh(), 3);
                 }
                 
                 newRowVariables.insert(newMetaVariables[0]);
@@ -56,7 +64,7 @@ namespace storm {
             storm::dd::DdManager<DdType>& ddManager = x.getDdManager();
             
             // Build diagonal BDD over new meta variables.
-            storm::dd::Bdd<DdType> diagonal = storm::utility::dd::getRowColumnDiagonal(x.getDdManager(), this->rowColumnMetaVariablePairs);
+            storm::dd::Bdd<DdType> diagonal = storm::utility::dd::getRowColumnDiagonal(ddManager, this->rowColumnMetaVariablePairs);
             diagonal &= this->allRows;
             diagonal = diagonal.swapVariables(this->oldNewMetaVariablePairs);
 
@@ -72,11 +80,12 @@ namespace storm {
             // As long as there are transitions, we eliminate them.
             uint64_t iterations = 0;
             while (!matrix.isZero()) {
-                // Determine inverse loop probabilies
+                // Determine inverse loop probabilies.
                 storm::dd::Add<DdType, ValueType> inverseLoopProbabilities = rowsAdd / (rowsAdd - (diagonalAdd * matrix).sumAbstract(newColumnVariables));
                 
                 // Scale all transitions with the inverse loop probabilities.
                 matrix *= inverseLoopProbabilities;
+                
                 solution *= inverseLoopProbabilities;
                 
                 // Delete diagonal elements, i.e. remove self-loops.

src/storm/solver/SymbolicEliminationLinearEquationSolver.h

@@ -32,7 +32,7 @@ namespace storm {
         };
         
         template<storm::dd::DdType DdType, typename ValueType>
-        class SymbolicEliminationLinearEquationSolverFactory {
+        class SymbolicEliminationLinearEquationSolverFactory : public SymbolicLinearEquationSolverFactory<DdType, ValueType> {
         public:
             virtual std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>> create(storm::dd::Add<DdType, ValueType> const& A, storm::dd::Bdd<DdType> const& allRows, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs) const;
             

src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp

@@ -155,15 +155,14 @@ namespace storm {
                 storm::dd::Add<DdType, ValueType> schedulerX = linearEquationSolver->solveEquations(currentSolution, schedulerB);
                 
                 // Policy improvement step.
-                storm::dd::Add<DdType, ValueType> tmp = this->A.multiplyMatrix(schedulerX.swapVariables(this->rowColumnMetaVariablePairs), this->columnMetaVariables);
-                tmp += b;
+                storm::dd::Add<DdType, ValueType> choiceValues = this->A.multiplyMatrix(schedulerX.swapVariables(this->rowColumnMetaVariablePairs), this->columnMetaVariables) + b;
                 
                 storm::dd::Bdd<DdType> nextScheduler;
                 if (minimize) {
-                    tmp += illegalMaskAdd;
-                    nextScheduler = tmp.minAbstractRepresentative(this->choiceVariables);
+                    choiceValues += illegalMaskAdd;
+                    nextScheduler = choiceValues.minAbstractRepresentative(this->choiceVariables);
                 } else {
-                    nextScheduler = tmp.maxAbstractRepresentative(this->choiceVariables);
+                    nextScheduler = choiceValues.maxAbstractRepresentative(this->choiceVariables);
                 }
                 
                 // Check for convergence.

src/storm/utility/constants.cpp

@@ -216,7 +216,7 @@ namespace storm {
         template<>
         storm::ClnRationalNumber infinity() {
             // FIXME: this should be treated more properly.
-            return storm::ClnRationalNumber(-1);
+            return storm::ClnRationalNumber(100000000000);
         }
 
         template<>
@@ -326,7 +326,7 @@ namespace storm {
         template<>
         storm::GmpRationalNumber infinity() {
             // FIXME: this should be treated more properly.
-            return storm::GmpRationalNumber(-1);
+            return storm::GmpRationalNumber(100000000000);
         }
         
         template<>
@@ -468,7 +468,7 @@ namespace storm {
         template<>
         storm::RationalFunction infinity() {
             // FIXME: this should be treated more properly.
-            return storm::RationalFunction(-1.0);
+            return storm::RationalFunction(convertNumber<RationalFunctionCoefficient>(100000000000));
         }
         
         template<>

src/test/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp

@@ -8,6 +8,7 @@
 #include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h"
 #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
 #include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h"
+#include "storm/solver/SymbolicEliminationLinearEquationSolver.h"
 #include "storm/parser/PrismParser.h"
 #include "storm/builder/DdPrismModelBuilder.h"
 #include "storm/models/symbolic/StandardRewardModel.h"
@@ -41,7 +42,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Cudd) {
     
     std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>>();
     
-    storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>> checker(*dtmc, std::unique_ptr<storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
+    storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>> checker(*dtmc, std::unique_ptr<storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::solver::GeneralSymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
     
     std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
     
@@ -103,7 +104,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Sylvan) {
     
     std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>>();
     
-    storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>> checker(*dtmc, std::unique_ptr<storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
+    storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>> checker(*dtmc, std::unique_ptr<storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::solver::GeneralSymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
     
     std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
     
@@ -143,6 +144,122 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Sylvan) {
     EXPECT_NEAR(3.6666622161865234, quantitativeResult4.getMax(), 10 * storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
 }
 
+TEST(SymbolicDtmcPrctlModelCheckerTest, Die_RationalNumber_Sylvan) {
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
+    
+    // A parser that we use for conveniently constructing the formulas.
+    storm::parser::FormulaParser formulaParser;
+    
+    // Build the die model with its reward model.
+    typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan, storm::RationalNumber>::Options options;
+    options.buildAllRewardModels = false;
+    options.rewardModelsToBuild.insert("coin_flips");
+    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan, storm::RationalNumber>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan, storm::RationalNumber>().build(program, options);
+    EXPECT_EQ(13ul, model->getNumberOfStates());
+    EXPECT_EQ(20ul, model->getNumberOfTransitions());
+    
+    ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
+    
+    std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, storm::RationalNumber>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, storm::RationalNumber>>();
+    
+    storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, storm::RationalNumber>> checker(*dtmc, std::unique_ptr<storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, storm::RationalNumber>>(new storm::solver::SymbolicEliminationLinearEquationSolverFactory<storm::dd::DdType::Sylvan, storm::RationalNumber>()));
+    
+    std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
+    
+    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
+    storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalNumber>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalNumber>();
+    
+    EXPECT_EQ(quantitativeResult1.getMin(), storm::utility::convertNumber<storm::RationalNumber>(std::string("1/6")));
+    EXPECT_EQ(quantitativeResult1.getMax(), storm::utility::convertNumber<storm::RationalNumber>(std::string("1/6")));
+    
+    formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
+    
+    result = checker.check(*formula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
+    storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalNumber>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalNumber>();
+    
+    EXPECT_EQ(quantitativeResult2.getMin(), storm::utility::convertNumber<storm::RationalNumber>(std::string("1/6")));
+    EXPECT_EQ(quantitativeResult2.getMax(), storm::utility::convertNumber<storm::RationalNumber>(std::string("1/6")));
+    
+    formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]");
+    
+    result = checker.check(*formula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
+    storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalNumber>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalNumber>();
+    
+    EXPECT_EQ(quantitativeResult3.getMin(), storm::utility::convertNumber<storm::RationalNumber>(std::string("1/6")));
+    EXPECT_EQ(quantitativeResult3.getMax(), storm::utility::convertNumber<storm::RationalNumber>(std::string("1/6")));
+    
+    formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]");
+    
+    result = checker.check(*formula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
+    storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalNumber>& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalNumber>();
+    
+    EXPECT_EQ(quantitativeResult4.getMin(), storm::utility::convertNumber<storm::RationalNumber>(std::string("11/3")));
+    EXPECT_EQ(quantitativeResult4.getMax(), storm::utility::convertNumber<storm::RationalNumber>(std::string("11/3")));
+}
+
+TEST(SymbolicDtmcPrctlModelCheckerTest, Die_RationalFunction_Sylvan) {
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pdtmc/parametric_die.pm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
+    
+    // A parser that we use for conveniently constructing the formulas.
+    storm::parser::FormulaParser formulaParser;
+    
+    // Build the die model with its reward model.
+    typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan, storm::RationalFunction>::Options options;
+    options.buildAllRewardModels = false;
+    options.rewardModelsToBuild.insert("coin_flips");
+    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan, storm::RationalFunction>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan, storm::RationalFunction>().build(program, options);
+    EXPECT_EQ(13ul, model->getNumberOfStates());
+    EXPECT_EQ(20ul, model->getNumberOfTransitions());
+    ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
+    
+    std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> instantiation;
+    std::set<storm::RationalFunctionVariable> variables = model->getParameters();
+    ASSERT_EQ(1ull, variables.size());
+    instantiation.emplace(*variables.begin(), storm::utility::convertNumber<storm::RationalFunctionCoefficient>(std::string("1/2")));
+    
+    std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, storm::RationalFunction>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, storm::RationalFunction>>();
+    
+    storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, storm::RationalFunction>> checker(*dtmc, std::unique_ptr<storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, storm::RationalFunction>>(new storm::solver::SymbolicEliminationLinearEquationSolverFactory<storm::dd::DdType::Sylvan, storm::RationalFunction>()));
+    
+    std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
+    
+    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
+    storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>();
+    
+    EXPECT_EQ(storm::utility::convertNumber<storm::RationalFunctionCoefficient>(quantitativeResult1.sum().evaluate(instantiation)), storm::utility::convertNumber<storm::RationalFunctionCoefficient>(std::string("1/6")));
+    
+    formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
+    
+    result = checker.check(*formula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
+    storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>();
+    
+    EXPECT_EQ(storm::utility::convertNumber<storm::RationalFunctionCoefficient>(quantitativeResult2.sum().evaluate(instantiation)), storm::utility::convertNumber<storm::RationalFunctionCoefficient>(std::string("1/6")));
+    
+    formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]");
+    
+    result = checker.check(*formula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
+    storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>();
+    
+    EXPECT_EQ(storm::utility::convertNumber<storm::RationalFunctionCoefficient>(quantitativeResult3.sum().evaluate(instantiation)), storm::utility::convertNumber<storm::RationalFunctionCoefficient>(std::string("1/6")));
+    
+    formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]");
+    
+    result = checker.check(*formula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
+    storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>();
+    
+    EXPECT_EQ(storm::utility::convertNumber<storm::RationalFunctionCoefficient>(quantitativeResult4.sum().evaluate(instantiation)), storm::utility::convertNumber<storm::RationalFunctionCoefficient>(std::string("11/3")));
+}
+
 TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Cudd) {
     storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
     storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
@@ -158,7 +275,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Cudd) {
     
     std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>>();
     
-    storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>> checker(*dtmc, std::unique_ptr<storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
+    storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>> checker(*dtmc, std::unique_ptr<storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::solver::GeneralSymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
     
     std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
     
@@ -203,7 +320,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Sylvan) {
     
     std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>>();
     
-    storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>> checker(*dtmc, std::unique_ptr<storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
+    storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>> checker(*dtmc, std::unique_ptr<storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::solver::GeneralSymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
     
     std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
     
@@ -259,7 +376,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) {
     
     std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>>();
     
-    storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>> checker(*dtmc, std::unique_ptr<storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
+    storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>> checker(*dtmc, std::unique_ptr<storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::solver::GeneralSymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
     
     std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
     
@@ -312,7 +429,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) {
     
     std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>>();
     
-    storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>> checker(*dtmc, std::unique_ptr<storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
+    storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>> checker(*dtmc, std::unique_ptr<storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::solver::GeneralSymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
     
     std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
     

src/test/storage/SylvanDdTest.cpp

@@ -520,7 +520,7 @@ TEST(SylvanDd, RationalFunctionEncodingTest) {
     
     storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> add;
     ASSERT_NO_THROW(add = encoding.template toAdd<storm::RationalFunction>());
-
+    
     // As an MTBDD, the 0-leaf is there, so the count is actually 2 and the node count is 6.
     EXPECT_EQ(6ul, add.getNodeCount());
     EXPECT_EQ(2ul, add.getLeafCount());