From 29716ea5f8c4783d6635ce6c77343f0bbf1533a0 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 24 Aug 2015 22:15:50 +0200 Subject: [PATCH] performance tests now compile again. also fixed some warnings Former-commit-id: 2fa8c2abd9423d379a0b60c79ddc7552597d0f42 --- src/logic/BinaryPathFormula.h | 2 +- src/logic/BinaryStateFormula.h | 2 +- src/logic/UnaryPathFormula.h | 2 +- src/logic/UnaryStateFormula.h | 2 +- .../SparseMarkovAutomatonCslModelChecker.h | 2 +- src/models/sparse/DeterministicModel.h | 2 +- src/models/sparse/Model.h | 8 +- src/models/sparse/NondeterministicModel.h | 4 +- ...alValueIterationEquationSolverSettings.cpp | 4 - src/storage/dd/CuddAdd.h | 4 +- test/performance/graph/GraphTest.cpp | 1 + .../GmmxxDtmcPrctModelCheckerTest.cpp | 6 +- .../GmmxxMdpPrctlModelCheckerTest.cpp | 96 ++++----- .../NativeDtmcPrctlModelCheckerTest.cpp | 5 +- .../NativeMdpPrctlModelCheckerTest.cpp | 108 +++++----- ...ValueIterationMdpPrctlModelCheckerTest.cpp | 185 ++++++------------ 16 files changed, 164 insertions(+), 269 deletions(-) diff --git a/src/logic/BinaryPathFormula.h b/src/logic/BinaryPathFormula.h index 4eff96117..9f2278132 100644 --- a/src/logic/BinaryPathFormula.h +++ b/src/logic/BinaryPathFormula.h @@ -32,7 +32,7 @@ namespace storm { virtual void gatherAtomicExpressionFormulas(std::vector>& atomicExpressionFormulas) const override; virtual void gatherAtomicLabelFormulas(std::vector>& atomicLabelFormulas) const override; - virtual void gatherReferencedRewardModels(std::set& referencedRewardModels) const; + virtual void gatherReferencedRewardModels(std::set& referencedRewardModels) const override; private: std::shared_ptr leftSubformula; diff --git a/src/logic/BinaryStateFormula.h b/src/logic/BinaryStateFormula.h index 0fdc8dd47..a0fcbc9d1 100644 --- a/src/logic/BinaryStateFormula.h +++ b/src/logic/BinaryStateFormula.h @@ -30,7 +30,7 @@ namespace storm { virtual void gatherAtomicExpressionFormulas(std::vector>& atomicExpressionFormulas) const override; virtual void gatherAtomicLabelFormulas(std::vector>& atomicLabelFormulas) const override; - virtual void gatherReferencedRewardModels(std::set& referencedRewardModels) const; + virtual void gatherReferencedRewardModels(std::set& referencedRewardModels) const override; private: std::shared_ptr leftSubformula; diff --git a/src/logic/UnaryPathFormula.h b/src/logic/UnaryPathFormula.h index 74501823f..a91ffe38f 100644 --- a/src/logic/UnaryPathFormula.h +++ b/src/logic/UnaryPathFormula.h @@ -30,7 +30,7 @@ namespace storm { virtual void gatherAtomicExpressionFormulas(std::vector>& atomicExpressionFormulas) const override; virtual void gatherAtomicLabelFormulas(std::vector>& atomicLabelFormulas) const override; - virtual void gatherReferencedRewardModels(std::set& referencedRewardModels) const; + virtual void gatherReferencedRewardModels(std::set& referencedRewardModels) const override; private: std::shared_ptr subformula; diff --git a/src/logic/UnaryStateFormula.h b/src/logic/UnaryStateFormula.h index 3db2b9263..745687e6b 100644 --- a/src/logic/UnaryStateFormula.h +++ b/src/logic/UnaryStateFormula.h @@ -29,7 +29,7 @@ namespace storm { virtual void gatherAtomicExpressionFormulas(std::vector>& atomicExpressionFormulas) const override; virtual void gatherAtomicLabelFormulas(std::vector>& atomicLabelFormulas) const override; - virtual void gatherReferencedRewardModels(std::set& referencedRewardModels) const; + virtual void gatherReferencedRewardModels(std::set& referencedRewardModels) const override; private: std::shared_ptr subformula; diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index 26e47bd92..e93c36dec 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -25,7 +25,7 @@ namespace storm { virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); + virtual std::unique_ptr computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; private: // An object that is used for retrieving solvers for systems of linear equations that are the result of nondeterministic choices. diff --git a/src/models/sparse/DeterministicModel.h b/src/models/sparse/DeterministicModel.h index b63e15e22..fb3e367df 100644 --- a/src/models/sparse/DeterministicModel.h +++ b/src/models/sparse/DeterministicModel.h @@ -54,7 +54,7 @@ namespace storm { virtual void reduceToStateBasedRewards() override; - virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const; + virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const override; }; } // namespace sparse diff --git a/src/models/sparse/Model.h b/src/models/sparse/Model.h index 6c33efde4..bf9da8713 100644 --- a/src/models/sparse/Model.h +++ b/src/models/sparse/Model.h @@ -91,14 +91,14 @@ namespace storm { * * @return The number of states of the model. */ - virtual uint_fast64_t getNumberOfStates() const; + virtual uint_fast64_t getNumberOfStates() const override; /*! * Returns the number of (non-zero) transitions of the model. * * @return The number of (non-zero) transitions of the model. */ - virtual uint_fast64_t getNumberOfTransitions() const; + virtual uint_fast64_t getNumberOfTransitions() const override; /*! * Retrieves the initial states of the model. @@ -228,14 +228,14 @@ namespace storm { * * @return The size of the internal representation of the model measured in bytes. */ - virtual std::size_t getSizeInBytes() const; + virtual std::size_t getSizeInBytes() const override; /*! * Prints information about the model to the specified stream. * * @param out The stream the information is to be printed to. */ - virtual void printModelInformationToStream(std::ostream& out) const; + virtual void printModelInformationToStream(std::ostream& out) const override; /*! * Exports the model to the dot-format and prints the result to the given stream. diff --git a/src/models/sparse/NondeterministicModel.h b/src/models/sparse/NondeterministicModel.h index 603ff4a22..9c5a01b05 100644 --- a/src/models/sparse/NondeterministicModel.h +++ b/src/models/sparse/NondeterministicModel.h @@ -75,9 +75,9 @@ namespace storm { virtual void reduceToStateBasedRewards() override; - virtual void printModelInformationToStream(std::ostream& out) const; + virtual void printModelInformationToStream(std::ostream& out) const override; - virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const; + virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const override; }; } // namespace sparse diff --git a/src/settings/modules/TopologicalValueIterationEquationSolverSettings.cpp b/src/settings/modules/TopologicalValueIterationEquationSolverSettings.cpp index a1a00e283..1ab944e00 100644 --- a/src/settings/modules/TopologicalValueIterationEquationSolverSettings.cpp +++ b/src/settings/modules/TopologicalValueIterationEquationSolverSettings.cpp @@ -53,10 +53,6 @@ namespace storm { } bool TopologicalValueIterationEquationSolverSettings::check() const { - bool optionsSet = isMaximalIterationCountSet() || isPrecisionSet() || isConvergenceCriterionSet(); - - //STORM_LOG_WARN_COND(storm::settings::generalSettings().getEquationSolver() == storm::settings::modules::GeneralSettings::EquationSolver::Gmmxx || !optionsSet, "gmm++ is not selected as the equation solver, so setting options for gmm++ has no effect."); - return true; } diff --git a/src/storage/dd/CuddAdd.h b/src/storage/dd/CuddAdd.h index 76b949d6b..acdc3d5e1 100644 --- a/src/storage/dd/CuddAdd.h +++ b/src/storage/dd/CuddAdd.h @@ -406,7 +406,7 @@ namespace storm { * * @return The support represented as a BDD. */ - Bdd getSupport() const; + Bdd getSupport() const override; /*! * Retrieves the number of encodings that are mapped to a non-zero value. @@ -610,7 +610,7 @@ namespace storm { * * @param filename The name of the file to which the DD is to be exported. */ - void exportToDot(std::string const& filename = "") const; + void exportToDot(std::string const& filename = "") const override; /*! * Retrieves an iterator that points to the first meta variable assignment with a non-zero function value. diff --git a/test/performance/graph/GraphTest.cpp b/test/performance/graph/GraphTest.cpp index 7ff4e4989..6cf22672e 100644 --- a/test/performance/graph/GraphTest.cpp +++ b/test/performance/graph/GraphTest.cpp @@ -6,6 +6,7 @@ #include "src/storage/StronglyConnectedComponentDecomposition.h" #include "src/models/sparse/Mdp.h" #include "src/models/sparse/Dtmc.h" +#include "src/models/sparse/StandardRewardModel.h" TEST(GraphTest, ExplicitProb01) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", ""); diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp index 0ecce639f..a662daef9 100644 --- a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp @@ -8,7 +8,7 @@ #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/utility/solver.h" #include "src/parser/AutoParser.h" - +#include "src/models/sparse/StandardRewardModel.h" TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", ""); @@ -20,7 +20,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { ASSERT_EQ(2036647ull, dtmc->getNumberOfStates()); ASSERT_EQ(7362293ull, 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); @@ -58,7 +58,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { ASSERT_EQ(1312334ull, dtmc->getNumberOfStates()); ASSERT_EQ(1574477ull, 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); diff --git a/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 527dbed69..9c891cc06 100644 --- a/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -7,64 +7,63 @@ #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/utility/solver.h" #include "src/parser/AutoParser.h" +#include "src/models/sparse/StandardRewardModel.h" + +#include "src/parser/FormulaParser.h" TEST(GmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew"); ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + std::shared_ptr> mdp = abstractModel->as>(); ASSERT_EQ(2095783ull, mdp->getNumberOfStates()); ASSERT_EQ(7714385ull, 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); - auto minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + std::shared_ptr formula = parser.parseFromString("Pmin=? [F \"elected\"]"); - std::unique_ptr result = checker.check(*minProbabilityOperatorFormula); + std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - auto maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + formula = parser.parseFromString("Pmax=? [F \"elected\"]"); - result = checker.check(*maxProbabilityOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("elected"); - auto trueFormula = std::make_shared(true); - auto boundedUntilFormula = std::make_shared(trueFormula, labelFormula, 25); - minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, boundedUntilFormula); + formula = parser.parseFromString("Pmin=? [F<=25 \"elected\"]"); - result = checker.check(*minProbabilityOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, boundedUntilFormula); + formula = parser.parseFromString("Pmax=? [F<=25 \"elected\"]"); - result = checker.check(*maxProbabilityOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("elected"); - auto reachabilityRewardFormula = std::make_shared(labelFormula); - auto minRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmin=? [F \"elected\"]"); - result = checker.check(*minRewardOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(6.172433512, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - auto maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmax=? [F \"elected\"]"); - result = checker.check(*maxRewardOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(6.1724344, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -75,85 +74,68 @@ TEST(GmxxMdpPrctlModelCheckerTest, Consensus) { ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + std::shared_ptr> mdp = abstractModel->as>(); ASSERT_EQ(63616ull, mdp->getNumberOfStates()); ASSERT_EQ(213472ull, 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("finished"); - auto eventuallyFormula = std::make_shared(labelFormula); - auto minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + std::shared_ptr formula = parser.parseFromString("Pmin=? [F \"finished\"]"); - std::unique_ptr result = checker.check(*minProbabilityOperatorFormula); + std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0, quantitativeResult1[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("finished"); - auto labelFormula2 = std::make_shared("all_coins_equal_0"); - auto andFormula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::And, labelFormula, labelFormula2); - eventuallyFormula = std::make_shared(andFormula); - minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + formula = parser.parseFromString("Pmin=? [F \"finished\" & \"all_coins_equal_0\"]"); - result = checker.check(*minProbabilityOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.4374282832, quantitativeResult2[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("finished"); - labelFormula2 = std::make_shared("all_coins_equal_1"); - andFormula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::And, labelFormula, labelFormula2); - eventuallyFormula = std::make_shared(andFormula); - auto maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + formula = parser.parseFromString("Pmax=? [F \"finished\" & \"all_coins_equal_1\"]"); - result = checker.check(*maxProbabilityOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.5293286369, quantitativeResult3[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("finished"); - labelFormula2 = std::make_shared("agree"); - auto notFormula = std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, labelFormula2); - andFormula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::And, labelFormula, notFormula); - eventuallyFormula = std::make_shared(andFormula); - maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + formula = parser.parseFromString("Pmax=? [F \"finished\" & !\"agree\"]"); - result = checker.check(*maxProbabilityOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.10414097, quantitativeResult4[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("finished"); - auto trueFormula = std::make_shared(true); - auto boundedUntilFormula = std::make_shared(trueFormula, labelFormula, 50); - minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, boundedUntilFormula); + formula = parser.parseFromString("Pmin=? [F<=50 \"finished\"]"); - result = checker.check(*minProbabilityOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0, quantitativeResult5[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, boundedUntilFormula); + formula = parser.parseFromString("Pmax=? [F<=50 \"finished\"]"); - result = checker.check(*maxProbabilityOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0, quantitativeResult6[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("finished"); - auto reachabilityRewardFormula = std::make_shared(labelFormula); - auto minRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmin=? [F \"finished\"]"); - result = checker.check(*minRewardOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult7 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1725.593313, quantitativeResult7[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - auto maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmax=? [F \"finished\"]"); - result = checker.check(*maxRewardOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult8 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(2183.142422, quantitativeResult8[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); diff --git a/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp b/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp index cce9c8878..1207479a4 100644 --- a/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp @@ -9,6 +9,7 @@ #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/utility/solver.h" #include "src/parser/AutoParser.h" +#include "src/models/sparse/StandardRewardModel.h" TEST(NativeDtmcPrctlModelCheckerTest, Crowds) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", ""); @@ -20,7 +21,7 @@ TEST(NativeDtmcPrctlModelCheckerTest, Crowds) { ASSERT_EQ(2036647ull, dtmc->getNumberOfStates()); ASSERT_EQ(7362293ull, 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); @@ -58,7 +59,7 @@ TEST(NativeDtmcPrctlModelCheckerTest, SynchronousLeader) { ASSERT_EQ(1312334ull, dtmc->getNumberOfStates()); ASSERT_EQ(1574477ull, 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); diff --git a/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp index e327910d8..73b45ba91 100644 --- a/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp @@ -8,64 +8,63 @@ #include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/utility/solver.h" #include "src/parser/AutoParser.h" +#include "src/models/sparse/StandardRewardModel.h" + +#include "src/parser/FormulaParser.h" TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew"); ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + std::shared_ptr> mdp = abstractModel->as>(); ASSERT_EQ(2095783ull, mdp->getNumberOfStates()); ASSERT_EQ(7714385ull, 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); - auto minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + std::shared_ptr formula = parser.parseFromString("Pmin=? [F \"elected\"]"); - std::unique_ptr result = checker.check(*minProbabilityOperatorFormula); + std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - auto maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + formula = parser.parseFromString("Pmax=? [F \"elected\"]"); - result = checker.check(*maxProbabilityOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("elected"); - auto trueFormula = std::make_shared(true); - auto boundedUntilFormula = std::make_shared(trueFormula, labelFormula, 25); - minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, boundedUntilFormula); - - result = checker.check(*minProbabilityOperatorFormula); + formula = parser.parseFromString("Pmin=? [F<=25 \"elected\"]"); + + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, boundedUntilFormula); + formula = parser.parseFromString("Pmax=? [F<=25 \"elected\"]"); - result = checker.check(*maxProbabilityOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("elected"); - auto reachabilityRewardFormula = std::make_shared(labelFormula); - auto minRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); - - result = checker.check(*minRewardOperatorFormula); + formula = parser.parseFromString("Rmin=? [F \"elected\"]"); + + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(6.172433512, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - auto maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmax=? [F \"elected\"]"); - result = checker.check(*maxRewardOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(6.1724344, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -76,85 +75,68 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) { ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + std::shared_ptr> mdp = abstractModel->as>(); ASSERT_EQ(63616ull, mdp->getNumberOfStates()); ASSERT_EQ(213472ull, 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("finished"); - auto eventuallyFormula = std::make_shared(labelFormula); - auto minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); - - std::unique_ptr result = checker.check(*minProbabilityOperatorFormula); + std::shared_ptr formula = parser.parseFromString("Pmin=? [F \"finished\"]"); + + std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0, quantitativeResult1[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("finished"); - auto labelFormula2 = std::make_shared("all_coins_equal_0"); - auto andFormula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::And, labelFormula, labelFormula2); - eventuallyFormula = std::make_shared(andFormula); - minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + formula = parser.parseFromString("Pmin=? [F \"finished\" & \"all_coins_equal_0\"]"); - result = checker.check(*minProbabilityOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.4374282832, quantitativeResult2[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("finished"); - labelFormula2 = std::make_shared("all_coins_equal_1"); - andFormula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::And, labelFormula, labelFormula2); - eventuallyFormula = std::make_shared(andFormula); - auto maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + formula = parser.parseFromString("Pmax=? [F \"finished\" & \"all_coins_equal_1\"]"); - result = checker.check(*maxProbabilityOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.5293286369, quantitativeResult3[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("finished"); - labelFormula2 = std::make_shared("agree"); - auto notFormula = std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, labelFormula2); - andFormula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::And, labelFormula, notFormula); - eventuallyFormula = std::make_shared(andFormula); - maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); - - result = checker.check(*maxProbabilityOperatorFormula); + formula = parser.parseFromString("Pmax=? [F \"finished\" & !\"agree\"]"); + + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.10414097, quantitativeResult4[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("finished"); - auto trueFormula = std::make_shared(true); - auto boundedUntilFormula = std::make_shared(trueFormula, labelFormula, 50); - minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, boundedUntilFormula); - - result = checker.check(*minProbabilityOperatorFormula); + formula = parser.parseFromString("Pmin=? [F<=50 \"finished\"]"); + + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0, quantitativeResult5[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, boundedUntilFormula); + formula = parser.parseFromString("Pmax=? [F<=50 \"finished\"]"); - result = checker.check(*maxProbabilityOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0, quantitativeResult6[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("finished"); - auto reachabilityRewardFormula = std::make_shared(labelFormula); - auto minRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); - - result = checker.check(*minRewardOperatorFormula); + formula = parser.parseFromString("Rmin=? [F \"finished\"]"); + + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult7 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1725.593313, quantitativeResult7[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - auto maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmax=? [F \"finished\"]"); - result = checker.check(*maxRewardOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult8 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(2183.142422, quantitativeResult8[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); diff --git a/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp index 1e636e1b3..da7bb0214 100644 --- a/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp @@ -8,74 +8,51 @@ #include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h" #include "src/settings/SettingMemento.h" #include "src/parser/AutoParser.h" +#include "src/models/sparse/StandardRewardModel.h" +#include "src/parser/FormulaParser.h" TEST(DISABLED_TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) { std::shared_ptr> mdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew")->as>(); + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + ASSERT_EQ(mdp->getNumberOfStates(), 2095783ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385ull); - storm::modelchecker::SparseMdpPrctlModelChecker mc(*mdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); - - auto apFormula = std::make_shared("elected"); - auto eventuallyFormula = std::make_shared(apFormula); - auto probFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); - - std::unique_ptr result = mc.check(*probFormula); - - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 1.0), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - probFormula.reset(); - - apFormula = std::make_shared("elected"); - eventuallyFormula = std::make_shared(apFormula); - probFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); - - result = mc.check(*probFormula); - - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 1.0), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - probFormula.reset(); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); - apFormula = std::make_shared("elected"); - auto boundedEventuallyFormula = std::make_shared(std::make_shared(true), apFormula, 25); - probFormula = std::make_shared(storm::logic::OptimalityType::Minimize, boundedEventuallyFormula); - - result = mc.check(*probFormula); - - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 0.0), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - probFormula.reset(); - - apFormula = std::make_shared("elected"); - boundedEventuallyFormula = std::make_shared(std::make_shared(true), apFormula, 25); - probFormula = std::make_shared(storm::logic::OptimalityType::Maximize, boundedEventuallyFormula); - - result = mc.check(*probFormula); + std::shared_ptr formula = parser.parseFromString("Pmin=? [F \"elected\"]"); + + std::unique_ptr result = checker.check(*formula); - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 0.0), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - probFormula.reset(); + ASSERT_NEAR(1.0, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - apFormula = std::make_shared("elected"); - auto reachabilityRewardFormula = std::make_shared(apFormula); - auto rewardFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + formula = parser.parseFromString("Pmax=? [F \"elected\"]"); + + result = checker.check(*formula); + ASSERT_NEAR(1.0, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - result = mc.check(*rewardFormula); + formula = parser.parseFromString("Pmin=? [F<=25 \"elected\"]"); + + result = checker.check(*formula); - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 6.172433512), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - rewardFormula.reset(); + ASSERT_NEAR(0.0, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - apFormula = std::make_shared("elected"); - reachabilityRewardFormula = std::make_shared(apFormula); - rewardFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + formula = parser.parseFromString("Pmax=? [F<=25 \"elected\"]"); + + result = checker.check(*formula); + ASSERT_NEAR(0.0, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - result = mc.check(*rewardFormula); + formula = parser.parseFromString("Rmin=? [F \"elected\"]"); + + result = checker.check(*formula); + ASSERT_NEAR(6.172433512, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 6.1724344), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - rewardFormula.reset(); + formula = parser.parseFromString("Rmax=? [F \"elected\"]"); + + result = checker.check(*formula); + ASSERT_NEAR(6.1724344, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); } TEST(DISABLED_TopologicalValueIterationMdpPrctlModelCheckerTest, Consensus) { @@ -84,96 +61,52 @@ TEST(DISABLED_TopologicalValueIterationMdpPrctlModelCheckerTest, Consensus) { std::shared_ptr> mdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", "")->as>(); + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + ASSERT_EQ(mdp->getNumberOfStates(), 63616ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 213472ull); - storm::modelchecker::SparseMdpPrctlModelChecker mc(*mdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); - auto apFormula = std::make_shared("finished"); - auto eventuallyFormula = std::make_shared(apFormula); - auto probFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + std::shared_ptr formula = parser.parseFromString("Pmin=? [F \"finished\"]"); - auto result = mc.check(*probFormula); + std::unique_ptr result = checker.check(*formula); - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[31168] - 1.0), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - probFormula.reset(); + ASSERT_NEAR(1.0, result->asExplicitQuantitativeCheckResult()[31168], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - apFormula = std::make_shared("finished"); - auto apFormula2 = std::make_shared("all_coins_equal_0"); - auto andFormula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::And, apFormula, apFormula2); - eventuallyFormula = std::make_shared(andFormula); - probFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + formula = parser.parseFromString("Pmin=? [F \"finished\" & \"all_coins_equal_0\"]"); - result = mc.check(*probFormula); - - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[31168] - 0.4374282832), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - probFormula.reset(); - - - apFormula = std::make_shared("finished"); - apFormula2 = std::make_shared("all_coins_equal_1"); - andFormula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::And, apFormula, apFormula2); - eventuallyFormula = std::make_shared(andFormula); - probFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + result = checker.check(*formula); + ASSERT_NEAR(0.4374282832, result->asExplicitQuantitativeCheckResult()[31168], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - result = mc.check(*probFormula); + formula = parser.parseFromString("Pmax=? [F \"finished\" & \"all_coins_equal_1\"]"); - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[31168] - 0.5293286369), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - probFormula.reset(); + result = checker.check(*formula); + ASSERT_NEAR(0.5293286369, result->asExplicitQuantitativeCheckResult()[31168], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - apFormula = std::make_shared("finished"); - apFormula2 = std::make_shared("agree"); - auto notFormula = std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, apFormula2); - andFormula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::And, apFormula, notFormula); - eventuallyFormula = std::make_shared(andFormula); - probFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); - - result = mc.check(*probFormula); + formula = parser.parseFromString("Pmax=? [F \"finished\" & !\"agree\"]"); - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[31168] - 0.10414097), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - probFormula.reset(); + result = checker.check(*formula); + ASSERT_NEAR(0.10414097, result->asExplicitQuantitativeCheckResult()[31168], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - apFormula = std::make_shared("finished"); - auto boundedEventuallyFormula = std::make_shared(std::make_shared(true), apFormula, 50ull); - probFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); - - result = mc.check(*probFormula); + formula = parser.parseFromString("Pmin=? [F<=50 \"finished\"]"); - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[31168] - 0.0), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - probFormula.reset(); + result = checker.check(*formula); + ASSERT_NEAR(0.0, result->asExplicitQuantitativeCheckResult()[31168], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - apFormula = std::make_shared("finished"); - boundedEventuallyFormula = std::make_shared(std::make_shared(true), apFormula, 50ull); - probFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + formula = parser.parseFromString("Pmax=? [F<=50 \"finished\"]"); - result = mc.check(*probFormula); - - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[31168] - 0.0), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - probFormula.reset(); - - apFormula = std::make_shared("finished"); - auto reachabilityRewardFormula = std::make_shared(apFormula); - auto rewardFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + result = checker.check(*formula); + ASSERT_NEAR(0.0, result->asExplicitQuantitativeCheckResult()[31168], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - result = mc.check(*rewardFormula); + formula = parser.parseFromString("Rmin=? [F \"finished\"]"); - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[31168] - 1725.593313), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - probFormula.reset(); + result = checker.check(*formula); + ASSERT_NEAR(1725.593313, result->asExplicitQuantitativeCheckResult()[31168], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - apFormula = std::make_shared("finished"); - reachabilityRewardFormula = std::make_shared(apFormula); - rewardFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); - - result = mc.check(*rewardFormula); - - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[31168] - 2183.142422), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - probFormula.reset(); + formula = parser.parseFromString("Rmax=? [F \"finished\"\"]"); + + result = checker.check(*formula); + ASSERT_NEAR(2183.142422, result->asExplicitQuantitativeCheckResult()[31168], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); } \ No newline at end of file