From 7376eaf8669057127c3477de7ee867c18604141d Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 7 Dec 2015 10:52:12 +0100 Subject: [PATCH] made symbolic MDP model checker tests work Former-commit-id: e2e0d07a5572ec5aff359d410f600c5968aa7f4b --- .../prctl/SymbolicMdpPrctlModelChecker.cpp | 1 + .../prctl/helper/SymbolicMdpPrctlHelper.cpp | 1 + .../SymbolicMinMaxLinearEquationSolver.cpp | 3 +- src/utility/solver.cpp | 1 + .../SymbolicMdpPrctlModelCheckerTest.cpp | 182 +++++++++++++++++- 5 files changed, 185 insertions(+), 3 deletions(-) diff --git a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp index f1db016ec..7924cfada 100644 --- a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp @@ -91,5 +91,6 @@ namespace storm { } template class SymbolicMdpPrctlModelChecker; + template class SymbolicMdpPrctlModelChecker; } } diff --git a/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp index a9ce5d7fb..9f78545e4 100644 --- a/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp @@ -200,6 +200,7 @@ namespace storm { } template class SymbolicMdpPrctlHelper; + template class SymbolicMdpPrctlHelper; } } } \ No newline at end of file diff --git a/src/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/solver/SymbolicMinMaxLinearEquationSolver.cpp index bffbfcb48..2821fad19 100644 --- a/src/solver/SymbolicMinMaxLinearEquationSolver.cpp +++ b/src/solver/SymbolicMinMaxLinearEquationSolver.cpp @@ -61,7 +61,7 @@ namespace storm { ++iterations; } - + return xCopy; } @@ -91,6 +91,7 @@ namespace storm { } template class SymbolicMinMaxLinearEquationSolver; + template class SymbolicMinMaxLinearEquationSolver; } } diff --git a/src/utility/solver.cpp b/src/utility/solver.cpp index 0c1e10278..42195cde3 100644 --- a/src/utility/solver.cpp +++ b/src/utility/solver.cpp @@ -191,6 +191,7 @@ namespace storm { template class SymbolicLinearEquationSolverFactory; template class SymbolicLinearEquationSolverFactory; template class SymbolicMinMaxLinearEquationSolverFactory; + template class SymbolicMinMaxLinearEquationSolverFactory; template class SymbolicGameSolverFactory; template class SymbolicGameSolverFactory; template class LinearEquationSolverFactory; diff --git a/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp index 7cdf9ef25..cb33cea0f 100644 --- a/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp @@ -17,7 +17,7 @@ #include "src/settings/modules/GeneralSettings.h" -TEST(SymbolicMdpPrctlModelCheckerTest, Dice) { +TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Cudd) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); // A parser that we use for conveniently constructing the formulas. @@ -114,7 +114,104 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice) { EXPECT_NEAR(7.3333272933959961, quantitativeResult8.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); } -TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader) { +TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Sylvan) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; + + // Build the die model with its reward model. +#ifdef WINDOWS + storm::builder::DdPrismModelBuilder::Options options; +#else + typename storm::builder::DdPrismModelBuilder::Options options; +#endif + options.buildAllRewardModels = false; + options.rewardModelsToBuild.insert("coinflips"); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); + EXPECT_EQ(169ul, model->getNumberOfStates()); + EXPECT_EQ(436ul, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); + + std::shared_ptr> mdp = model->as>(); + + storm::modelchecker::SymbolicMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory())); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); + + std::unique_ptr result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult6 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult7 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(7.3333272933959961, quantitativeResult7.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(7.3333272933959961, quantitativeResult7.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult8 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(7.3333272933959961, quantitativeResult8.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(7.3333272933959961, quantitativeResult8.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); +} + +TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); // A parser that we use for conveniently constructing the formulas. @@ -192,3 +289,84 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader) { EXPECT_NEAR(4.2856890848060498, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(4.2856890848060498, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); } + +TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; + + // Build the die model with its reward model. +#ifdef WINDOWS + storm::builder::DdPrismModelBuilder::Options options; +#else + typename storm::builder::DdPrismModelBuilder::Options options; +#endif + options.buildAllRewardModels = false; + options.rewardModelsToBuild.insert("rounds"); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); + EXPECT_EQ(3172ul, model->getNumberOfStates()); + EXPECT_EQ(7144ul, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); + + std::shared_ptr> mdp = model->as>(); + + storm::modelchecker::SymbolicMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory())); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); + + std::unique_ptr result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(0.0625, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.0625, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.0625, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult(); + + // FIXME: this precision bound is not really good. + EXPECT_NEAR(4.2857, quantitativeResult5.getMin(), 100 * storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(4.2857, quantitativeResult5.getMax(), 100 * storm::settings::nativeEquationSolverSettings().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult6 = result->asSymbolicQuantitativeCheckResult(); + + // FIXME: this precision bound is not really good. + EXPECT_NEAR(4.2857, quantitativeResult6.getMin(), 100 * storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(4.2857, quantitativeResult6.getMax(), 100 * storm::settings::nativeEquationSolverSettings().getPrecision()); +} \ No newline at end of file