diff --git a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp index 7999da353..1e131c335 100644 --- a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp @@ -13,6 +13,8 @@ #include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/settings/SettingMemento.h" #include "src/parser/AutoParser.h" +#include "src/parser/PrismParser.h" +#include "src/builder/ExplicitPrismModelBuilder.h" TEST(GmmxxDtmcPrctlModelCheckerTest, Die) { std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.coin_flips.trans.rew"); @@ -214,7 +216,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) { TEST(GmmxxDtmcPrctlModelCheckerTest, LRA) { storm::storage::SparseMatrixBuilder matrixBuilder; - std::shared_ptr> mdp; + std::shared_ptr> dtmc; // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -260,9 +262,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRA) { ap.addLabelToState("a", 13); ap.addLabelToState("a", 14); - mdp.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap)); + dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap)); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); @@ -278,3 +280,42 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRA) { EXPECT_NEAR(0.3 / 3., quantitativeResult1[14], storm::settings::nativeEquationSolverSettings().getPrecision()); } } + +TEST(GmmxxDtmcPrctlModelCheckerTest, Conditional) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/test_conditional.pm"); + + std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder().translateProgram(program); + ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc); + ASSERT_EQ(4ul, model->getNumberOfStates()); + ASSERT_EQ(5ul, model->getNumberOfTransitions()); + + std::shared_ptr> dtmc = model->as>(); + + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"target\"]"); + + std::unique_ptr result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(0.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"target\" || F \"condition\"]"); + + result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(storm::utility::one(), quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("R=? [F \"target\"]"); + + result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); + EXPECT_EQ(storm::utility::infinity(), quantitativeResult3[0]); + + formula = formulaParser.parseSingleFormulaFromString("R=? [F \"target\" || F \"condition\"]"); + + result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(storm::utility::one(), quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision()); +} diff --git a/test/functional/modelchecker/test_conditional.pm b/test/functional/modelchecker/test_conditional.pm new file mode 100644 index 000000000..57b8ba44c --- /dev/null +++ b/test/functional/modelchecker/test_conditional.pm @@ -0,0 +1,18 @@ +dtmc + +module test + s : [0 .. 3] init 0; + + [] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2); + [] s=1 -> 1 : true; + [] s=2 -> 1 : (s'=3); + [] s=3 -> 1 : true; + +endmodule + +rewards + s=2 : 1; +endrewards + +label "condition" = s=2; +label "target" = s=3;