From c1b3a4f991198b700ddc6047caf1569a67de14cb Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 30 Jul 2019 17:19:13 +0200 Subject: [PATCH] LraMdpPrctlModelCheckerTest: Test LRA computation for different environments. Added a testcase. --- resources/examples/testfiles/mdp/cs_nfail3.nm | 74 ++ .../solver/MinMaxSolverEnvironment.cpp | 17 + .../solver/MinMaxSolverEnvironment.h | 5 + .../helper/SparseMarkovAutomatonCslHelper.cpp | 7 +- .../prctl/helper/SparseMdpPrctlHelper.cpp | 8 +- .../LraMdpPrctlModelCheckerTest.cpp | 772 ++++++++++-------- 6 files changed, 550 insertions(+), 333 deletions(-) create mode 100644 resources/examples/testfiles/mdp/cs_nfail3.nm diff --git a/resources/examples/testfiles/mdp/cs_nfail3.nm b/resources/examples/testfiles/mdp/cs_nfail3.nm new file mode 100644 index 000000000..6a300595e --- /dev/null +++ b/resources/examples/testfiles/mdp/cs_nfail3.nm @@ -0,0 +1,74 @@ +mdp + +module server + + s:[0..3]; + i:[0..3]; + j:[0..3]; + + // initial cancel loops + [client1_cancel] s=0 -> true; + [client2_cancel] s=0 -> true; + [client3_cancel] s=0 -> true; + + // client i request/grant/cancel + [client1_request] s=0 -> (s'=1) & (i'=1); + [client1_grant] s=1 & i=1 -> (s'=2); + [client1_cancel] s=2 & i=1 -> (s'=0) & (i'=0); + [client2_request] s=0 -> (s'=1) & (i'=2); + [client2_grant] s=1 & i=2 -> (s'=2); + [client2_cancel] s=2 & i=2 -> (s'=0) & (i'=0); + [client3_request] s=0 -> (s'=1) & (i'=3); + [client3_grant] s=1 & i=3 -> (s'=2); + [client3_cancel] s=2 & i=3 -> (s'=0) & (i'=0); + + // deny other requests when serving + [client1_request] s=2 -> (s'=3) & (j'=1); + [client1_deny] s=3 & j=1 -> (s'=2) & (j'=0); + [client2_request] s=2 -> (s'=3) & (j'=2); + [client2_deny] s=3 & j=2 -> (s'=2) & (j'=0); + [client3_request] s=2 -> (s'=3) & (j'=3); + [client3_deny] s=3 & j=3 -> (s'=2) & (j'=0); + + // cancel loops when serving + [client1_cancel] s=2 & i!=1 -> true; + [client2_cancel] s=2 & i!=2 -> true; + [client3_cancel] s=2 & i!=3 -> true; + +endmodule + +module client1 + + c1:[-1..3]; + + [client1_ch_mind] c1=-1 -> 0.9:(c1'=0)+0.1:(c1'=3); + // change mind with probability 0.1 + [client1_request] c1=0 -> (c1'=1); + [client1_deny] c1=1 -> (c1'=0); + [client1_grant] c1=1 -> (c1'=2); + [client1_useResource] c1=2 -> (c1'=2); + [client1_cancel] c1=2 -> (c1'=0); + [client1_cancel] c1=3 -> (c1'=1); + +endmodule + +module client2 = client1[ c1=c2, client1_ch_mind=client2_ch_mind, client1_request=client2_request, +client1_deny=client2_deny, client1_grant=client2_grant, +client1_useResource=client2_useResource, client1_cancel=client2_cancel] + +endmodule + +module client3 = client1[ c1=c3, client1_ch_mind=client3_ch_mind, client1_request=client3_request, +client1_deny=client3_deny, client1_grant=client3_grant, +client1_useResource=client3_useResource, client1_cancel=client3_cancel] + +endmodule + + +rewards "grants" + [client1_grant] true : 1; + [client2_grant] true : 1; + [client3_grant] true : 1; +endrewards + + diff --git a/src/storm/environment/solver/MinMaxSolverEnvironment.cpp b/src/storm/environment/solver/MinMaxSolverEnvironment.cpp index 63cf5c698..63f29573e 100644 --- a/src/storm/environment/solver/MinMaxSolverEnvironment.cpp +++ b/src/storm/environment/solver/MinMaxSolverEnvironment.cpp @@ -22,6 +22,8 @@ namespace storm { STORM_LOG_ASSERT(considerRelativeTerminationCriterion || minMaxSettings.getConvergenceCriterion() == storm::settings::modules::MinMaxEquationSolverSettings::ConvergenceCriterion::Absolute, "Unknown convergence criterion"); multiplicationStyle = minMaxSettings.getValueIterationMultiplicationStyle(); symmetricUpdates = minMaxSettings.isForceIntervalIterationSymmetricUpdatesSet(); + lraMethod = minMaxSettings.getLraMethod(); + lraMethodSetFromDefault = minMaxSettings.isLraMethodSetFromDefaultValue(); } MinMaxSolverEnvironment::~MinMaxSolverEnvironment() { @@ -81,4 +83,19 @@ namespace storm { symmetricUpdates = value; } + storm::solver::LraMethod const& MinMaxSolverEnvironment::getLraMethod() const { + return lraMethod; + } + + bool const& MinMaxSolverEnvironment::isLraMethodSetFromDefault() const { + return lraMethodSetFromDefault; + } + + void MinMaxSolverEnvironment::setLraMethod(storm::solver::LraMethod value, bool isSetFromDefault) { + lraMethod = value; + lraMethodSetFromDefault = isSetFromDefault; + } + + + } diff --git a/src/storm/environment/solver/MinMaxSolverEnvironment.h b/src/storm/environment/solver/MinMaxSolverEnvironment.h index b0a19d8c4..104eee739 100644 --- a/src/storm/environment/solver/MinMaxSolverEnvironment.h +++ b/src/storm/environment/solver/MinMaxSolverEnvironment.h @@ -27,6 +27,9 @@ namespace storm { void setMultiplicationStyle(storm::solver::MultiplicationStyle value); bool isSymmetricUpdatesSet() const; void setSymmetricUpdates(bool value); + storm::solver::LraMethod const& getLraMethod() const; + bool const& isLraMethodSetFromDefault() const; + void setLraMethod(storm::solver::LraMethod value, bool isSetFromDefault = false); private: storm::solver::MinMaxMethod minMaxMethod; @@ -36,6 +39,8 @@ namespace storm { bool considerRelativeTerminationCriterion; storm::solver::MultiplicationStyle multiplicationStyle; bool symmetricUpdates; + storm::solver::LraMethod lraMethod; + bool lraMethodSetFromDefault; }; } diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index ef5518668..9dbce4cce 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -877,12 +877,11 @@ namespace storm { } // Solve MEC with the method specified in the settings - auto minMaxSettings = storm::settings::getModule(); - storm::solver::LraMethod method = minMaxSettings.getLraMethod(); - if (storm::NumberTraits::IsExact && minMaxSettings.isLraMethodSetFromDefaultValue() && method != storm::solver::LraMethod::LinearProgramming) { + storm::solver::LraMethod method = env.solver().minMax().getLraMethod(); + if (storm::NumberTraits::IsExact && env.solver().minMax().isLraMethodSetFromDefault() && method != storm::solver::LraMethod::LinearProgramming) { STORM_LOG_INFO("Selecting 'LP' as the solution technique for long-run properties to guarantee exact results. If you want to override this, please explicitly specify a different LRA method."); method = storm::solver::LraMethod::LinearProgramming; - } else if (env.solver().isForceSoundness() && minMaxSettings.isLraMethodSetFromDefaultValue() && method != storm::solver::LraMethod::ValueIteration) { + } else if (env.solver().isForceSoundness() && env.solver().minMax().isLraMethodSetFromDefault() && method != storm::solver::LraMethod::ValueIteration) { STORM_LOG_INFO("Selecting 'VI' as the solution technique for long-run properties to guarantee sound results. If you want to override this, please explicitly specify a different LRA method."); method = storm::solver::LraMethod::ValueIteration; } diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 85817db72..9e036a383 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -26,7 +26,6 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/ModelCheckerSettings.h" -#include "storm/settings/modules/MinMaxEquationSolverSettings.h" #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/CoreSettings.h" #include "storm/settings/modules/IOSettings.h" @@ -1410,12 +1409,11 @@ namespace storm { } // Solve MEC with the method specified in the settings - auto minMaxSettings = storm::settings::getModule(); - storm::solver::LraMethod method = minMaxSettings.getLraMethod(); - if (storm::NumberTraits::IsExact && minMaxSettings.isLraMethodSetFromDefaultValue() && method != storm::solver::LraMethod::LinearProgramming) { + storm::solver::LraMethod method = env.solver().minMax().getLraMethod(); + if (storm::NumberTraits::IsExact && env.solver().minMax().isLraMethodSetFromDefault() && method != storm::solver::LraMethod::LinearProgramming) { STORM_LOG_INFO("Selecting 'LP' as the solution technique for long-run properties to guarantee exact results. If you want to override this, please explicitly specify a different LRA method."); method = storm::solver::LraMethod::LinearProgramming; - } else if (env.solver().isForceSoundness() && minMaxSettings.isLraMethodSetFromDefaultValue() && method != storm::solver::LraMethod::ValueIteration) { + } else if (env.solver().isForceSoundness() && env.solver().minMax().isLraMethodSetFromDefault() && method != storm::solver::LraMethod::ValueIteration) { STORM_LOG_INFO("Selecting 'VI' as the solution technique for long-run properties to guarantee sound results. If you want to override this, please explicitly specify a different LRA method."); method = storm::solver::LraMethod::ValueIteration; } diff --git a/src/test/storm/modelchecker/LraMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/LraMdpPrctlModelCheckerTest.cpp index b05ebfb76..c0f527bd2 100644 --- a/src/test/storm/modelchecker/LraMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/LraMdpPrctlModelCheckerTest.cpp @@ -1,6 +1,15 @@ #include "gtest/gtest.h" + +#include "test/storm_gtest.h" + #include "storm-config.h" +#include "storm/api/builder.h" +#include "storm-conv/api/storm-conv.h" +#include "storm-parsers/api/model_descriptions.h" +#include "storm/api/properties.h" +#include "storm-parsers/api/properties.h" + #include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/Formulas.h" #include "storm/solver/StandardMinMaxLinearEquationSolver.h" @@ -13,332 +22,447 @@ #include "storm/settings/modules/NativeEquationSolverSettings.h" #include "storm-parsers/parser/AutoParser.h" - -TEST(LraMdpPrctlModelCheckerTest, LRA_SingleMec) { - storm::storage::SparseMatrixBuilder matrixBuilder; - std::shared_ptr> mdp; - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - { - matrixBuilder = storm::storage::SparseMatrixBuilder(2, 2, 2); - matrixBuilder.addNextValue(0, 1, 1.); - matrixBuilder.addNextValue(1, 0, 1.); - storm::storage::SparseMatrix transitionMatrix = matrixBuilder.build(); - - storm::models::sparse::StateLabeling ap(2); - ap.addLabel("a"); - ap.addLabelToState("a", 1); - - mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); - - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(.5, quantitativeResult1[1], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(.5, quantitativeResult2[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(.5, quantitativeResult2[1], storm::settings::getModule().getPrecision()); +#include "storm/environment/solver/MinMaxSolverEnvironment.h" + +namespace { + + + class SparseValueTypeValueIterationEnvironment { + public: + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Mdp ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setLraMethod(storm::solver::LraMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); + return env; + } + }; + + class SparseValueTypeLinearProgrammingEnvironment { + public: + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Mdp ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setLraMethod(storm::solver::LraMethod::LinearProgramming); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); + return env; + } + }; + + class SparseRationalLinearProgrammingEnvironment { + public: + static const bool isExact = true; + typedef storm::RationalNumber ValueType; + typedef storm::models::sparse::Mdp ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setLraMethod(storm::solver::LraMethod::LinearProgramming); + return env; + } + }; + + template + class LraMdpPrctlModelCheckerTest : public ::testing::Test { + public: + typedef typename TestType::ValueType ValueType; + typedef typename storm::models::sparse::Mdp SparseModelType; + + LraMdpPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {} + storm::Environment const& env() const { return _environment; } + ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber(input);} + ValueType precision() const { return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");} + bool isSparseModel() const { return std::is_same::value; } + + std::pair, std::vector>> buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { + std::pair, std::vector>> result; + storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); + program = storm::utility::prism::preprocess(program, constantDefinitionString); + result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + result.first = storm::api::buildSparseModel(program, result.second)->template as(); + return result; + } + + std::vector> getTasks(std::vector> const& formulas) const { + std::vector> result; + for (auto const& f : formulas) { + result.emplace_back(*f); + } + return result; + } + + private: + storm::Environment _environment; + }; + + typedef ::testing::Types< + SparseValueTypeValueIterationEnvironment, + SparseValueTypeLinearProgrammingEnvironment +#ifdef STORM_HAVE_Z3_OPTIMIZE + , SparseRationalLinearProgrammingEnvironment +#endif + > TestingTypes; + + TYPED_TEST_CASE(LraMdpPrctlModelCheckerTest, TestingTypes); + + + TYPED_TEST(LraMdpPrctlModelCheckerTest, LRA_SingleMec) { + typedef typename TestFixture::ValueType ValueType; + + storm::storage::SparseMatrixBuilder matrixBuilder; + std::shared_ptr> mdp; + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; + + { + matrixBuilder = storm::storage::SparseMatrixBuilder(2, 2, 2); + matrixBuilder.addNextValue(0, 1, this->parseNumber("1")); + matrixBuilder.addNextValue(1, 0, this->parseNumber("1")); + storm::storage::SparseMatrix transitionMatrix = matrixBuilder.build(); + + storm::models::sparse::StateLabeling ap(2); + ap.addLabel("a"); + ap.addLabelToState("a", 1); + + mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); + + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); + + std::unique_ptr result = checker.check(this->env(), *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[0], this->precision()); + EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[1], this->precision()); + + formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]"); + + result = checker.check(this->env(), *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult2[0], this->precision()); + EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult2[1], this->precision()); + } + { + matrixBuilder = storm::storage::SparseMatrixBuilder(2, 2, 4); + matrixBuilder.addNextValue(0, 0, this->parseNumber("0.5")); + matrixBuilder.addNextValue(0, 1, this->parseNumber("0.5")); + matrixBuilder.addNextValue(1, 0, this->parseNumber("0.5")); + matrixBuilder.addNextValue(1, 1, this->parseNumber("0.5")); + storm::storage::SparseMatrix transitionMatrix = matrixBuilder.build(); + + storm::models::sparse::StateLabeling ap(2); + ap.addLabel("a"); + ap.addLabelToState("a", 1); + + mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); + + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); + + std::unique_ptr result = checker.check(this->env(), *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[0], this->precision()); + EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[1], this->precision()); + + formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]"); + + result = checker.check(this->env(), *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult2[0], this->precision()); + EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult2[1], this->precision()); + } + { + matrixBuilder = storm::storage::SparseMatrixBuilder(4, 3, 4, true, true, 3); + matrixBuilder.newRowGroup(0); + matrixBuilder.addNextValue(0, 1, this->parseNumber("1")); + matrixBuilder.newRowGroup(1); + matrixBuilder.addNextValue(1, 0, this->parseNumber("1")); + matrixBuilder.addNextValue(2, 2, this->parseNumber("1")); + matrixBuilder.newRowGroup(3); + matrixBuilder.addNextValue(3, 0, this->parseNumber("1")); + storm::storage::SparseMatrix transitionMatrix = matrixBuilder.build(); + + storm::models::sparse::StateLabeling ap(3); + ap.addLabel("a"); + ap.addLabelToState("a", 2); + ap.addLabel("b"); + ap.addLabelToState("b", 0); + ap.addLabel("c"); + ap.addLabelToState("c", 0); + ap.addLabelToState("c", 2); + + mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); + + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); + + std::unique_ptr result = checker.check(this->env(), *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[0], this->precision()); + EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[1], this->precision()); + EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[2], this->precision()); + + formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]"); + + result = checker.check(this->env(), *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[0], this->precision()); + EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[1], this->precision()); + EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[2], this->precision()); + + formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"b\"]"); + + result = checker.check(this->env(), *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult3[0], this->precision()); + EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult3[1], this->precision()); + EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult3[2], this->precision()); + + formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"b\"]"); + + result = checker.check(this->env(), *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult4[0], this->precision()); + EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult4[1], this->precision()); + EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult4[2], this->precision()); + + formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"c\"]"); + + result = checker.check(this->env(), *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(this->parseNumber("2/3"), quantitativeResult5[0], this->precision()); + EXPECT_NEAR(this->parseNumber("2/3"), quantitativeResult5[1], this->precision()); + EXPECT_NEAR(this->parseNumber("2/3"), quantitativeResult5[2], this->precision()); + + formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"c\"]"); + + result = checker.check(this->env(), *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult6[0], this->precision()); + EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult6[1], this->precision()); + EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult6[2], this->precision()); + } } - { - matrixBuilder = storm::storage::SparseMatrixBuilder(2, 2, 4); - matrixBuilder.addNextValue(0, 0, .5); - matrixBuilder.addNextValue(0, 1, .5); - matrixBuilder.addNextValue(1, 0, .5); - matrixBuilder.addNextValue(1, 1, .5); - storm::storage::SparseMatrix transitionMatrix = matrixBuilder.build(); - - storm::models::sparse::StateLabeling ap(2); - ap.addLabel("a"); - ap.addLabelToState("a", 1); - - mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); - - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(.5, quantitativeResult1[1], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(.5, quantitativeResult2[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(.5, quantitativeResult2[1], storm::settings::getModule().getPrecision()); + + TYPED_TEST(LraMdpPrctlModelCheckerTest, LRA) { + typedef typename TestFixture::ValueType ValueType; + + storm::storage::SparseMatrixBuilder matrixBuilder; + std::shared_ptr> mdp; + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; + + { + matrixBuilder = storm::storage::SparseMatrixBuilder(4, 3, 4, true, true, 3); + matrixBuilder.newRowGroup(0); + matrixBuilder.addNextValue(0, 1, this->parseNumber("1")); + matrixBuilder.newRowGroup(1); + matrixBuilder.addNextValue(1, 1, this->parseNumber("1")); + matrixBuilder.addNextValue(2, 2, this->parseNumber("1")); + matrixBuilder.newRowGroup(3); + matrixBuilder.addNextValue(3, 2, this->parseNumber("1")); + storm::storage::SparseMatrix transitionMatrix = matrixBuilder.build(); + + storm::models::sparse::StateLabeling ap(3); + ap.addLabel("a"); + ap.addLabelToState("a", 0); + ap.addLabel("b"); + ap.addLabelToState("b", 1); + ap.addLabel("c"); + ap.addLabelToState("c", 2); + + mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); + + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); + + std::unique_ptr result = checker.check(this->env(), *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(this->parseNumber("0"), quantitativeResult1[0], this->precision()); + EXPECT_NEAR(this->parseNumber("0"), quantitativeResult1[1], this->precision()); + EXPECT_NEAR(this->parseNumber("0"), quantitativeResult1[2], this->precision()); + + formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]"); + + result = checker.check(this->env(), *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[0], this->precision()); + EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[1], this->precision()); + EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[2], this->precision()); + + formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"b\"]"); + + result = checker.check(this->env(), *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(this->parseNumber("1"), quantitativeResult3[0], this->precision()); + EXPECT_NEAR(this->parseNumber("1"), quantitativeResult3[1], this->precision()); + EXPECT_NEAR(this->parseNumber("0"), quantitativeResult3[2], this->precision()); + + formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"b\"]"); + + result = checker.check(this->env(), *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(this->parseNumber("0"), quantitativeResult4[0], this->precision()); + EXPECT_NEAR(this->parseNumber("0"), quantitativeResult4[1], this->precision()); + EXPECT_NEAR(this->parseNumber("0"), quantitativeResult4[2], this->precision()); + + formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"c\"]"); + + result = checker.check(this->env(), *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(this->parseNumber("1"), quantitativeResult5[0], this->precision()); + EXPECT_NEAR(this->parseNumber("1"), quantitativeResult5[1], this->precision()); + EXPECT_NEAR(this->parseNumber("1"), quantitativeResult5[2], this->precision()); + + formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"c\"]"); + + result = checker.check(this->env(), *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(this->parseNumber("0"), quantitativeResult6[0], this->precision()); + EXPECT_NEAR(this->parseNumber("0"), quantitativeResult6[1], this->precision()); + EXPECT_NEAR(this->parseNumber("1"), quantitativeResult6[2], this->precision()); + } + { + matrixBuilder = storm::storage::SparseMatrixBuilder(22, 15, 28, true, true, 15); + matrixBuilder.newRowGroup(0); + matrixBuilder.addNextValue(0, 1, this->parseNumber("1")); + matrixBuilder.newRowGroup(1); + matrixBuilder.addNextValue(1, 0, this->parseNumber("1")); + matrixBuilder.addNextValue(2, 2, this->parseNumber("1")); + matrixBuilder.addNextValue(3, 4, this->parseNumber("0.7")); + matrixBuilder.addNextValue(3, 6, this->parseNumber("0.3")); + matrixBuilder.newRowGroup(4); + matrixBuilder.addNextValue(4, 0, this->parseNumber("1")); + + matrixBuilder.newRowGroup(5); + matrixBuilder.addNextValue(5, 4, this->parseNumber("1")); + matrixBuilder.addNextValue(6, 5, this->parseNumber("0.8")); + matrixBuilder.addNextValue(6, 9, this->parseNumber("0.2")); + matrixBuilder.newRowGroup(7); + matrixBuilder.addNextValue(7, 3, this->parseNumber("1")); + matrixBuilder.addNextValue(8, 5, this->parseNumber("1")); + matrixBuilder.newRowGroup(9); + matrixBuilder.addNextValue(9, 3, this->parseNumber("1")); + + matrixBuilder.newRowGroup(10); + matrixBuilder.addNextValue(10, 7, this->parseNumber("1")); + matrixBuilder.newRowGroup(11); + matrixBuilder.addNextValue(11, 6, this->parseNumber("1")); + matrixBuilder.addNextValue(12, 8, this->parseNumber("1")); + matrixBuilder.newRowGroup(13); + matrixBuilder.addNextValue(13, 6, this->parseNumber("1")); + + matrixBuilder.newRowGroup(14); + matrixBuilder.addNextValue(14, 10, this->parseNumber("1")); + matrixBuilder.newRowGroup(15); + matrixBuilder.addNextValue(15, 9, this->parseNumber("1")); + matrixBuilder.addNextValue(16, 11, this->parseNumber("1")); + matrixBuilder.newRowGroup(17); + matrixBuilder.addNextValue(17, 9, this->parseNumber("1")); + + matrixBuilder.newRowGroup(18); + matrixBuilder.addNextValue(18, 5, this->parseNumber("0.4")); + matrixBuilder.addNextValue(18, 8, this->parseNumber("0.3")); + matrixBuilder.addNextValue(18, 11, this->parseNumber("0.3")); + + matrixBuilder.newRowGroup(19); + matrixBuilder.addNextValue(19, 7, this->parseNumber("0.7")); + matrixBuilder.addNextValue(19, 12, this->parseNumber("0.3")); + + matrixBuilder.newRowGroup(20); + matrixBuilder.addNextValue(20, 12, this->parseNumber("0.1")); + matrixBuilder.addNextValue(20, 13, this->parseNumber("0.9")); + matrixBuilder.addNextValue(21, 12, this->parseNumber("1")); + + storm::storage::SparseMatrix transitionMatrix = matrixBuilder.build(); + + storm::models::sparse::StateLabeling ap(15); + ap.addLabel("a"); + ap.addLabelToState("a", 1); + ap.addLabelToState("a", 4); + ap.addLabelToState("a", 5); + ap.addLabelToState("a", 7); + ap.addLabelToState("a", 11); + ap.addLabelToState("a", 13); + ap.addLabelToState("a", 14); + + mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); + + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); + + std::unique_ptr result = checker.check(this->env(), *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(this->parseNumber("37 / 60"), quantitativeResult1[0], this->precision()); + EXPECT_NEAR(this->parseNumber("2/3"), quantitativeResult1[3], this->precision()); + EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[6], this->precision()); + EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[9], this->precision()); + EXPECT_NEAR(this->parseNumber("31 / 60"), quantitativeResult1[12], this->precision()); + EXPECT_NEAR(this->parseNumber("101 / 200"), quantitativeResult1[13], this->precision()); + EXPECT_NEAR(this->parseNumber("31 / 60"), quantitativeResult1[14], this->precision()); + + formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]"); + + result = checker.check(this->env(), *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(this->parseNumber("0.1"), quantitativeResult2[0], this->precision()); + EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[3], this->precision()); + EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult2[6], this->precision()); + EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[9], this->precision()); + EXPECT_NEAR(this->parseNumber("0.1"), quantitativeResult2[12], this->precision()); + EXPECT_NEAR(this->parseNumber("79 / 300"), quantitativeResult2[13], this->precision()); + EXPECT_NEAR(this->parseNumber("0.1"), quantitativeResult2[14], this->precision()); + } } - { - matrixBuilder = storm::storage::SparseMatrixBuilder(4, 3, 4, true, true, 3); - matrixBuilder.newRowGroup(0); - matrixBuilder.addNextValue(0, 1, 1); - matrixBuilder.newRowGroup(1); - matrixBuilder.addNextValue(1, 0, 1); - matrixBuilder.addNextValue(2, 2, 1); - matrixBuilder.newRowGroup(3); - matrixBuilder.addNextValue(3, 0, 1); - storm::storage::SparseMatrix transitionMatrix = matrixBuilder.build(); - - storm::models::sparse::StateLabeling ap(3); - ap.addLabel("a"); - ap.addLabelToState("a", 2); - ap.addLabel("b"); - ap.addLabelToState("b", 0); - ap.addLabel("c"); - ap.addLabelToState("c", 0); - ap.addLabelToState("c", 2); - - mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); - - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1. / 3., quantitativeResult1[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1. / 3., quantitativeResult1[1], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1. / 3., quantitativeResult1[2], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0, quantitativeResult2[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0, quantitativeResult2[1], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0, quantitativeResult2[2], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"b\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.5, quantitativeResult3[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.5, quantitativeResult3[1], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.5, quantitativeResult3[2], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"b\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1. / 3., quantitativeResult4[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1. / 3., quantitativeResult4[1], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1. / 3., quantitativeResult4[2], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"c\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(2. / 3., quantitativeResult5[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(2. / 3., quantitativeResult5[1], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(2. / 3., quantitativeResult5[2], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"c\"]"); + + TYPED_TEST(LraMdpPrctlModelCheckerTest, cs_nfail) { + typedef typename TestFixture::ValueType ValueType; + + std::string formulasString = "R{\"grants\"}max=? [ MP ]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/cs_nfail3.nm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(184ul, model->getNumberOfStates()); + EXPECT_EQ(541ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); + auto mdp = model->template as>(); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); + std::unique_ptr result; + + result = checker.check(this->env(), tasks[0]); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(this->parseNumber("333/1000"), quantitativeResult[*mdp->getInitialStates().begin()], this->precision()); - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.5, quantitativeResult6[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.5, quantitativeResult6[1], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.5, quantitativeResult6[2], storm::settings::getModule().getPrecision()); - } -} - -TEST(LraMdpPrctlModelCheckerTest, LRA) { - storm::storage::SparseMatrixBuilder matrixBuilder; - std::shared_ptr> mdp; - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - { - matrixBuilder = storm::storage::SparseMatrixBuilder(4, 3, 4, true, true, 3); - matrixBuilder.newRowGroup(0); - matrixBuilder.addNextValue(0, 1, 1); - matrixBuilder.newRowGroup(1); - matrixBuilder.addNextValue(1, 1, 1); - matrixBuilder.addNextValue(2, 2, 1); - matrixBuilder.newRowGroup(3); - matrixBuilder.addNextValue(3, 2, 1); - storm::storage::SparseMatrix transitionMatrix = matrixBuilder.build(); - - storm::models::sparse::StateLabeling ap(3); - ap.addLabel("a"); - ap.addLabelToState("a", 0); - ap.addLabel("b"); - ap.addLabelToState("b", 1); - ap.addLabel("c"); - ap.addLabelToState("c", 2); - - mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); - - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0, quantitativeResult1[1], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0, quantitativeResult1[2], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0, quantitativeResult2[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0, quantitativeResult2[1], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0, quantitativeResult2[2], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"b\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0, quantitativeResult3[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0, quantitativeResult3[1], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0, quantitativeResult3[2], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"b\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0, quantitativeResult4[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0, quantitativeResult4[1], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0, quantitativeResult4[2], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"c\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0, quantitativeResult5[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0, quantitativeResult5[1], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0, quantitativeResult5[2], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"c\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0, quantitativeResult6[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0, quantitativeResult6[1], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0, quantitativeResult6[2], storm::settings::getModule().getPrecision()); } - { - matrixBuilder = storm::storage::SparseMatrixBuilder(22, 15, 28, true, true, 15); - matrixBuilder.newRowGroup(0); - matrixBuilder.addNextValue(0, 1, 1); - matrixBuilder.newRowGroup(1); - matrixBuilder.addNextValue(1, 0, 1); - matrixBuilder.addNextValue(2, 2, 1); - matrixBuilder.addNextValue(3, 4, 0.7); - matrixBuilder.addNextValue(3, 6, 0.3); - matrixBuilder.newRowGroup(4); - matrixBuilder.addNextValue(4, 0, 1); - - matrixBuilder.newRowGroup(5); - matrixBuilder.addNextValue(5, 4, 1); - matrixBuilder.addNextValue(6, 5, 0.8); - matrixBuilder.addNextValue(6, 9, 0.2); - matrixBuilder.newRowGroup(7); - matrixBuilder.addNextValue(7, 3, 1); - matrixBuilder.addNextValue(8, 5, 1); - matrixBuilder.newRowGroup(9); - matrixBuilder.addNextValue(9, 3, 1); - - matrixBuilder.newRowGroup(10); - matrixBuilder.addNextValue(10, 7, 1); - matrixBuilder.newRowGroup(11); - matrixBuilder.addNextValue(11, 6, 1); - matrixBuilder.addNextValue(12, 8, 1); - matrixBuilder.newRowGroup(13); - matrixBuilder.addNextValue(13, 6, 1); - - matrixBuilder.newRowGroup(14); - matrixBuilder.addNextValue(14, 10, 1); - matrixBuilder.newRowGroup(15); - matrixBuilder.addNextValue(15, 9, 1); - matrixBuilder.addNextValue(16, 11, 1); - matrixBuilder.newRowGroup(17); - matrixBuilder.addNextValue(17, 9, 1); - - matrixBuilder.newRowGroup(18); - matrixBuilder.addNextValue(18, 5, 0.4); - matrixBuilder.addNextValue(18, 8, 0.3); - matrixBuilder.addNextValue(18, 11, 0.3); - - matrixBuilder.newRowGroup(19); - matrixBuilder.addNextValue(19, 7, 0.7); - matrixBuilder.addNextValue(19, 12, 0.3); - - matrixBuilder.newRowGroup(20); - matrixBuilder.addNextValue(20, 12, 0.1); - matrixBuilder.addNextValue(20, 13, 0.9); - matrixBuilder.addNextValue(21, 12, 1); - storm::storage::SparseMatrix transitionMatrix = matrixBuilder.build(); - - storm::models::sparse::StateLabeling ap(15); - ap.addLabel("a"); - ap.addLabelToState("a", 1); - ap.addLabelToState("a", 4); - ap.addLabelToState("a", 5); - ap.addLabelToState("a", 7); - ap.addLabelToState("a", 11); - ap.addLabelToState("a", 13); - ap.addLabelToState("a", 14); - - mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); - - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(37. / 60., quantitativeResult1[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(2. / 3., quantitativeResult1[3], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.5, quantitativeResult1[6], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1. / 3., quantitativeResult1[9], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(31. / 60., quantitativeResult1[12], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(101. / 200., quantitativeResult1[13], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(31. / 60., quantitativeResult1[14], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.3 / 3., quantitativeResult2[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0, quantitativeResult2[3], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1. / 3., quantitativeResult2[6], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0, quantitativeResult2[9], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.3 / 3., quantitativeResult2[12], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(.79 / 3., quantitativeResult2[13], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.3 / 3., quantitativeResult2[14], storm::settings::getModule().getPrecision()); - } -} + +} \ No newline at end of file