From 4496b5300248ffd3b65ec1915df8c483f80f2c4b Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 28 Jun 2016 15:29:59 +0200 Subject: [PATCH] merge fixes Former-commit-id: ff5de6fc69a577202fae1e2198e4333258207f03 --- .../SparseMdpMultiObjectiveModelChecker.cpp | 4 +- .../helper/SparseMultiObjectiveHelper.cpp | 5 +- .../SparseMultiObjectivePostprocessor.cpp | 3 + .../SparseMultiObjectivePreprocessor.cpp | 5 ++ ...parseMultiObjectiveWeightVectorChecker.cpp | 26 ++++++--- .../StandardMinMaxLinearEquationSolver.cpp | 13 ++++- src/storage/geometry/Polytope.cpp | 2 + src/utility/constants.cpp | 32 +++++++++++ src/utility/constants.h | 23 ++------ src/utility/storm.h | 56 +++++++++---------- ...parseMdpMultiObjectiveModelCheckerTest.cpp | 40 ++++++------- 11 files changed, 128 insertions(+), 81 deletions(-) diff --git a/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp b/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp index 661d3a0c3..c191f0b63 100644 --- a/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp +++ b/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp @@ -59,8 +59,10 @@ namespace storm { return result; } - template class SparseMdpMultiObjectiveModelChecker>; +#ifdef STORM_HAVE_CARL + template class SparseMdpMultiObjectiveModelChecker>; +#endif } } diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp index 59a8327d0..0f3606c2b 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp @@ -230,7 +230,7 @@ namespace storm { template void SparseMultiObjectiveHelper::performRefinementStep(WeightVector const& direction, bool saveScheduler, SparseMultiObjectiveWeightVectorChecker& weightVectorChecker, ResultData& result) { weightVectorChecker.check(storm::utility::vector::convertNumericVector(direction)); - STORM_LOG_DEBUG("weighted objectives checker result is " << weightVectorChecker.getInitialStateResultOfObjectives()); + STORM_LOG_DEBUG("weighted objectives checker result is " << storm::utility::vector::convertNumericVector(weightVectorChecker.getInitialStateResultOfObjectives())); if(saveScheduler) { result.refinementSteps().emplace_back(direction, weightVectorChecker.template getInitialStateResultOfObjectives(), weightVectorChecker.getScheduler()); } else { @@ -308,6 +308,9 @@ namespace storm { #ifdef STORM_HAVE_CARL template class SparseMultiObjectiveHelper, storm::RationalNumber>; template class SparseMultiObjectiveHelper, storm::RationalNumber>; + + template class SparseMultiObjectiveHelper, storm::RationalNumber>; + template class SparseMultiObjectiveHelper, storm::RationalNumber>; #endif } } diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp index 3c67a63b7..aebbef595 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp @@ -325,6 +325,9 @@ namespace storm { #ifdef STORM_HAVE_CARL template class SparseMultiObjectivePostprocessor, storm::RationalNumber>; template class SparseMultiObjectivePostprocessor, storm::RationalNumber>; + + template class SparseMultiObjectivePostprocessor, storm::RationalNumber>; + template class SparseMultiObjectivePostprocessor, storm::RationalNumber>; #endif } diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp index 978af4461..4ccca84cb 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp @@ -444,6 +444,11 @@ namespace storm { template class SparseMultiObjectivePreprocessor>; template class SparseMultiObjectivePreprocessor>; + +#ifdef STORM_HAVE_CARL + template class SparseMultiObjectivePreprocessor>; + template class SparseMultiObjectivePreprocessor>; +#endif } diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp index 785ba8c0c..e5d343bd1 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp +++ b/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 void SparseMultiObjectiveWeightVectorChecker::check(std::vector 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(weightVector)); storm::storage::BitVector unboundedObjectives(data.objectives.size(), false); std::vector weightedRewardVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero()); 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()); 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() << " ...WeightVectorChecker done."); } template @@ -83,13 +82,15 @@ namespace storm { std::vector subResult(removerResult.matrix.getRowGroupCount()); - storm::utility::solver::MinMaxLinearEquationSolverFactory solverFactory; - std::unique_ptr> solver = solverFactory.create(removerResult.matrix, true); + storm::solver::GeneralMinMaxLinearEquationSolverFactory solverFactory; + std::unique_ptr> 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(data.preprocessedModel.getNumberOfStates()); this->scheduler = storm::storage::TotalScheduler(data.preprocessedModel.getNumberOfStates()); + std::unique_ptr 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 deterministicMatrix = data.preprocessedModel.getTransitionMatrix().selectRowsFromRowGroups(this->scheduler.getChoices(), true); storm::storage::SparseMatrix deterministicBackwardTransitions = deterministicMatrix.transpose(); std::vector deterministicStateRewards(deterministicMatrix.getRowCount()); - storm::utility::solver::LinearEquationSolverFactory linearEquationSolverFactory; + storm::solver::GeneralLinearEquationSolverFactory 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 SparseMultiObjectiveWeightVectorChecker>::getInitialStateResultOfObjectives() const; template std::vector SparseMultiObjectiveWeightVectorChecker>::getInitialStateResultOfObjectives() const; + + template class SparseMultiObjectiveWeightVectorChecker>; + template std::vector SparseMultiObjectiveWeightVectorChecker>::getInitialStateResultOfObjectives() const; + template class SparseMultiObjectiveWeightVectorChecker>; + template std::vector SparseMultiObjectiveWeightVectorChecker>::getInitialStateResultOfObjectives() const; + template std::vector SparseMultiObjectiveWeightVectorChecker>::getInitialStateResultOfObjectives() const; + template std::vector SparseMultiObjectiveWeightVectorChecker>::getInitialStateResultOfObjectives() const; #endif } diff --git a/src/solver/StandardMinMaxLinearEquationSolver.cpp b/src/solver/StandardMinMaxLinearEquationSolver.cpp index db507ef68..e32814f8d 100644 --- a/src/solver/StandardMinMaxLinearEquationSolver.cpp +++ b/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 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(std::move(choices)); + } + // Dispose of allocated scratch memory. if (!xMemoryProvided) { delete copyX; @@ -396,4 +407,4 @@ namespace storm { template class EliminationMinMaxLinearEquationSolverFactory; } -} \ No newline at end of file +} diff --git a/src/storage/geometry/Polytope.cpp b/src/storage/geometry/Polytope.cpp index dd65de8e0..8b75cfb72 100644 --- a/src/storage/geometry/Polytope.cpp +++ b/src/storage/geometry/Polytope.cpp @@ -265,11 +265,13 @@ namespace storm { } template class Polytope; + template std::shared_ptr> Polytope::convertNumberRepresentation() const; #ifdef STORM_HAVE_CARL template class Polytope; template std::shared_ptr> Polytope::convertNumberRepresentation() const; template std::shared_ptr> Polytope::convertNumberRepresentation() const; + template std::shared_ptr> Polytope::convertNumberRepresentation() const; #endif } } diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp index 33a799313..b2cef709d 100644 --- a/src/utility/constants.cpp +++ b/src/utility/constants.cpp @@ -109,6 +109,11 @@ namespace storm { return number; } + template + ValueType sqrt(ValueType const& number) { + return std::sqrt(number); + } + template 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(number); + } + template<> + RationalFunction convertNumber(double const& number){ + return RationalFunction(carl::rationalize(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& simplify(storm::storage::MatrixEntry& matrixEntry); template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& 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); diff --git a/src/utility/constants.h b/src/utility/constants.h index 8d3ff087f..9c9f4a329 100644 --- a/src/utility/constants.h +++ b/src/utility/constants.h @@ -11,9 +11,6 @@ #include #include -#include - -#include "src/adapters/CarlAdapter.h" namespace storm { @@ -55,23 +52,11 @@ namespace storm { storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); template - TargetType convertNumber(SourceType const& number) { -#ifdef STORM_HAVE_CARL - return carl::convert(number); -#else - return static_cast(number); -#endif - } - - template - 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 + ValueType sqrt(ValueType const& number); + template ValueType abs(ValueType const& number); } diff --git a/src/utility/storm.h b/src/utility/storm.h index 2cc5ac27c..a341f5b32 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -318,51 +318,47 @@ namespace storm { } template - std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant = false) { - storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); - + std::unique_ptr verifySparseMarkovAutomaton(std::shared_ptr> ma, storm::modelchecker::CheckTask const& task) { std::unique_ptr result; - if (model->getType() == storm::models::ModelType::Dtmc) { - result = verifySparseDtmc(model->template as>(), task); - } else if (model->getType() == storm::models::ModelType::Mdp) { - result = verifySparseMdp(model->template as>(), task); - } else if (model->getType() == storm::models::ModelType::Ctmc) { - result = verifySparseCtmc(model->template as>(), task); - } else if (model->getType() == storm::models::ModelType::MarkovAutomaton) { - std::shared_ptr> ma = model->template as>(); + 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> 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> modelchecker(*ma); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); } else { - - - storm::modelchecker::SparseMaMultiObjectiveModelChecker> 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> modelchecker(*ma); - if(modelchecker.canHandle(task)) { + if (modelchecker.canHandle(task)) { result = modelchecker.check(task); } else { - storm::modelchecker::SparseMaMultiObjectiveModelChecker> 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 + std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant = false) { + storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); + + std::unique_ptr result; + if (model->getType() == storm::models::ModelType::Dtmc) { + result = verifySparseDtmc(model->template as>(), task); + } else if (model->getType() == storm::models::ModelType::Mdp) { + result = verifySparseMdp(model->template as>(), task); + } else if (model->getType() == storm::models::ModelType::Ctmc) { + result = verifySparseCtmc(model->template as>(), task); + } else if (model->getType() == storm::models::ModelType::MarkovAutomaton) { + result = verifySparseMarkovAutomaton(model->template as>(), task); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type " << model->getType() << " is not supported."); } return result; - } template<> diff --git a/test/functional/modelchecker/SparseMdpMultiObjectiveModelCheckerTest.cpp b/test/functional/modelchecker/SparseMdpMultiObjectiveModelCheckerTest.cpp index 08605d2de..a8fd4aeca 100644 --- a/test/functional/modelchecker/SparseMdpMultiObjectiveModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseMdpMultiObjectiveModelCheckerTest.cpp @@ -23,8 +23,8 @@ TEST(SparseMdpMultiObjectiveModelCheckerTest, probEqual1Objective) { storm::prism::Program program = storm::parseProgram(programFile); program.checkValidity(); std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); - typename storm::builder::ExplicitPrismModelBuilder::Options options = storm::builder::ExplicitPrismModelBuilder::Options(formulas); - std::shared_ptr> mdp = storm::builder::ExplicitPrismModelBuilder(program, options).translate()->as>(); + storm::generator::NextStateGeneratorOptions options(formulas); + std::shared_ptr> mdp = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); storm::modelchecker::SparseMdpMultiObjectiveModelChecker> checker(*mdp); @@ -49,8 +49,8 @@ TEST(SparseMdpMultiObjectiveModelCheckerTest, probEqual0Objective) { storm::prism::Program program = storm::parseProgram(programFile); program.checkValidity(); std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); - typename storm::builder::ExplicitPrismModelBuilder::Options options = storm::builder::ExplicitPrismModelBuilder::Options(formulas); - std::shared_ptr> mdp = storm::builder::ExplicitPrismModelBuilder(program, options).translate()->as>(); + storm::generator::NextStateGeneratorOptions options(formulas); + std::shared_ptr> mdp = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); storm::modelchecker::SparseMdpMultiObjectiveModelChecker> checker(*mdp); @@ -85,8 +85,8 @@ TEST(SparseMdpMultiObjectiveModelCheckerTest, preprocessorResultsTest) { storm::prism::Program program = storm::parseProgram(programFile); program.checkValidity(); std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); - typename storm::builder::ExplicitPrismModelBuilder::Options options = storm::builder::ExplicitPrismModelBuilder::Options(formulas); - std::shared_ptr> mdp = storm::builder::ExplicitPrismModelBuilder(program, options).translate()->as>(); + storm::generator::NextStateGeneratorOptions options(formulas); + std::shared_ptr> mdp = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); storm::modelchecker::SparseMdpMultiObjectiveModelChecker> checker(*mdp); @@ -151,8 +151,8 @@ TEST(SparseMdpMultiObjectiveModelCheckerTest, consensus) { storm::prism::Program program = storm::parseProgram(programFile); program.checkValidity(); std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); - typename storm::builder::ExplicitPrismModelBuilder::Options options = storm::builder::ExplicitPrismModelBuilder::Options(formulas); - std::shared_ptr> mdp = storm::builder::ExplicitPrismModelBuilder(program, options).translate()->as>(); + storm::generator::NextStateGeneratorOptions options(formulas); + std::shared_ptr> mdp = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); storm::modelchecker::SparseMdpMultiObjectiveModelChecker> checker(*mdp); @@ -182,8 +182,8 @@ TEST(SparseMdpMultiObjectiveModelCheckerTest, zeroconf) { storm::prism::Program program = storm::parseProgram(programFile); program.checkValidity(); std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); - typename storm::builder::ExplicitPrismModelBuilder::Options options = storm::builder::ExplicitPrismModelBuilder::Options(formulas); - std::shared_ptr> mdp = storm::builder::ExplicitPrismModelBuilder(program, options).translate()->as>(); + storm::generator::NextStateGeneratorOptions options(formulas); + std::shared_ptr> mdp = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); storm::modelchecker::SparseMdpMultiObjectiveModelChecker> checker(*mdp); @@ -213,8 +213,8 @@ TEST(SparseMdpMultiObjectiveModelCheckerTest, zeroconfTb) { storm::prism::Program program = storm::parseProgram(programFile); program.checkValidity(); std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); - typename storm::builder::ExplicitPrismModelBuilder::Options options = storm::builder::ExplicitPrismModelBuilder::Options(formulas); - std::shared_ptr> mdp = storm::builder::ExplicitPrismModelBuilder(program, options).translate()->as>(); + storm::generator::NextStateGeneratorOptions options(formulas); + std::shared_ptr> mdp = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); storm::modelchecker::SparseMdpMultiObjectiveModelChecker> checker(*mdp); @@ -244,8 +244,8 @@ TEST(SparseMdpMultiObjectiveModelCheckerTest, team3with2objectives) { storm::prism::Program program = storm::parseProgram(programFile); program.checkValidity(); std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); - typename storm::builder::ExplicitPrismModelBuilder::Options options = storm::builder::ExplicitPrismModelBuilder::Options(formulas); - std::shared_ptr> mdp = storm::builder::ExplicitPrismModelBuilder(program, options).translate()->as>(); + storm::generator::NextStateGeneratorOptions options(formulas); + std::shared_ptr> mdp = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); storm::modelchecker::SparseMdpMultiObjectiveModelChecker> checker(*mdp); @@ -275,8 +275,8 @@ TEST(SparseMdpMultiObjectiveModelCheckerTest, team3with3objectives) { storm::prism::Program program = storm::parseProgram(programFile); program.checkValidity(); std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); - typename storm::builder::ExplicitPrismModelBuilder::Options options = storm::builder::ExplicitPrismModelBuilder::Options(formulas); - std::shared_ptr> mdp = storm::builder::ExplicitPrismModelBuilder(program, options).translate()->as>(); + storm::generator::NextStateGeneratorOptions options(formulas); + std::shared_ptr> mdp = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); storm::modelchecker::SparseMdpMultiObjectiveModelChecker> checker(*mdp); @@ -306,8 +306,8 @@ TEST(SparseMdpMultiObjectiveModelCheckerTest, scheduler) { storm::prism::Program program = storm::parseProgram(programFile); program.checkValidity(); std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); - typename storm::builder::ExplicitPrismModelBuilder::Options options = storm::builder::ExplicitPrismModelBuilder::Options(formulas); - std::shared_ptr> mdp = storm::builder::ExplicitPrismModelBuilder(program, options).translate()->as>(); + storm::generator::NextStateGeneratorOptions options(formulas); + std::shared_ptr> mdp = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); storm::modelchecker::SparseMdpMultiObjectiveModelChecker> checker(*mdp); @@ -337,8 +337,8 @@ TEST(SparseMdpMultiObjectiveModelCheckerTest, dpm) { storm::prism::Program program = storm::parseProgram(programFile); program.checkValidity(); std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); - typename storm::builder::ExplicitPrismModelBuilder::Options options = storm::builder::ExplicitPrismModelBuilder::Options(formulas); - std::shared_ptr> mdp = storm::builder::ExplicitPrismModelBuilder(program, options).translate()->as>(); + storm::generator::NextStateGeneratorOptions options(formulas); + std::shared_ptr> mdp = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); storm::modelchecker::SparseMdpMultiObjectiveModelChecker> checker(*mdp);