From 72cb30d6b0e43b8870c4ea8e11d36eb278d39370 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 18 Aug 2015 10:35:38 +0200 Subject: [PATCH] started replacing ValueType template argument by model class in all instantiations Former-commit-id: 197e3876a4af1353c8ed5a227f80ece7be28e9a4 --- .../MILPMinimalLabelSetGenerator.h | 8 +++--- src/utility/cli.h | 16 +++++------ .../GmmxxCtmcCslModelCheckerTest.cpp | 8 +++--- .../GmmxxDtmcPrctlModelCheckerTest.cpp | 22 +++++++-------- .../GmmxxMdpPrctlModelCheckerTest.cpp | 8 +++--- .../NativeCtmcCslModelCheckerTest.cpp | 8 +++--- .../NativeDtmcPrctlModelCheckerTest.cpp | 22 +++++++-------- .../NativeMdpPrctlModelCheckerTest.cpp | 28 +++++++++---------- .../SparseDtmcEliminationModelCheckerTest.cpp | 6 ++-- 9 files changed, 62 insertions(+), 64 deletions(-) diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 1339d646a..098566707 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -6,7 +6,7 @@ #include "src/models/sparse/Mdp.h" #include "src/logic/Formulas.h" #include "src/storage/prism/Program.h" -#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" +#include "src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/exceptions/NotImplementedException.h" @@ -932,8 +932,8 @@ namespace storm { // (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set. double maximalReachabilityProbability = 0; if (checkThresholdFeasible) { - storm::modelchecker::SparseMdpPrctlModelChecker modelchecker(labeledMdp); - std::vector result = modelchecker.computeUntilProbabilitiesHelper(false, phiStates, psiStates, false); + storm::modelchecker::helper::SparseMdpPrctlHelper modelcheckerHelper; + std::vector result = modelcheckerHelper.computeUntilProbabilities(false, labeledMdp.getTransitionMatrix(), labeledMdp.getBackwardTransitions(), phiStates, psiStates, false, storm::utility::solver::MinMaxLinearEquationSolverFactory()); for (auto state : labeledMdp.getInitialStates()) { maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]); } @@ -991,7 +991,7 @@ namespace storm { storm::storage::BitVector phiStates; storm::storage::BitVector psiStates; - storm::modelchecker::SparseMdpPrctlModelChecker modelchecker(labeledMdp); + storm::modelchecker::SparsePropositionalModelChecker> modelchecker(labeledMdp); if (probabilityOperator.getSubformula().isUntilFormula()) { storm::logic::UntilFormula const& untilFormula = probabilityOperator.getSubformula().asUntilFormula(); diff --git a/src/utility/cli.h b/src/utility/cli.h index c48a4a262..2a7914d48 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -72,9 +72,7 @@ namespace storm { namespace utility { namespace cli { - - - std::string getCurrentWorkingDirectory(); + std::string getCurrentWorkingDirectory(); void printHeader(const int argc, const char* argv[]); @@ -213,11 +211,11 @@ namespace storm { std::unique_ptr result; if (model->getType() == storm::models::ModelType::Dtmc) { std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::SparseDtmcPrctlModelChecker modelchecker(*dtmc); + storm::modelchecker::SparseDtmcPrctlModelChecker> modelchecker(*dtmc); if (modelchecker.canHandle(*formula.get())) { result = modelchecker.check(*formula.get()); } else { - storm::modelchecker::SparseDtmcEliminationModelChecker modelchecker2(*dtmc); + storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker2(*dtmc); if (modelchecker2.canHandle(*formula.get())) { result = modelchecker2.check(*formula.get()); } @@ -229,17 +227,17 @@ namespace storm { storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker modelchecker(*mdp); result = modelchecker.check(*formula.get()); } else { - storm::modelchecker::SparseMdpPrctlModelChecker modelchecker(*mdp); + storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(*mdp); result = modelchecker.check(*formula.get()); } #else - storm::modelchecker::SparseMdpPrctlModelChecker modelchecker(*mdp); + storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(*mdp); result = modelchecker.check(*formula.get()); #endif } else if (model->getType() == storm::models::ModelType::Ctmc) { std::shared_ptr> ctmc = model->template as>(); - storm::modelchecker::SparseCtmcCslModelChecker modelchecker(*ctmc); + storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc); result = modelchecker.check(*formula.get()); } @@ -281,7 +279,7 @@ namespace storm { std::cout << std::endl << "Model checking property: " << *formula << " ..."; std::unique_ptr result; - storm::modelchecker::SparseDtmcEliminationModelChecker modelchecker(*dtmc); + storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker(*dtmc); if (modelchecker.canHandle(*formula.get())) { result = modelchecker.check(*formula.get()); } else { diff --git a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp index 76f178e8f..db391045f 100644 --- a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp @@ -37,7 +37,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Cluster) { uint_fast64_t initialState = *ctmc->getInitialStates().begin(); // Create model checker. - storm::modelchecker::SparseCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); // Start checking properties. formula = formulaParser.parseFromString("P=? [ F<=100 !\"minimum\"]"); @@ -121,7 +121,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Embedded) { uint_fast64_t initialState = *ctmc->getInitialStates().begin(); // Create model checker. - storm::modelchecker::SparseCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); // Start checking properties. formula = formulaParser.parseFromString("P=? [ F<=10000 \"down\"]"); @@ -183,7 +183,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Polling) { uint_fast64_t initialState = *ctmc->getInitialStates().begin(); // Create model checker. - storm::modelchecker::SparseCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); // Start checking properties. formula = formulaParser.parseFromString("P=?[ F<=10 \"target\"]"); @@ -231,7 +231,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Tandem) { uint_fast64_t initialState = *ctmc->getInitialStates().begin(); // Create model checker. - storm::modelchecker::SparseCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); // Start checking properties. formula = formulaParser.parseFromString("P=? [ F<=10 \"network_full\" ]"); diff --git a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp index 01f97ba61..c0ad1325b 100644 --- a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp @@ -21,7 +21,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) { ASSERT_EQ(dtmc->getNumberOfStates(), 13ull); ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull); - storm::modelchecker::SparseDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); auto labelFormula = std::make_shared("one"); auto eventuallyFormula = std::make_shared(labelFormula); @@ -66,7 +66,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { ASSERT_EQ(8607ull, dtmc->getNumberOfStates()); ASSERT_EQ(15113ull, dtmc->getNumberOfTransitions()); - storm::modelchecker::SparseDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); auto labelFormula = std::make_shared("observe0Greater1"); auto eventuallyFormula = std::make_shared(labelFormula); @@ -102,7 +102,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { ASSERT_EQ(12400ull, dtmc->getNumberOfStates()); ASSERT_EQ(16495ull, dtmc->getNumberOfTransitions()); - storm::modelchecker::SparseDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); auto labelFormula = std::make_shared("elected"); auto eventuallyFormula = std::make_shared(labelFormula); @@ -144,9 +144,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) { ap.addLabel("a"); ap.addLabelToState("a", 1); - dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap, boost::none, boost::none, boost::none)); + dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap)); - storm::modelchecker::SparseDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); auto labelFormula = std::make_shared("a"); auto lraFormula = std::make_shared(labelFormula); @@ -169,9 +169,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) { ap.addLabel("a"); ap.addLabelToState("a", 1); - dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap, boost::none, boost::none, boost::none)); + dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap)); - storm::modelchecker::SparseDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); auto labelFormula = std::make_shared("a"); auto lraFormula = std::make_shared(labelFormula); @@ -194,9 +194,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) { ap.addLabel("a"); ap.addLabelToState("a", 2); - dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap, boost::none, boost::none, boost::none)); + dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap)); - storm::modelchecker::SparseDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); auto labelFormula = std::make_shared("a"); auto lraFormula = std::make_shared(labelFormula); @@ -255,9 +255,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRA) { ap.addLabelToState("a", 13); ap.addLabelToState("a", 14); - mdp.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap, boost::none, boost::none, boost::none)); + mdp.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap)); - storm::modelchecker::SparseDtmcPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); auto labelFormula = std::make_shared("a"); auto lraFormula = std::make_shared(labelFormula); diff --git a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 69dcda869..9983c65e7 100644 --- a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -21,7 +21,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { ASSERT_EQ(mdp->getNumberOfStates(), 169ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); - storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); auto labelFormula = std::make_shared("two"); auto eventuallyFormula = std::make_shared(labelFormula); @@ -93,7 +93,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> stateRewardMdp = abstractModel->as>(); - storm::modelchecker::SparseMdpPrctlModelChecker stateRewardModelChecker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> stateRewardModelChecker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); labelFormula = std::make_shared("done"); reachabilityRewardFormula = std::make_shared(labelFormula); @@ -117,7 +117,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> stateAndTransitionRewardMdp = abstractModel->as>(); - storm::modelchecker::SparseMdpPrctlModelChecker stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); labelFormula = std::make_shared("done"); reachabilityRewardFormula = std::make_shared(labelFormula); @@ -146,7 +146,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(3172ull, mdp->getNumberOfStates()); ASSERT_EQ(7144ull, mdp->getNumberOfTransitions()); - storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); auto labelFormula = std::make_shared("elected"); auto eventuallyFormula = std::make_shared(labelFormula); diff --git a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp index a7ee670b6..3da0ce7b1 100644 --- a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp @@ -37,7 +37,7 @@ TEST(SparseCtmcCslModelCheckerTest, Cluster) { uint_fast64_t initialState = *ctmc->getInitialStates().begin(); // Create model checker. - storm::modelchecker::SparseCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); // Start checking properties. formula = formulaParser.parseFromString("P=? [ F<=100 !\"minimum\"]"); @@ -113,7 +113,7 @@ TEST(SparseCtmcCslModelCheckerTest, Embedded) { uint_fast64_t initialState = *ctmc->getInitialStates().begin(); // Create model checker. - storm::modelchecker::SparseCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); // Start checking properties. formula = formulaParser.parseFromString("P=? [ F<=10000 \"down\"]"); @@ -168,7 +168,7 @@ TEST(SparseCtmcCslModelCheckerTest, Polling) { uint_fast64_t initialState = *ctmc->getInitialStates().begin(); // Create model checker. - storm::modelchecker::SparseCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); // Start checking properties. formula = formulaParser.parseFromString("P=?[ F<=10 \"target\"]"); @@ -209,7 +209,7 @@ TEST(SparseCtmcCslModelCheckerTest, Tandem) { uint_fast64_t initialState = *ctmc->getInitialStates().begin(); // Create model checker. - storm::modelchecker::SparseCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); // Start checking properties. formula = formulaParser.parseFromString("P=? [ F<=10 \"network_full\" ]"); diff --git a/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp index ced23c35e..9b6a4aa00 100644 --- a/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp @@ -22,7 +22,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, Die) { ASSERT_EQ(dtmc->getNumberOfStates(), 13ull); ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull); - storm::modelchecker::SparseDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); auto labelFormula = std::make_shared("one"); auto eventuallyFormula = std::make_shared(labelFormula); @@ -67,7 +67,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, Crowds) { ASSERT_EQ(8607ull, dtmc->getNumberOfStates()); ASSERT_EQ(15113ull, dtmc->getNumberOfTransitions()); - storm::modelchecker::SparseDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); auto labelFormula = std::make_shared("observe0Greater1"); auto eventuallyFormula = std::make_shared(labelFormula); @@ -103,7 +103,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, SynchronousLeader) { ASSERT_EQ(12400ull, dtmc->getNumberOfStates()); ASSERT_EQ(16495ull, dtmc->getNumberOfTransitions()); - storm::modelchecker::SparseDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); auto labelFormula = std::make_shared("elected"); auto eventuallyFormula = std::make_shared(labelFormula); @@ -145,9 +145,9 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) { ap.addLabel("a"); ap.addLabelToState("a", 1); - dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap, boost::none, boost::none, boost::none)); + dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap)); - storm::modelchecker::SparseDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory(storm::solver::NativeLinearEquationSolver::SolutionMethod::SOR, 0.9))); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory(storm::solver::NativeLinearEquationSolver::SolutionMethod::SOR, 0.9))); auto labelFormula = std::make_shared("a"); auto lraFormula = std::make_shared(labelFormula); @@ -170,9 +170,9 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) { ap.addLabel("a"); ap.addLabelToState("a", 1); - dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap, boost::none, boost::none, boost::none)); + dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap)); - storm::modelchecker::SparseDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory(storm::solver::NativeLinearEquationSolver::SolutionMethod::SOR, 0.9))); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory(storm::solver::NativeLinearEquationSolver::SolutionMethod::SOR, 0.9))); auto labelFormula = std::make_shared("a"); auto lraFormula = std::make_shared(labelFormula); @@ -195,9 +195,9 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) { ap.addLabel("a"); ap.addLabelToState("a", 2); - dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap, boost::none, boost::none, boost::none)); + dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap)); - storm::modelchecker::SparseDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory(storm::solver::NativeLinearEquationSolver::SolutionMethod::SOR, 0.9))); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory(storm::solver::NativeLinearEquationSolver::SolutionMethod::SOR, 0.9))); auto labelFormula = std::make_shared("a"); auto lraFormula = std::make_shared(labelFormula); @@ -256,9 +256,9 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRA) { ap.addLabelToState("a", 13); ap.addLabelToState("a", 14); - mdp.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap, boost::none, boost::none, boost::none)); + mdp.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap)); - storm::modelchecker::SparseDtmcPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory(storm::solver::NativeLinearEquationSolver::SolutionMethod::SOR, 0.9))); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory(storm::solver::NativeLinearEquationSolver::SolutionMethod::SOR, 0.9))); auto labelFormula = std::make_shared("a"); auto lraFormula = std::make_shared(labelFormula); diff --git a/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp index 87a4f0e21..c26b9c881 100644 --- a/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp @@ -20,7 +20,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { ASSERT_EQ(mdp->getNumberOfStates(), 169ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); - storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); auto labelFormula = std::make_shared("two"); auto eventuallyFormula = std::make_shared(labelFormula); @@ -92,7 +92,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> stateRewardMdp = abstractModel->as>(); - storm::modelchecker::SparseMdpPrctlModelChecker stateRewardModelChecker(*stateRewardMdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); labelFormula = std::make_shared("done"); reachabilityRewardFormula = std::make_shared(labelFormula); @@ -116,7 +116,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> stateAndTransitionRewardMdp = abstractModel->as>(); - storm::modelchecker::SparseMdpPrctlModelChecker stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); labelFormula = std::make_shared("done"); reachabilityRewardFormula = std::make_shared(labelFormula); @@ -145,7 +145,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(3172ull, mdp->getNumberOfStates()); ASSERT_EQ(7144ull, mdp->getNumberOfTransitions()); - storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); auto labelFormula = std::make_shared("elected"); auto eventuallyFormula = std::make_shared(labelFormula); @@ -211,9 +211,9 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) { ap.addLabel("a"); ap.addLabelToState("a", 1); - mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap, boost::none, boost::none, boost::none)); + mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); - storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); auto labelFormula = std::make_shared("a"); auto lraFormula = std::make_shared(storm::logic::OptimalityType::Maximize, labelFormula); @@ -244,9 +244,9 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) { ap.addLabel("a"); ap.addLabelToState("a", 1); - mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap, boost::none, boost::none, boost::none)); + mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); - storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); auto labelFormula = std::make_shared("a"); auto lraFormula = std::make_shared(storm::logic::OptimalityType::Maximize, labelFormula); @@ -286,9 +286,9 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) { ap.addLabelToState("c", 0); ap.addLabelToState("c", 2); - mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap, boost::none, boost::none, boost::none)); + mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); - storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); auto labelFormula = std::make_shared("a"); auto lraFormula = std::make_shared(storm::logic::OptimalityType::Maximize, labelFormula); @@ -372,9 +372,9 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) { ap.addLabel("c"); ap.addLabelToState("c", 2); - mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap, boost::none, boost::none, boost::none)); + mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); - storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); auto labelFormula = std::make_shared("a"); auto lraFormula = std::make_shared(storm::logic::OptimalityType::Maximize, labelFormula); @@ -497,9 +497,9 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) { ap.addLabelToState("a", 13); ap.addLabelToState("a", 14); - mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap, boost::none, boost::none, boost::none)); + mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); - storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); auto labelFormula = std::make_shared("a"); auto lraFormula = std::make_shared(storm::logic::OptimalityType::Maximize, labelFormula); diff --git a/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp b/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp index e14a146d6..86b4494f8 100644 --- a/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp @@ -20,7 +20,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, Die) { ASSERT_EQ(dtmc->getNumberOfStates(), 13ull); ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull); - storm::modelchecker::SparseDtmcEliminationModelChecker checker(*dtmc); + storm::modelchecker::SparseDtmcEliminationModelChecker> checker(*dtmc); auto labelFormula = std::make_shared("one"); auto eventuallyFormula = std::make_shared(labelFormula); @@ -65,7 +65,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, Crowds) { ASSERT_EQ(8607ull, dtmc->getNumberOfStates()); ASSERT_EQ(15113ull, dtmc->getNumberOfTransitions()); - storm::modelchecker::SparseDtmcEliminationModelChecker checker(*dtmc); + storm::modelchecker::SparseDtmcEliminationModelChecker> checker(*dtmc); auto labelFormula = std::make_shared("observe0Greater1"); auto eventuallyFormula = std::make_shared(labelFormula); @@ -125,7 +125,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, SynchronousLeader) { ASSERT_EQ(12400ull, dtmc->getNumberOfStates()); ASSERT_EQ(16495ull, dtmc->getNumberOfTransitions()); - storm::modelchecker::SparseDtmcEliminationModelChecker checker(*dtmc); + storm::modelchecker::SparseDtmcEliminationModelChecker> checker(*dtmc); auto labelFormula = std::make_shared("elected"); auto eventuallyFormula = std::make_shared(labelFormula);