merge fixes

Former-commit-id: ff5de6fc69

src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp

@@ -59,8 +59,10 @@ namespace storm {
             return result;
         }
         
-        
                 
         template class SparseMdpMultiObjectiveModelChecker<storm::models::sparse::Mdp<double>>;
+#ifdef STORM_HAVE_CARL
+        template class SparseMdpMultiObjectiveModelChecker<storm::models::sparse::Mdp<storm::RationalNumber>>;
+#endif
     }
 }

src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp

@@ -230,7 +230,7 @@ namespace storm {
             template <class SparseModelType, typename RationalNumberType>
             void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::performRefinementStep(WeightVector const& direction, bool saveScheduler, SparseMultiObjectiveWeightVectorChecker<SparseModelType>& weightVectorChecker, ResultData& result) {
                 weightVectorChecker.check(storm::utility::vector::convertNumericVector<typename SparseModelType::ValueType>(direction));
-                STORM_LOG_DEBUG("weighted objectives checker result is " << weightVectorChecker.getInitialStateResultOfObjectives());
+                STORM_LOG_DEBUG("weighted objectives checker result is " << storm::utility::vector::convertNumericVector<double>(weightVectorChecker.getInitialStateResultOfObjectives()));
                 if(saveScheduler) {
                     result.refinementSteps().emplace_back(direction, weightVectorChecker.template getInitialStateResultOfObjectives<RationalNumberType>(), weightVectorChecker.getScheduler());
                 } else {
@@ -308,6 +308,9 @@ namespace storm {
 #ifdef STORM_HAVE_CARL
             template class SparseMultiObjectiveHelper<storm::models::sparse::Mdp<double>, storm::RationalNumber>;
             template class SparseMultiObjectiveHelper<storm::models::sparse::MarkovAutomaton<double>, storm::RationalNumber>;
+            
+            template class SparseMultiObjectiveHelper<storm::models::sparse::Mdp<storm::RationalNumber>, storm::RationalNumber>;
+            template class SparseMultiObjectiveHelper<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>, storm::RationalNumber>;
 #endif
         }
     }

src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp

@@ -325,6 +325,9 @@ namespace storm {
 #ifdef STORM_HAVE_CARL
             template class SparseMultiObjectivePostprocessor<storm::models::sparse::Mdp<double>, storm::RationalNumber>;
             template class SparseMultiObjectivePostprocessor<storm::models::sparse::MarkovAutomaton<double>, storm::RationalNumber>;
+            
+            template class SparseMultiObjectivePostprocessor<storm::models::sparse::Mdp<storm::RationalNumber>, storm::RationalNumber>;
+            template class SparseMultiObjectivePostprocessor<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>, storm::RationalNumber>;
 #endif
             
         }

src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp

@@ -444,6 +444,11 @@ namespace storm {
             
             template class SparseMultiObjectivePreprocessor<storm::models::sparse::Mdp<double>>;
             template class SparseMultiObjectivePreprocessor<storm::models::sparse::MarkovAutomaton<double>>;
+            
+#ifdef STORM_HAVE_CARL
+            template class SparseMultiObjectivePreprocessor<storm::models::sparse::Mdp<storm::RationalNumber>>;
+            template class SparseMultiObjectivePreprocessor<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>;
+#endif
 
             
         }

src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp

@@ -11,7 +11,6 @@
 #include "src/transformer/NeutralECRemover.h"
 #include "src/utility/graph.h"
 #include "src/utility/macros.h"
-#include "src/utility/solver.h"
 #include "src/utility/vector.h"
 
 #include "src/exceptions/IllegalFunctionCallException.h"
@@ -32,7 +31,7 @@ namespace storm {
             template <class SparseModelType>
             void SparseMultiObjectiveWeightVectorChecker<SparseModelType>::check(std::vector<ValueType> const& weightVector) {
                 checkHasBeenCalled=true;
-                STORM_LOG_DEBUG("Invoked WeightVectorChecker with weights " << std::endl << "\t" << weightVector);
+                STORM_LOG_DEBUG("Invoked WeightVectorChecker with weights " << std::endl << "\t" << storm::utility::vector::convertNumericVector<double>(weightVector));
                 storm::storage::BitVector unboundedObjectives(data.objectives.size(), false);
                 std::vector<ValueType> weightedRewardVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero<ValueType>());
                 for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) {
@@ -44,9 +43,9 @@ namespace storm {
                 unboundedWeightedPhase(unboundedObjectives, weightedRewardVector);
                 STORM_LOG_DEBUG("Unbounded weighted phase result: " << weightedResult[data.preprocessedModel.getInitialStates().getNextSetIndex(0)] << " (value in initial state).");
                 unboundedIndividualPhase(weightVector);
-                STORM_LOG_DEBUG("Unbounded individual phase results in initial state: " << getInitialStateResultOfObjectives());
+                STORM_LOG_DEBUG("Unbounded individual phase results in initial state: " << getInitialStateResultOfObjectives<double>());
                 boundedPhase(weightVector, ~unboundedObjectives, weightedRewardVector);
-                STORM_LOG_DEBUG("Bounded individual phase results in initial state: " << getInitialStateResultOfObjectives() << " ...WeightVectorChecker done.");
+                STORM_LOG_DEBUG("Bounded individual phase results in initial state: " << getInitialStateResultOfObjectives<double>() << " ...WeightVectorChecker done.");
             }
             
             template <class SparseModelType>
@@ -83,13 +82,15 @@ namespace storm {
                 
                 std::vector<ValueType> subResult(removerResult.matrix.getRowGroupCount());
                 
-                storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> solverFactory;
-                std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = solverFactory.create(removerResult.matrix, true);
+                storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> solverFactory;
+                std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = solverFactory.create(removerResult.matrix);
                 solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize);
-                solver->solveEquationSystem(subResult, removerResult.vector);
+                solver->setTrackScheduler(true);
+                solver->solveEquations(subResult, removerResult.vector);
                 
                 this->weightedResult = std::vector<ValueType>(data.preprocessedModel.getNumberOfStates());
                 this->scheduler = storm::storage::TotalScheduler(data.preprocessedModel.getNumberOfStates());
+                std::unique_ptr<storm::storage::TotalScheduler>  solverScheduler = solver->getScheduler();
                 storm::storage::BitVector statesWithUndefinedScheduler(data.preprocessedModel.getNumberOfStates(), false);
                 for(uint_fast64_t state = 0; state < data.preprocessedModel.getNumberOfStates(); ++state) {
                     uint_fast64_t stateInReducedModel = removerResult.oldToNewStateMapping[state];
@@ -97,7 +98,7 @@ namespace storm {
                     if(stateInReducedModel < removerResult.matrix.getRowGroupCount()) {
                         this->weightedResult[state] = subResult[stateInReducedModel];
                         // Check if the chosen row originaly belonged to the current state
-                        uint_fast64_t chosenRowInReducedModel = removerResult.matrix.getRowGroupIndices()[stateInReducedModel] + solver->getScheduler().getChoice(stateInReducedModel);
+                        uint_fast64_t chosenRowInReducedModel = removerResult.matrix.getRowGroupIndices()[stateInReducedModel] + solverScheduler->getChoice(stateInReducedModel);
                         uint_fast64_t chosenRowInOriginalModel = removerResult.newToOldRowMapping[chosenRowInReducedModel];
                         if(chosenRowInOriginalModel >= data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state] &&
                            chosenRowInOriginalModel <  data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state+1]) {
@@ -139,7 +140,7 @@ namespace storm {
                 storm::storage::SparseMatrix<ValueType> deterministicMatrix = data.preprocessedModel.getTransitionMatrix().selectRowsFromRowGroups(this->scheduler.getChoices(), true);
                 storm::storage::SparseMatrix<ValueType> deterministicBackwardTransitions = deterministicMatrix.transpose();
                 std::vector<ValueType> deterministicStateRewards(deterministicMatrix.getRowCount());
-                storm::utility::solver::LinearEquationSolverFactory<ValueType> linearEquationSolverFactory;
+                storm::solver::GeneralLinearEquationSolverFactory<ValueType> linearEquationSolverFactory;
                 //TODO check if all but one entry of weightVector is zero
                 //Also only compute values for objectives with weightVector != zero,
                 //one check can be omitted as the result can be computed back from the weighed result and the results from the remaining objectives
@@ -224,6 +225,13 @@ namespace storm {
 #ifdef STORM_HAVE_CARL
             template std::vector<storm::RationalNumber> SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::Mdp<double>>::getInitialStateResultOfObjectives<storm::RationalNumber>() const;
             template std::vector<storm::RationalNumber> SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>::getInitialStateResultOfObjectives<storm::RationalNumber>() const;
+            
+            template class SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::Mdp<storm::RationalNumber>>;
+            template std::vector<double> SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::Mdp<storm::RationalNumber>>::getInitialStateResultOfObjectives<double>() const;
+            template class SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>;
+            template std::vector<double> SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>::getInitialStateResultOfObjectives<double>() const;
+            template std::vector<storm::RationalNumber> SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::Mdp<storm::RationalNumber>>::getInitialStateResultOfObjectives<storm::RationalNumber>() const;
+            template std::vector<storm::RationalNumber> SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>::getInitialStateResultOfObjectives<storm::RationalNumber>() const;
 #endif
             
         }

src/solver/StandardMinMaxLinearEquationSolver.cpp

@@ -233,6 +233,17 @@ namespace storm {
                 std::swap(x, *currentX);
             }
             
+            // If requested, we store the scheduler for retrieval.
+            if (this->isTrackSchedulerSet()) {
+                if(iterations==0){ //may happen due to custom termination condition. Then we need to compute x'= A*x+b
+                    solver->multiply(x, *multiplyResult, &b);
+                }
+                std::vector<storm::storage::sparse::state_type> choices(this->A.getRowGroupCount());
+                // Reduce the multiplyResult and keep track of the choices made
+                storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, x, this->A.getRowGroupIndices(), &choices);
+                this->scheduler = std::make_unique<storm::storage::TotalScheduler>(std::move(choices));
+            }
+            
             // Dispose of allocated scratch memory.
             if (!xMemoryProvided) {
                 delete copyX;
@@ -396,4 +407,4 @@ namespace storm {
         template class EliminationMinMaxLinearEquationSolverFactory<storm::RationalNumber>;
         
     }
-}
+}

src/storage/geometry/Polytope.cpp

@@ -265,11 +265,13 @@ namespace storm {
             }
             
             template class Polytope<double>;
+            template std::shared_ptr<Polytope<double>> Polytope<double>::convertNumberRepresentation() const;
             
 #ifdef STORM_HAVE_CARL
             template class Polytope<storm::RationalNumber>;
             template std::shared_ptr<Polytope<double>> Polytope<storm::RationalNumber>::convertNumberRepresentation() const;
             template std::shared_ptr<Polytope<storm::RationalNumber>> Polytope<double>::convertNumberRepresentation() const;
+            template std::shared_ptr<Polytope<storm::RationalNumber>> Polytope<storm::RationalNumber>::convertNumberRepresentation() const;
 #endif
         }
     }

src/utility/constants.cpp

@@ -109,6 +109,11 @@ namespace storm {
             return number;
         }
         
+        template<typename ValueType>
+        ValueType sqrt(ValueType const& number) {
+            return std::sqrt(number);
+        }
+        
         template<typename ValueType>
         ValueType abs(ValueType const& number) {
             return std::fabs(number);
@@ -142,7 +147,32 @@ namespace storm {
             value.simplify();
             return std::move(value);
         }
+        
+        template<>
+        double convertNumber(RationalNumber const& number){
+            return carl::toDouble(number);
+        }
+        
+        template<>
+        RationalNumber convertNumber(RationalNumber const& number){
+            return number;
+        }
+        
+        template<>
+        RationalNumber convertNumber(double const& number){
+            return carl::rationalize<RationalNumber>(number);
+        }
 
+        template<>
+        RationalFunction convertNumber(double const& number){
+            return RationalFunction(carl::rationalize<RationalNumber>(number));
+        }
+        
+        template<>
+        storm::RationalNumber sqrt(storm::RationalNumber const& number) {
+            return carl::sqrt(number);
+        }
+        
         template<>
         storm::RationalNumber abs(storm::RationalNumber const& number) {
             return carl::abs(number);
@@ -183,6 +213,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);
 
+        template double sqrt(double const& number);
         template double abs(double const& number);
         
         template bool isOne(float const& value);
@@ -249,6 +280,7 @@ namespace storm {
         template double convertNumber(storm::RationalNumber const& number);
         template storm::RationalNumber convertNumber(double const& number);
 
+        template storm::RationalNumber sqrt(storm::RationalNumber const& number);
         template storm::RationalNumber abs(storm::RationalNumber const& number);
 
 //        template storm::RationalNumber pow(storm::RationalNumber const& value, uint_fast64_t exponent);

src/utility/constants.h

@@ -11,9 +11,6 @@
 
 #include <limits>
 #include <cstdint>
-#include <cmath>
-
-#include "src/adapters/CarlAdapter.h"
 
 namespace storm {
     
@@ -55,23 +52,11 @@ namespace storm {
         storm::storage::MatrixEntry<IndexType, ValueType>&& simplify(storm::storage::MatrixEntry<IndexType, ValueType>&& matrixEntry);
         
         template<typename TargetType, typename SourceType>
-        TargetType convertNumber(SourceType const& number) {
-#ifdef STORM_HAVE_CARL
-            return carl::convert<SourceType, TargetType>(number);
-#else
-            return static_cast<TargetType>(number);
-#endif
-        }
-        
-        template<typename ValueType>
-        ValueType sqrt(ValueType const& value) {
-#ifdef STORM_HAVE_CARL
-            return carl::sqrt(value);
-#else
-            return std::sqrt(value);
-#endif
-        }
+        TargetType convertNumber(SourceType const& number);
 
+        template<typename ValueType>
+        ValueType sqrt(ValueType const& number);
+        
         template<typename ValueType>
         ValueType abs(ValueType const& number);
     }

src/utility/storm.h

@@ -318,51 +318,47 @@ namespace storm {
     }
 
     template<typename ValueType>
-    std::unique_ptr<storm::modelchecker::CheckResult> verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::shared_ptr<storm::logic::Formula const> const& formula, bool onlyInitialStatesRelevant = false) {
-        storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant);
-
+    std::unique_ptr<storm::modelchecker::CheckResult> verifySparseMarkovAutomaton(std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma, storm::modelchecker::CheckTask<storm::logic::Formula> const& task) {
         std::unique_ptr<storm::modelchecker::CheckResult> result;
-        if (model->getType() == storm::models::ModelType::Dtmc) {
-            result = verifySparseDtmc(model->template as<storm::models::sparse::Dtmc<ValueType>>(), task);
-        } else if (model->getType() == storm::models::ModelType::Mdp) {
-            result = verifySparseMdp(model->template as<storm::models::sparse::Mdp<ValueType>>(), task);
-        } else if (model->getType() == storm::models::ModelType::Ctmc) {
-            result = verifySparseCtmc(model->template as<storm::models::sparse::Ctmc<ValueType>>(), task);
-        } else if (model->getType() == storm::models::ModelType::MarkovAutomaton) {
-            std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = model->template as<storm::models::sparse::MarkovAutomaton<ValueType>>();
+        if(task.getFormula().isMultiObjectiveFormula()) {
             // Close the MA, if it is not already closed.
             if (!ma->isClosed()) {
                 ma->close();
             }
-            if(task.getFormula().isMultiObjectiveFormula()) {
-                 storm::modelchecker::SparseMaMultiObjectiveModelChecker<storm::models::sparse::MarkovAutomaton<ValueType>> modelchecker(*ma);
-                if(modelchecker.canHandle(task)) {
-                    result = modelchecker.check(task);
-                } else {
-                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type " << model->getType() << " is not supported.");
-                }
+            storm::modelchecker::SparseMaMultiObjectiveModelChecker<storm::models::sparse::MarkovAutomaton<ValueType>> modelchecker(*ma);
+            if (modelchecker.canHandle(task)) {
+                result = modelchecker.check(task);
             } else {
-
-
-                  storm::modelchecker::SparseMaMultiObjectiveModelChecker<storm::models::sparse::MarkovAutomaton<ValueType>> modelchecker2(*ma);
-                if(modelchecker2.canHandle(task)){
-                    result = modelchecker2.check(task);
-                }
+                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The property " << task.getFormula() << " is not supported.");
             }
+        } else {
             storm::modelchecker::SparseMarkovAutomatonCslModelChecker<storm::models::sparse::MarkovAutomaton<ValueType>> modelchecker(*ma);
-            if(modelchecker.canHandle(task)) {
+            if (modelchecker.canHandle(task)) {
                 result = modelchecker.check(task);
             } else {
-                storm::modelchecker::SparseMaMultiObjectiveModelChecker<storm::models::sparse::MarkovAutomaton<ValueType>> modelchecker2(*ma);
-                if(modelchecker2.canHandle(task)){
-                    result = modelchecker2.check(task);
-                }
+                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The property " << task.getFormula() << " is not supported.");
             }
+        }
+        return result;
+    }
+
+    template<typename ValueType>
+    std::unique_ptr<storm::modelchecker::CheckResult> verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::shared_ptr<storm::logic::Formula const> const& formula, bool onlyInitialStatesRelevant = false) {
+        storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant);
+
+        std::unique_ptr<storm::modelchecker::CheckResult> result;
+        if (model->getType() == storm::models::ModelType::Dtmc) {
+            result = verifySparseDtmc(model->template as<storm::models::sparse::Dtmc<ValueType>>(), task);
+        } else if (model->getType() == storm::models::ModelType::Mdp) {
+            result = verifySparseMdp(model->template as<storm::models::sparse::Mdp<ValueType>>(), task);
+        } else if (model->getType() == storm::models::ModelType::Ctmc) {
+            result = verifySparseCtmc(model->template as<storm::models::sparse::Ctmc<ValueType>>(), task);
+        } else if (model->getType() == storm::models::ModelType::MarkovAutomaton) {
+            result = verifySparseMarkovAutomaton(model->template as<storm::models::sparse::MarkovAutomaton<ValueType>>(), task);
         } else {
             STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type " << model->getType() << " is not supported.");
         }
         return result;
-
     }
     
     template<>

test/functional/modelchecker/SparseMdpMultiObjectiveModelCheckerTest.cpp

@@ -23,8 +23,8 @@ TEST(SparseMdpMultiObjectiveModelCheckerTest, probEqual1Objective) {
     storm::prism::Program program = storm::parseProgram(programFile);
     program.checkValidity();
     std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulasAsString, program);
-    typename storm::builder::ExplicitPrismModelBuilder<double>::Options options = storm::builder::ExplicitPrismModelBuilder<double>::Options(formulas);
-    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitPrismModelBuilder<double>(program, options).translate()->as<storm::models::sparse::Mdp<double>>();
+    storm::generator::NextStateGeneratorOptions options(formulas);
+    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitModelBuilder<double>(program, options).build()->as<storm::models::sparse::Mdp<double>>();
     uint_fast64_t const initState = *mdp->getInitialStates().begin();
     
     storm::modelchecker::SparseMdpMultiObjectiveModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
@@ -49,8 +49,8 @@ TEST(SparseMdpMultiObjectiveModelCheckerTest, probEqual0Objective) {
     storm::prism::Program program = storm::parseProgram(programFile);
     program.checkValidity();
     std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulasAsString, program);
-    typename storm::builder::ExplicitPrismModelBuilder<double>::Options options = storm::builder::ExplicitPrismModelBuilder<double>::Options(formulas);
-    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitPrismModelBuilder<double>(program, options).translate()->as<storm::models::sparse::Mdp<double>>();
+    storm::generator::NextStateGeneratorOptions options(formulas);
+    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitModelBuilder<double>(program, options).build()->as<storm::models::sparse::Mdp<double>>();
     uint_fast64_t const initState = *mdp->getInitialStates().begin();
     
     storm::modelchecker::SparseMdpMultiObjectiveModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
@@ -85,8 +85,8 @@ TEST(SparseMdpMultiObjectiveModelCheckerTest, preprocessorResultsTest) {
     storm::prism::Program program = storm::parseProgram(programFile);
     program.checkValidity();
     std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulasAsString, program);
-    typename storm::builder::ExplicitPrismModelBuilder<double>::Options options = storm::builder::ExplicitPrismModelBuilder<double>::Options(formulas);
-    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitPrismModelBuilder<double>(program, options).translate()->as<storm::models::sparse::Mdp<double>>();
+    storm::generator::NextStateGeneratorOptions options(formulas);
+    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitModelBuilder<double>(program, options).build()->as<storm::models::sparse::Mdp<double>>();
     uint_fast64_t const initState = *mdp->getInitialStates().begin();
     
     storm::modelchecker::SparseMdpMultiObjectiveModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
@@ -151,8 +151,8 @@ TEST(SparseMdpMultiObjectiveModelCheckerTest, consensus) {
     storm::prism::Program program = storm::parseProgram(programFile);
     program.checkValidity();
     std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulasAsString, program);
-    typename storm::builder::ExplicitPrismModelBuilder<double>::Options options = storm::builder::ExplicitPrismModelBuilder<double>::Options(formulas);
-    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitPrismModelBuilder<double>(program, options).translate()->as<storm::models::sparse::Mdp<double>>();
+    storm::generator::NextStateGeneratorOptions options(formulas);
+    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitModelBuilder<double>(program, options).build()->as<storm::models::sparse::Mdp<double>>();
     uint_fast64_t const initState = *mdp->getInitialStates().begin();
     
     storm::modelchecker::SparseMdpMultiObjectiveModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
@@ -182,8 +182,8 @@ TEST(SparseMdpMultiObjectiveModelCheckerTest, zeroconf) {
     storm::prism::Program program = storm::parseProgram(programFile);
     program.checkValidity();
     std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulasAsString, program);
-    typename storm::builder::ExplicitPrismModelBuilder<double>::Options options = storm::builder::ExplicitPrismModelBuilder<double>::Options(formulas);
-    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitPrismModelBuilder<double>(program, options).translate()->as<storm::models::sparse::Mdp<double>>();
+    storm::generator::NextStateGeneratorOptions options(formulas);
+    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitModelBuilder<double>(program, options).build()->as<storm::models::sparse::Mdp<double>>();
     uint_fast64_t const initState = *mdp->getInitialStates().begin();
     
     storm::modelchecker::SparseMdpMultiObjectiveModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
@@ -213,8 +213,8 @@ TEST(SparseMdpMultiObjectiveModelCheckerTest, zeroconfTb) {
     storm::prism::Program program = storm::parseProgram(programFile);
     program.checkValidity();
     std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulasAsString, program);
-    typename storm::builder::ExplicitPrismModelBuilder<double>::Options options = storm::builder::ExplicitPrismModelBuilder<double>::Options(formulas);
-    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitPrismModelBuilder<double>(program, options).translate()->as<storm::models::sparse::Mdp<double>>();
+    storm::generator::NextStateGeneratorOptions options(formulas);
+    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitModelBuilder<double>(program, options).build()->as<storm::models::sparse::Mdp<double>>();
     uint_fast64_t const initState = *mdp->getInitialStates().begin();
     
     storm::modelchecker::SparseMdpMultiObjectiveModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
@@ -244,8 +244,8 @@ TEST(SparseMdpMultiObjectiveModelCheckerTest, team3with2objectives) {
     storm::prism::Program program = storm::parseProgram(programFile);
     program.checkValidity();
     std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulasAsString, program);
-    typename storm::builder::ExplicitPrismModelBuilder<double>::Options options = storm::builder::ExplicitPrismModelBuilder<double>::Options(formulas);
-    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitPrismModelBuilder<double>(program, options).translate()->as<storm::models::sparse::Mdp<double>>();
+    storm::generator::NextStateGeneratorOptions options(formulas);
+    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitModelBuilder<double>(program, options).build()->as<storm::models::sparse::Mdp<double>>();
     uint_fast64_t const initState = *mdp->getInitialStates().begin();
     
     storm::modelchecker::SparseMdpMultiObjectiveModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
@@ -275,8 +275,8 @@ TEST(SparseMdpMultiObjectiveModelCheckerTest, team3with3objectives) {
     storm::prism::Program program = storm::parseProgram(programFile);
     program.checkValidity();
     std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulasAsString, program);
-    typename storm::builder::ExplicitPrismModelBuilder<double>::Options options = storm::builder::ExplicitPrismModelBuilder<double>::Options(formulas);
-    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitPrismModelBuilder<double>(program, options).translate()->as<storm::models::sparse::Mdp<double>>();
+    storm::generator::NextStateGeneratorOptions options(formulas);
+    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitModelBuilder<double>(program, options).build()->as<storm::models::sparse::Mdp<double>>();
     uint_fast64_t const initState = *mdp->getInitialStates().begin();
     
     storm::modelchecker::SparseMdpMultiObjectiveModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
@@ -306,8 +306,8 @@ TEST(SparseMdpMultiObjectiveModelCheckerTest, scheduler) {
     storm::prism::Program program = storm::parseProgram(programFile);
     program.checkValidity();
     std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulasAsString, program);
-    typename storm::builder::ExplicitPrismModelBuilder<double>::Options options = storm::builder::ExplicitPrismModelBuilder<double>::Options(formulas);
-    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitPrismModelBuilder<double>(program, options).translate()->as<storm::models::sparse::Mdp<double>>();
+    storm::generator::NextStateGeneratorOptions options(formulas);
+    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitModelBuilder<double>(program, options).build()->as<storm::models::sparse::Mdp<double>>();
     uint_fast64_t const initState = *mdp->getInitialStates().begin();
     
     storm::modelchecker::SparseMdpMultiObjectiveModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
@@ -337,8 +337,8 @@ TEST(SparseMdpMultiObjectiveModelCheckerTest, dpm) {
     storm::prism::Program program = storm::parseProgram(programFile);
     program.checkValidity();
     std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulasAsString, program);
-    typename storm::builder::ExplicitPrismModelBuilder<double>::Options options = storm::builder::ExplicitPrismModelBuilder<double>::Options(formulas);
-    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitPrismModelBuilder<double>(program, options).translate()->as<storm::models::sparse::Mdp<double>>();
+    storm::generator::NextStateGeneratorOptions options(formulas);
+    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitModelBuilder<double>(program, options).build()->as<storm::models::sparse::Mdp<double>>();
     uint_fast64_t const initState = *mdp->getInitialStates().begin();
     
     storm::modelchecker::SparseMdpMultiObjectiveModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);