From a896c0df286234b21a6b8c6a34edb8fb7670b758 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 10 Apr 2017 15:08:27 +0200 Subject: [PATCH] improved exact computations --- .../modelchecker/parametric/RegionChecker.cpp | 40 +++++++++---------- .../modelchecker/parametric/RegionChecker.h | 4 +- ...SparseDtmcParameterLiftingModelChecker.cpp | 13 +++--- .../parametric/SparseDtmcRegionChecker.cpp | 30 ++++++-------- .../parametric/SparseDtmcRegionChecker.h | 4 +- .../SparseMdpParameterLiftingModelChecker.cpp | 15 +++++-- .../parametric/SparseMdpRegionChecker.cpp | 30 +++++++------- .../parametric/SparseMdpRegionChecker.h | 4 +- src/storm/solver/StandardGameSolver.cpp | 2 - src/storm/utility/storm.h | 4 +- .../SparseDtmcParameterLiftingTest.cpp | 28 ++++++------- .../SparseMdpParameterLiftingTest.cpp | 24 +++++------ 12 files changed, 99 insertions(+), 99 deletions(-) diff --git a/src/storm/modelchecker/parametric/RegionChecker.cpp b/src/storm/modelchecker/parametric/RegionChecker.cpp index 7a37266be..ca270537b 100644 --- a/src/storm/modelchecker/parametric/RegionChecker.cpp +++ b/src/storm/modelchecker/parametric/RegionChecker.cpp @@ -29,25 +29,25 @@ namespace storm { this->applyExactValidation = storm::settings::getModule().isExactValidationSet(); } - template - RegionChecker::RegionChecker(SparseModelType const& parametricModel) : parametricModel(parametricModel) { + template + RegionChecker::RegionChecker(SparseModelType const& parametricModel) : parametricModel(parametricModel) { initializationStopwatch.start(); STORM_LOG_THROW(parametricModel.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "Parameter lifting requires models with only one initial state"); initializationStopwatch.stop(); } - template - RegionCheckerSettings const& RegionChecker::getSettings() const { + template + RegionCheckerSettings const& RegionChecker::getSettings() const { return settings; } - template - void RegionChecker::setSettings(RegionCheckerSettings const& newSettings) { + template + void RegionChecker::setSettings(RegionCheckerSettings const& newSettings) { settings = newSettings; } - template - void RegionChecker::specifyFormula(CheckTask const& checkTask) { + template + void RegionChecker::specifyFormula(CheckTask const& checkTask) { initializationStopwatch.start(); STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::NotSupportedException, "Parameter lifting requires a property where only the value in the initial states is relevant."); STORM_LOG_THROW(checkTask.isBoundSet(), storm::exceptions::NotSupportedException, "Parameter lifting requires a bounded property."); @@ -67,8 +67,8 @@ namespace storm { initializationStopwatch.stop(); } - template - RegionCheckResult RegionChecker::analyzeRegion(storm::storage::ParameterRegion const& region, RegionCheckResult const& initialResult, bool sampleVerticesOfRegion) { + template + RegionCheckResult RegionChecker::analyzeRegion(storm::storage::ParameterRegion const& region, RegionCheckResult const& initialResult, bool sampleVerticesOfRegion) { RegionCheckResult result = initialResult; // Check if we need to check the formula on one point to decide whether to show AllSat or AllViolated @@ -119,8 +119,8 @@ namespace storm { return result; } - template - RegionCheckResult RegionChecker::analyzeRegionExactValidation(storm::storage::ParameterRegion const& region, RegionCheckResult const& initialResult) { + template + RegionCheckResult RegionChecker::analyzeRegionExactValidation(storm::storage::ParameterRegion const& region, RegionCheckResult const& initialResult) { RegionCheckResult numericResult = analyzeRegion(region, initialResult, false); parameterLiftingCheckerStopwatch.start(); if (numericResult == RegionCheckResult::AllSat || numericResult == RegionCheckResult::AllViolated) { @@ -156,8 +156,8 @@ namespace storm { } - template - std::vector, RegionCheckResult>> RegionChecker::performRegionRefinement(storm::storage::ParameterRegion const& region, CoefficientType const& threshold) { + template + std::vector, RegionCheckResult>> RegionChecker::performRegionRefinement(storm::storage::ParameterRegion const& region, CoefficientType const& threshold) { STORM_LOG_INFO("Applying refinement on region: " << region.toString(true) << " ."); auto areaOfParameterSpace = region.area(); @@ -242,8 +242,8 @@ namespace storm { return result; } - template - SparseModelType const& RegionChecker::getConsideredParametricModel() const { + template + SparseModelType const& RegionChecker::getConsideredParametricModel() const { if (simplifiedModel) { return *simplifiedModel; } else { @@ -251,8 +251,8 @@ namespace storm { } } - template - std::string RegionChecker::visualizeResult(std::vector, RegionCheckResult>> const& result, storm::storage::ParameterRegion const& parameterSpace, typename storm::storage::ParameterRegion::VariableType const& x, typename storm::storage::ParameterRegion::VariableType const& y) { + template + std::string RegionChecker::visualizeResult(std::vector, RegionCheckResult>> const& result, storm::storage::ParameterRegion const& parameterSpace, typename storm::storage::ParameterRegion::VariableType const& x, typename storm::storage::ParameterRegion::VariableType const& y) { std::stringstream stream; @@ -306,8 +306,8 @@ namespace storm { } #ifdef STORM_HAVE_CARL - template class RegionChecker, double>; - template class RegionChecker, double>; + template class RegionChecker, double, storm::RationalNumber>; + template class RegionChecker, double, storm::RationalNumber>; template class RegionChecker, storm::RationalNumber>; template class RegionChecker, storm::RationalNumber>; #endif diff --git a/src/storm/modelchecker/parametric/RegionChecker.h b/src/storm/modelchecker/parametric/RegionChecker.h index f057106e8..680ab361c 100644 --- a/src/storm/modelchecker/parametric/RegionChecker.h +++ b/src/storm/modelchecker/parametric/RegionChecker.h @@ -8,6 +8,7 @@ #include "storm/modelchecker/CheckTask.h" #include "storm/storage/ParameterRegion.h" #include "storm/utility/Stopwatch.h" +#include "storm/utility/NumberTraits.h" namespace storm { namespace modelchecker{ @@ -19,8 +20,9 @@ namespace storm { bool applyExactValidation; }; - template + template class RegionChecker { + static_assert(storm::NumberTraits::IsExact, "Specified type for exact computations is not exact."); public: diff --git a/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp index 28a1547b7..87b4a02a4 100644 --- a/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp +++ b/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp @@ -9,6 +9,7 @@ #include "storm/solver/StandardMinMaxLinearEquationSolver.h" #include "storm/utility/vector.h" #include "storm/utility/graph.h" +#include "storm/utility/NumberTraits.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/InvalidPropertyException.h" @@ -175,18 +176,18 @@ namespace storm { // Set up the solver auto solver = solverFactory->create(parameterLifter->getMatrix()); - solver->setTrackScheduler(true); - if (std::is_same::value && dynamic_cast*>(solver.get())) { + if (storm::NumberTraits::IsExact && dynamic_cast*>(solver.get())) { STORM_LOG_INFO("Parameter Lifting: Setting solution method for exact MinMaxSolver to policy iteration"); auto* standardSolver = dynamic_cast*>(solver.get()); auto settings = standardSolver->getSettings(); settings.setSolutionMethod(storm::solver::StandardMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration); standardSolver->setSettings(settings); } - if(lowerResultBound) solver->setLowerBound(lowerResultBound.get()); - if(upperResultBound) solver->setUpperBound(upperResultBound.get()); - if(storm::solver::minimize(dirForParameters) && minSched && !stepBound) solver->setSchedulerHint(std::move(minSched.get())); - if(storm::solver::maximize(dirForParameters) && maxSched && !stepBound) solver->setSchedulerHint(std::move(maxSched.get())); + if (lowerResultBound) solver->setLowerBound(lowerResultBound.get()); + if (upperResultBound) solver->setUpperBound(upperResultBound.get()); + if (!stepBound) solver->setTrackScheduler(true); + if (storm::solver::minimize(dirForParameters) && minSched && !stepBound) solver->setSchedulerHint(std::move(minSched.get())); + if (storm::solver::maximize(dirForParameters) && maxSched && !stepBound) solver->setSchedulerHint(std::move(maxSched.get())); if (this->currentCheckTask->isBoundSet() && solver->hasSchedulerHint()) { // If we reach this point, we know that after applying the hint, the x-values can only become larger (if we maximize) or smaller (if we minimize). std::unique_ptr> termCond; diff --git a/src/storm/modelchecker/parametric/SparseDtmcRegionChecker.cpp b/src/storm/modelchecker/parametric/SparseDtmcRegionChecker.cpp index 28c4b7f40..c9a841964 100644 --- a/src/storm/modelchecker/parametric/SparseDtmcRegionChecker.cpp +++ b/src/storm/modelchecker/parametric/SparseDtmcRegionChecker.cpp @@ -7,19 +7,19 @@ #include "storm/transformer/SparseParametricDtmcSimplifier.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/models/sparse/Dtmc.h" -#include "SparseMdpRegionChecker.h" +#include "storm/utility/NumberTraits.h" namespace storm { namespace modelchecker { namespace parametric { - template - SparseDtmcRegionChecker::SparseDtmcRegionChecker(SparseModelType const& parametricModel) : RegionChecker(parametricModel) { + template + SparseDtmcRegionChecker::SparseDtmcRegionChecker(SparseModelType const& parametricModel) : RegionChecker(parametricModel) { // Intentionally left empty } - template - void SparseDtmcRegionChecker::simplifyParametricModel(CheckTask const& checkTask) { + template + void SparseDtmcRegionChecker::simplifyParametricModel(CheckTask const& checkTask) { storm::transformer::SparseParametricDtmcSimplifier simplifier(this->parametricModel); if(simplifier.simplify(checkTask.getFormula())) { this->simplifiedModel = simplifier.getSimplifiedModel(); @@ -30,33 +30,29 @@ namespace storm { } } - template - void SparseDtmcRegionChecker::initializeUnderlyingCheckers() { + template + void SparseDtmcRegionChecker::initializeUnderlyingCheckers() { if (this->settings.applyExactValidation) { - //STORM_LOG_WARN_COND(!(std::is_same::CoefficientType) , "Exact validation is not necessarry if the original computation is already exact"); - STORM_LOG_WARN_COND(!(std::is_same::value) , "Exact validation is not necessarry if the original computation is already exact"); - //this->exactParameterLiftingChecker = std::make_unique::CoefficientType>>(this->getConsideredParametricModel()); // todo: use template argument instead of storm::Rational - this->exactParameterLiftingChecker = std::make_unique>(this->getConsideredParametricModel()); + STORM_LOG_WARN_COND(!storm::NumberTraits::IsExact, "Exact validation is not necessarry if the original computation is already exact"); + this->exactParameterLiftingChecker = std::make_unique>(this->getConsideredParametricModel()); } this->parameterLiftingChecker = std::make_unique>(this->getConsideredParametricModel()); this->instantiationChecker = std::make_unique>(this->getConsideredParametricModel()); this->instantiationChecker->setInstantiationsAreGraphPreserving(true); } - template - void SparseDtmcRegionChecker::applyHintsToExactChecker() { + template + void SparseDtmcRegionChecker::applyHintsToExactChecker() { auto dtmcPLChecker = dynamic_cast*>(this->parameterLiftingChecker.get()); STORM_LOG_ASSERT(dtmcPLChecker, "Underlying Parameter lifting checker has unexpected type"); - auto exactDtmcPLChecker = dynamic_cast*>(this->exactParameterLiftingChecker.get()); - //auto exactDtmcPLChecker = dynamic_cast::CoefficientType>*>(this->exactParameterLiftingChecker.get()); // todo: use template argument instead of storm::Rational + auto exactDtmcPLChecker = dynamic_cast*>(this->exactParameterLiftingChecker.get()); STORM_LOG_ASSERT(exactDtmcPLChecker, "Underlying exact parameter lifting checker has unexpected type"); exactDtmcPLChecker->getCurrentMaxScheduler() = dtmcPLChecker->getCurrentMaxScheduler(); exactDtmcPLChecker->getCurrentMinScheduler() = dtmcPLChecker->getCurrentMinScheduler(); } - #ifdef STORM_HAVE_CARL - template class SparseDtmcRegionChecker, double>; + template class SparseDtmcRegionChecker, double, storm::RationalNumber>; template class SparseDtmcRegionChecker, storm::RationalNumber>; #endif } // namespace parametric diff --git a/src/storm/modelchecker/parametric/SparseDtmcRegionChecker.h b/src/storm/modelchecker/parametric/SparseDtmcRegionChecker.h index 4e0919144..561594d2e 100644 --- a/src/storm/modelchecker/parametric/SparseDtmcRegionChecker.h +++ b/src/storm/modelchecker/parametric/SparseDtmcRegionChecker.h @@ -9,8 +9,8 @@ namespace storm { namespace parametric{ - template - class SparseDtmcRegionChecker : public RegionChecker { + template + class SparseDtmcRegionChecker : public RegionChecker { public: SparseDtmcRegionChecker(SparseModelType const& parametricModel); diff --git a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp index 2808123b4..066a5f1b7 100644 --- a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp +++ b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp @@ -8,6 +8,8 @@ #include "storm/models/sparse/StandardRewardModel.h" #include "storm/utility/vector.h" #include "storm/utility/graph.h" +#include "storm/utility/NumberTraits.h" +#include "storm/solver/StandardGameSolver.h" #include "storm/logic/FragmentSpecification.h" #include "storm/exceptions/InvalidArgumentException.h" @@ -208,9 +210,16 @@ namespace storm { // Set up the solver auto solver = solverFactory->create(player1Matrix, parameterLifter->getMatrix()); - if(lowerResultBound) solver->setLowerBound(lowerResultBound.get()); - if(upperResultBound) solver->setUpperBound(upperResultBound.get()); - if(applyPreviousResultAsHint) { + if (storm::NumberTraits::IsExact && dynamic_cast*>(solver.get())) { + STORM_LOG_INFO("Parameter Lifting: Setting solution method for exact Game Solver to policy iteration"); + auto* standardSolver = dynamic_cast*>(solver.get()); + auto settings = standardSolver->getSettings(); + settings.setSolutionMethod(storm::solver::StandardGameSolverSettings::SolutionMethod::PolicyIteration); + standardSolver->setSettings(settings); + } + if (lowerResultBound) solver->setLowerBound(lowerResultBound.get()); + if (upperResultBound) solver->setUpperBound(upperResultBound.get()); + if (applyPreviousResultAsHint) { solver->setTrackSchedulers(true); x.resize(maybeStates.getNumberOfSetBits(), storm::utility::zero()); if(storm::solver::minimize(dirForParameters) && minSched && player1Sched) solver->setSchedulerHints(std::move(player1Sched.get()), std::move(minSched.get())); diff --git a/src/storm/modelchecker/parametric/SparseMdpRegionChecker.cpp b/src/storm/modelchecker/parametric/SparseMdpRegionChecker.cpp index e35366024..9ee9422ff 100644 --- a/src/storm/modelchecker/parametric/SparseMdpRegionChecker.cpp +++ b/src/storm/modelchecker/parametric/SparseMdpRegionChecker.cpp @@ -7,19 +7,20 @@ #include "storm/transformer/SparseParametricMdpSimplifier.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/models/sparse/Mdp.h" -#include "SparseMdpRegionChecker.h" +#include "storm/utility/NumberTraits.h" + namespace storm { namespace modelchecker { namespace parametric { - template - SparseMdpRegionChecker::SparseMdpRegionChecker(SparseModelType const& parametricModel) : RegionChecker(parametricModel) { + template + SparseMdpRegionChecker::SparseMdpRegionChecker(SparseModelType const& parametricModel) : RegionChecker(parametricModel) { // Intentionally left empty } - template - void SparseMdpRegionChecker::simplifyParametricModel(CheckTask const& checkTask) { + template + void SparseMdpRegionChecker::simplifyParametricModel(CheckTask const& checkTask) { storm::transformer::SparseParametricMdpSimplifier simplifier(this->parametricModel); if(simplifier.simplify(checkTask.getFormula())) { this->simplifiedModel = simplifier.getSimplifiedModel(); @@ -30,25 +31,22 @@ namespace storm { } } - template - void SparseMdpRegionChecker::initializeUnderlyingCheckers() { + template + void SparseMdpRegionChecker::initializeUnderlyingCheckers() { if (this->settings.applyExactValidation) { - //STORM_LOG_WARN_COND(!(std::is_same::CoefficientType>::value), "Exact validation is not necessarry if the original computation is already exact"); // todo: use templated argument instead of storm::RationalNumber - STORM_LOG_WARN_COND(!(std::is_same::value), "Exact validation is not necessarry if the original computation is already exact"); - //this->exactParameterLiftingChecker = std::make_unique::CoefficientType>>(this->getConsideredParametricModel()); // todo: use templated argument instead of storm::RationalNumber - this->exactParameterLiftingChecker = std::make_unique>(this->getConsideredParametricModel()); + STORM_LOG_WARN_COND(!storm::NumberTraits::IsExact, "Exact validation is not necessarry if the original computation is already exact"); + this->exactParameterLiftingChecker = std::make_unique>(this->getConsideredParametricModel()); } this->parameterLiftingChecker = std::make_unique>(this->getConsideredParametricModel()); this->instantiationChecker = std::make_unique>(this->getConsideredParametricModel()); this->instantiationChecker->setInstantiationsAreGraphPreserving(true); } - template - void SparseMdpRegionChecker::applyHintsToExactChecker() { + template + void SparseMdpRegionChecker::applyHintsToExactChecker() { auto MdpPLChecker = dynamic_cast*>(this->parameterLiftingChecker.get()); STORM_LOG_ASSERT(MdpPLChecker, "Underlying Parameter lifting checker has unexpected type"); - auto exactMdpPLChecker = dynamic_cast*>(this->exactParameterLiftingChecker.get()); -// auto exactMdpPLChecker = dynamic_cast::CoefficientType>*>(this->exactParameterLiftingChecker.get()); // todo: use template argument instead of storm::RationalNumber + auto exactMdpPLChecker = dynamic_cast*>(this->exactParameterLiftingChecker.get()); STORM_LOG_ASSERT(exactMdpPLChecker, "Underlying exact parameter lifting checker has unexpected type"); exactMdpPLChecker->getCurrentMaxScheduler() = MdpPLChecker->getCurrentMaxScheduler(); exactMdpPLChecker->getCurrentMinScheduler() = MdpPLChecker->getCurrentMinScheduler(); @@ -57,7 +55,7 @@ namespace storm { #ifdef STORM_HAVE_CARL - template class SparseMdpRegionChecker, double>; + template class SparseMdpRegionChecker, double, storm::RationalNumber>; template class SparseMdpRegionChecker, storm::RationalNumber>; #endif } // namespace parametric diff --git a/src/storm/modelchecker/parametric/SparseMdpRegionChecker.h b/src/storm/modelchecker/parametric/SparseMdpRegionChecker.h index 1776a3866..72c355eee 100644 --- a/src/storm/modelchecker/parametric/SparseMdpRegionChecker.h +++ b/src/storm/modelchecker/parametric/SparseMdpRegionChecker.h @@ -9,8 +9,8 @@ namespace storm { namespace parametric{ - template - class SparseMdpRegionChecker : public RegionChecker { + template + class SparseMdpRegionChecker : public RegionChecker { public: SparseMdpRegionChecker(SparseModelType const& parametricModel); diff --git a/src/storm/solver/StandardGameSolver.cpp b/src/storm/solver/StandardGameSolver.cpp index 16f10587b..49998ab46 100644 --- a/src/storm/solver/StandardGameSolver.cpp +++ b/src/storm/solver/StandardGameSolver.cpp @@ -397,8 +397,6 @@ namespace storm { inducedVector.resize(inducedMatrix.getRowCount()); storm::utility::vector::selectVectorValues(inducedVector, selectedRows, b); } - - template typename StandardGameSolver::Status StandardGameSolver::updateStatusIfNotConverged(Status status, std::vector const& x, uint64_t iterations) const { diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index 6f5d2b5c1..f69351da6 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -360,7 +360,7 @@ namespace storm { resultVisualization = regionChecker.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin())); } } else { - storm::modelchecker::parametric::SparseDtmcRegionChecker , double> regionChecker(*markovModel->template as>()); + storm::modelchecker::parametric::SparseDtmcRegionChecker , double, storm::RationalNumber> regionChecker(*markovModel->template as>()); regionChecker.specifyFormula(task); result = regionChecker.performRegionRefinement(parameterSpace, refinementThreshold); parameterLiftingStopWatch.stop(); @@ -378,7 +378,7 @@ namespace storm { resultVisualization = regionChecker.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin())); } } else { - storm::modelchecker::parametric::SparseMdpRegionChecker, double> regionChecker(*markovModel->template as>()); + storm::modelchecker::parametric::SparseMdpRegionChecker, double, storm::RationalNumber> regionChecker(*markovModel->template as>()); regionChecker.specifyFormula(task); result = regionChecker.performRegionRefinement(parameterSpace, refinementThreshold); parameterLiftingStopWatch.stop(); diff --git a/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp b/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp index ddffd4f06..0314c3e56 100644 --- a/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp +++ b/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp @@ -5,9 +5,7 @@ #include "storm/adapters/CarlAdapter.h" -#include "utility/storm.h" -#include "storm/models/sparse/Model.h" -#include "modelchecker/parametric/SparseDtmcRegionChecker.h" +#include "storm/utility/storm.h" TEST(SparseDtmcParameterLiftingTest, Brp_Prob) { @@ -25,7 +23,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Prob) { auto rewParameters = storm::models::sparse::getRewardParameters(*model); modelParameters.insert(rewParameters.begin(), rewParameters.end()); - storm::modelchecker::parametric::SparseDtmcRegionChecker, double> regionChecker(*model); + storm::modelchecker::parametric::SparseDtmcRegionChecker, double, storm::RationalNumber> regionChecker(*model); regionChecker.specifyFormula(storm::modelchecker::CheckTask(*formulas[0], true)); //start testing @@ -55,7 +53,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew) { auto rewParameters = storm::models::sparse::getRewardParameters(*model); modelParameters.insert(rewParameters.begin(), rewParameters.end()); - storm::modelchecker::parametric::SparseDtmcRegionChecker, double> regionChecker(*model); + storm::modelchecker::parametric::SparseDtmcRegionChecker, double, storm::RationalNumber> regionChecker(*model); regionChecker.specifyFormula(storm::modelchecker::CheckTask(*formulas[0], true)); //start testing @@ -85,7 +83,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded) { auto rewParameters = storm::models::sparse::getRewardParameters(*model); modelParameters.insert(rewParameters.begin(), rewParameters.end()); - storm::modelchecker::parametric::SparseDtmcRegionChecker, double> regionChecker(*model); + storm::modelchecker::parametric::SparseDtmcRegionChecker, double, storm::RationalNumber> regionChecker(*model); regionChecker.specifyFormula(storm::modelchecker::CheckTask(*formulas[0], true)); //start testing @@ -116,7 +114,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Prob_exactValidation) { auto rewParameters = storm::models::sparse::getRewardParameters(*model); modelParameters.insert(rewParameters.begin(), rewParameters.end()); - storm::modelchecker::parametric::SparseDtmcRegionChecker, double> regionChecker(*model); + storm::modelchecker::parametric::SparseDtmcRegionChecker, double, storm::RationalNumber> regionChecker(*model); auto settings = regionChecker.getSettings(); settings.applyExactValidation = true; regionChecker.setSettings(settings); @@ -149,7 +147,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_exactValidation) { auto rewParameters = storm::models::sparse::getRewardParameters(*model); modelParameters.insert(rewParameters.begin(), rewParameters.end()); - storm::modelchecker::parametric::SparseDtmcRegionChecker, double> regionChecker(*model); + storm::modelchecker::parametric::SparseDtmcRegionChecker, double, storm::RationalNumber> regionChecker(*model); auto settings = regionChecker.getSettings(); settings.applyExactValidation = true; regionChecker.setSettings(settings); @@ -182,7 +180,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded_exactValidation) { auto rewParameters = storm::models::sparse::getRewardParameters(*model); modelParameters.insert(rewParameters.begin(), rewParameters.end()); - storm::modelchecker::parametric::SparseDtmcRegionChecker, double> regionChecker(*model); + storm::modelchecker::parametric::SparseDtmcRegionChecker, double, storm::RationalNumber> regionChecker(*model); auto settings = regionChecker.getSettings(); settings.applyExactValidation = true; regionChecker.setSettings(settings); @@ -215,7 +213,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Infty) { auto rewParameters = storm::models::sparse::getRewardParameters(*model); modelParameters.insert(rewParameters.begin(), rewParameters.end()); - storm::modelchecker::parametric::SparseDtmcRegionChecker, double> regionChecker(*model); + storm::modelchecker::parametric::SparseDtmcRegionChecker, double, storm::RationalNumber> regionChecker(*model); regionChecker.specifyFormula(storm::modelchecker::CheckTask(*formulas[0], true)); //start testing @@ -241,7 +239,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_4Par) { auto rewParameters = storm::models::sparse::getRewardParameters(*model); modelParameters.insert(rewParameters.begin(), rewParameters.end()); - storm::modelchecker::parametric::SparseDtmcRegionChecker, double> regionChecker(*model); + storm::modelchecker::parametric::SparseDtmcRegionChecker, double, storm::RationalNumber> regionChecker(*model); regionChecker.specifyFormula(storm::modelchecker::CheckTask(*formulas[0], true)); //start testing @@ -272,7 +270,7 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob) { auto rewParameters = storm::models::sparse::getRewardParameters(*model); modelParameters.insert(rewParameters.begin(), rewParameters.end()); - storm::modelchecker::parametric::SparseDtmcRegionChecker, double> regionChecker(*model); + storm::modelchecker::parametric::SparseDtmcRegionChecker, double, storm::RationalNumber> regionChecker(*model); regionChecker.specifyFormula(storm::modelchecker::CheckTask(*formulas[0], true)); //start testing @@ -305,7 +303,7 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_stepBounded) { auto rewParameters = storm::models::sparse::getRewardParameters(*model); modelParameters.insert(rewParameters.begin(), rewParameters.end()); - storm::modelchecker::parametric::SparseDtmcRegionChecker, double> regionChecker(*model); + storm::modelchecker::parametric::SparseDtmcRegionChecker, double, storm::RationalNumber> regionChecker(*model); regionChecker.specifyFormula(storm::modelchecker::CheckTask(*formulas[0], true)); //start testing @@ -339,7 +337,7 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_1Par) { auto rewParameters = storm::models::sparse::getRewardParameters(*model); modelParameters.insert(rewParameters.begin(), rewParameters.end()); - storm::modelchecker::parametric::SparseDtmcRegionChecker, double> regionChecker(*model); + storm::modelchecker::parametric::SparseDtmcRegionChecker, double, storm::RationalNumber> regionChecker(*model); regionChecker.specifyFormula(storm::modelchecker::CheckTask(*formulas[0], true)); //start testing @@ -370,7 +368,7 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_Const) { auto rewParameters = storm::models::sparse::getRewardParameters(*model); modelParameters.insert(rewParameters.begin(), rewParameters.end()); - storm::modelchecker::parametric::SparseDtmcRegionChecker, double> regionChecker(*model); + storm::modelchecker::parametric::SparseDtmcRegionChecker, double, storm::RationalNumber> regionChecker(*model); regionChecker.specifyFormula(storm::modelchecker::CheckTask(*formulas[0], true)); //start testing diff --git a/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp b/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp index cb15b9aaf..81832d240 100644 --- a/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp +++ b/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp @@ -5,9 +5,7 @@ #include "storm/adapters/CarlAdapter.h" -#include "utility/storm.h" -#include "storm/models/sparse/Model.h" -#include "storm/modelchecker/parametric/SparseMdpRegionChecker.h" +#include "storm/utility/storm.h" TEST(SparseMdpParameterLiftingTest, two_dice_Prob) { @@ -24,7 +22,7 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob) { auto rewParameters = storm::models::sparse::getRewardParameters(*model); modelParameters.insert(rewParameters.begin(), rewParameters.end()); - storm::modelchecker::parametric::SparseMdpRegionChecker, double> regionChecker(*model); + storm::modelchecker::parametric::SparseMdpRegionChecker, double, storm::RationalNumber> regionChecker(*model); regionChecker.specifyFormula(storm::modelchecker::CheckTask(*formulas[0], true)); auto allSatRegion = storm::storage::ParameterRegion::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters); @@ -54,7 +52,7 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob_bounded) { auto rewParameters = storm::models::sparse::getRewardParameters(*model); modelParameters.insert(rewParameters.begin(), rewParameters.end()); - storm::modelchecker::parametric::SparseMdpRegionChecker, double> regionChecker(*model); + storm::modelchecker::parametric::SparseMdpRegionChecker, double, storm::RationalNumber> regionChecker(*model); regionChecker.specifyFormula(storm::modelchecker::CheckTask(*formulas[0], true)); auto allSatRegion = storm::storage::ParameterRegion::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters); @@ -84,7 +82,7 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob_exactValidation) { auto rewParameters = storm::models::sparse::getRewardParameters(*model); modelParameters.insert(rewParameters.begin(), rewParameters.end()); - storm::modelchecker::parametric::SparseMdpRegionChecker, double> regionChecker(*model); + storm::modelchecker::parametric::SparseMdpRegionChecker, double, storm::RationalNumber> regionChecker(*model); regionChecker.specifyFormula(storm::modelchecker::CheckTask(*formulas[0], true)); auto allSatRegion = storm::storage::ParameterRegion::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters); @@ -114,7 +112,7 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob_bounded_exactValidation) { auto rewParameters = storm::models::sparse::getRewardParameters(*model); modelParameters.insert(rewParameters.begin(), rewParameters.end()); - storm::modelchecker::parametric::SparseMdpRegionChecker, double> regionChecker(*model); + storm::modelchecker::parametric::SparseMdpRegionChecker, double, storm::RationalNumber> regionChecker(*model); regionChecker.specifyFormula(storm::modelchecker::CheckTask(*formulas[0], true)); auto allSatRegion = storm::storage::ParameterRegion::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters); @@ -142,7 +140,7 @@ TEST(SparseMdpParameterLiftingTest, coin_Prob) { auto rewParameters = storm::models::sparse::getRewardParameters(*model); modelParameters.insert(rewParameters.begin(), rewParameters.end()); - storm::modelchecker::parametric::SparseMdpRegionChecker, double> regionChecker(*model); + storm::modelchecker::parametric::SparseMdpRegionChecker, double, storm::RationalNumber> regionChecker(*model); regionChecker.specifyFormula(storm::modelchecker::CheckTask(*formulas[0], true)); //start testing @@ -172,7 +170,7 @@ TEST(SparseMdpParameterLiftingTest, brp_Prop) { auto rewParameters = storm::models::sparse::getRewardParameters(*model); modelParameters.insert(rewParameters.begin(), rewParameters.end()); - storm::modelchecker::parametric::SparseMdpRegionChecker, double> regionChecker(*model); + storm::modelchecker::parametric::SparseMdpRegionChecker, double, storm::RationalNumber> regionChecker(*model); regionChecker.specifyFormula(storm::modelchecker::CheckTask(*formulas[0], true)); //start testing @@ -203,7 +201,7 @@ TEST(SparseMdpParameterLiftingTest, brp_Rew) { auto rewParameters = storm::models::sparse::getRewardParameters(*model); modelParameters.insert(rewParameters.begin(), rewParameters.end()); - storm::modelchecker::parametric::SparseMdpRegionChecker, double> regionChecker(*model); + storm::modelchecker::parametric::SparseMdpRegionChecker, double, storm::RationalNumber> regionChecker(*model); regionChecker.specifyFormula(storm::modelchecker::CheckTask(*formulas[0], true)); //start testing @@ -233,7 +231,7 @@ TEST(SparseMdpParameterLiftingTest, brp_Rew_bounded) { auto rewParameters = storm::models::sparse::getRewardParameters(*model); modelParameters.insert(rewParameters.begin(), rewParameters.end()); - storm::modelchecker::parametric::SparseMdpRegionChecker, double> regionChecker(*model); + storm::modelchecker::parametric::SparseMdpRegionChecker, double, storm::RationalNumber> regionChecker(*model); regionChecker.specifyFormula(storm::modelchecker::CheckTask(*formulas[0], true)); //start testing @@ -264,7 +262,7 @@ TEST(SparseMdpParameterLiftingTest, Brp_Rew_Infty) { auto rewParameters = storm::models::sparse::getRewardParameters(*model); modelParameters.insert(rewParameters.begin(), rewParameters.end()); - storm::modelchecker::parametric::SparseMdpRegionChecker, double> regionChecker(*model); + storm::modelchecker::parametric::SparseMdpRegionChecker, double, storm::RationalNumber> regionChecker(*model); regionChecker.specifyFormula(storm::modelchecker::CheckTask(*formulas[0], true)); //start testing @@ -290,7 +288,7 @@ TEST(SparseMdpParameterLiftingTest, Brp_Rew_4Par) { auto rewParameters = storm::models::sparse::getRewardParameters(*model); modelParameters.insert(rewParameters.begin(), rewParameters.end()); - storm::modelchecker::parametric::SparseMdpRegionChecker, double> regionChecker(*model); + storm::modelchecker::parametric::SparseMdpRegionChecker, double, storm::RationalNumber> regionChecker(*model); regionChecker.specifyFormula(storm::modelchecker::CheckTask(*formulas[0], true)); //start testing