From bdf415d41607b10b4d93a69bba4bf7adefe32e9f Mon Sep 17 00:00:00 2001 From: PBerger Date: Wed, 14 Sep 2016 13:43:26 +0200 Subject: [PATCH] Added fancy tests. Former-commit-id: 09605531124533dddb362a73492c4d45fae65a79 --- .../GameBasedDtmcModelCheckerTest.cpp | 285 ++++++++++++++++++ .../GameBasedMdpModelCheckerTest.cpp | 143 +++++++++ 2 files changed, 428 insertions(+) create mode 100644 test/functional/modelchecker/GameBasedDtmcModelCheckerTest.cpp create mode 100644 test/functional/modelchecker/GameBasedMdpModelCheckerTest.cpp diff --git a/test/functional/modelchecker/GameBasedDtmcModelCheckerTest.cpp b/test/functional/modelchecker/GameBasedDtmcModelCheckerTest.cpp new file mode 100644 index 000000000..0485ef9f1 --- /dev/null +++ b/test/functional/modelchecker/GameBasedDtmcModelCheckerTest.cpp @@ -0,0 +1,285 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "src/parser/FormulaParser.h" +#include "src/logic/Formulas.h" +#include "src/utility/solver.h" +#include "src/modelchecker/abstraction/GameBasedMdpModelChecker.h" +#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "src/parser/PrismParser.h" +#include "src/builder/DdPrismModelBuilder.h" +#include "src/models/symbolic/StandardRewardModel.h" +#include "src/models/symbolic/Dtmc.h" +#include "src/settings/SettingsManager.h" + +#include "src/settings/modules/NativeEquationSolverSettings.h" + +#include "src/settings/modules/GeneralSettings.h" + +TEST(GameBasedDtmcModelCheckerTest, Die_Cudd) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + + // 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 + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); + EXPECT_EQ(13ul, model->getNumberOfStates()); + EXPECT_EQ(20ul, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); + + std::shared_ptr> dtmc = model->as>(); + auto checker = std::make_shared>>(program); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); + storm::modelchecker::CheckTask task(*formula, true); + + std::unique_ptr result = checker->check(task); + //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1.0/6.0, quantitativeResult1[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); + task = storm::modelchecker::CheckTask(*formula, true); + + result = checker->check(task); + //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1.0/6.0, quantitativeResult2[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); + task = storm::modelchecker::CheckTask(*formula, true); + + result = checker->check(task); + //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1.0/6.0, quantitativeResult3[0], storm::settings::getModule().getPrecision()); +} + +TEST(GameBasedDtmcModelCheckerTest, Die_Sylvan) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + + // 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 + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); + EXPECT_EQ(13ul, model->getNumberOfStates()); + EXPECT_EQ(20ul, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); + + std::shared_ptr> dtmc = model->as>(); + auto checker = std::make_shared>>(program); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); + storm::modelchecker::CheckTask task(*formula, true); + + std::unique_ptr result = checker->check(task); + //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1.0/6.0, quantitativeResult1[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); + task = storm::modelchecker::CheckTask(*formula, true); + + result = checker->check(task); + //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1.0/6.0, quantitativeResult2[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); + task = storm::modelchecker::CheckTask(*formula, true); + + result = checker->check(task); + //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1.0/6.0, quantitativeResult3[0], storm::settings::getModule().getPrecision()); +} + +TEST(GameBasedDtmcModelCheckerTest, Crowds_Cudd) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; + + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); + EXPECT_EQ(8607ul, model->getNumberOfStates()); + EXPECT_EQ(15113ul, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); + + std::shared_ptr> dtmc = model->as>(); + auto checker = std::make_shared>>(program); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); + storm::modelchecker::CheckTask task(*formula, true); + + std::unique_ptr result = checker->check(task); + //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.33288236360191303, quantitativeResult1[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]"); + task = storm::modelchecker::CheckTask(*formula, true); + + result = checker->check(task); + //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.15222081144084315, quantitativeResult2[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]"); + task = storm::modelchecker::CheckTask(*formula, true); + + result = checker->check(task); + //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.3215392962289586, quantitativeResult3[0], storm::settings::getModule().getPrecision()); +} + +TEST(GameBasedDtmcModelCheckerTest, Crowds_Sylvan) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; + + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); + EXPECT_EQ(8607ul, model->getNumberOfStates()); + EXPECT_EQ(15113ul, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); + + std::shared_ptr> dtmc = model->as>(); + auto checker = std::make_shared>>(program); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); + storm::modelchecker::CheckTask task(*formula, true); + + std::unique_ptr result = checker->check(task); + //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + // FIXME: precision not optimal. + EXPECT_NEAR(0.33288236360191303, quantitativeResult1[0], 10 * storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]"); + task = storm::modelchecker::CheckTask(*formula, true); + + result = checker->check(task); + //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + + // FIXME: precision not optimal. + EXPECT_NEAR(0.15222081144084315, quantitativeResult2[0], 10 * storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]"); + task = storm::modelchecker::CheckTask(*formula, true); + + result = checker->check(task); + //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); + + // FIXME: precision not optimal. + EXPECT_NEAR(0.3215392962289586, quantitativeResult3[0], 10 * storm::settings::getModule().getPrecision()); +} + +TEST(GameBasedDtmcModelCheckerTest, SynchronousLeader_Cudd) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + + // 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 + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); + EXPECT_EQ(273ul, model->getNumberOfStates()); + EXPECT_EQ(397ul, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); + + std::shared_ptr> dtmc = model->as>(); + auto checker = std::make_shared>>(program); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); + storm::modelchecker::CheckTask task(*formula, true); + + std::unique_ptr result = checker->check(task); + //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]"); + task = storm::modelchecker::CheckTask(*formula, true); + + result = checker->check(task); + //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.99999989760000074, quantitativeResult2[0], storm::settings::getModule().getPrecision()); +} + +TEST(GameBasedDtmcModelCheckerTest, SynchronousLeader_Sylvan) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + + // 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 + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); + EXPECT_EQ(273ul, model->getNumberOfStates()); + EXPECT_EQ(397ul, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); + + std::shared_ptr> dtmc = model->as>(); + auto checker = std::make_shared>>(program); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); + storm::modelchecker::CheckTask task(*formula, true); + + std::unique_ptr result = checker->check(task); + //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]"); + task = storm::modelchecker::CheckTask(*formula, true); + + result = checker->check(task); + //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.99999989760000074, quantitativeResult2[0], storm::settings::getModule().getPrecision()); +} diff --git a/test/functional/modelchecker/GameBasedMdpModelCheckerTest.cpp b/test/functional/modelchecker/GameBasedMdpModelCheckerTest.cpp new file mode 100644 index 000000000..ff07a208a --- /dev/null +++ b/test/functional/modelchecker/GameBasedMdpModelCheckerTest.cpp @@ -0,0 +1,143 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "src/parser/FormulaParser.h" +#include "src/logic/Formulas.h" +#include "src/models/sparse/StandardRewardModel.h" +#include "src/models/sparse/Model.h" +#include "src/modelchecker/abstraction/GameBasedMdpModelChecker.h" +#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" + +#include "src/parser/AutoParser.h" +#include "src/parser/PrismParser.h" + +#include "utility/storm.h" + +TEST(GameBasedMdpModelCheckerTest, Dice_Cudd) { + std::string programFile = STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.nm"; + std::string formulaFile = STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.prctl"; + + storm::prism::Program program = storm::parseProgram(programFile); + + // Build the die model +#ifdef WINDOWS + storm::builder::DdPrismModelBuilder::Options options; +#else + typename storm::builder::DdPrismModelBuilder::Options options; +#endif + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); + + ASSERT_EQ(model->getNumberOfStates(), 169ull); + ASSERT_EQ(model->getNumberOfTransitions(), 436ull); + + std::shared_ptr> mdp = model->as>(); + auto mdpModelchecker = std::make_shared>>(program); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); + storm::modelchecker::CheckTask task(*formula, true); + + std::unique_ptr result = mdpModelchecker->check(task); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.0277777612209320068, quantitativeResult1[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); + task = storm::modelchecker::CheckTask(*formula, true); + + result = mdpModelchecker->check(task); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.0277777612209320068, quantitativeResult2[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); + task = storm::modelchecker::CheckTask(*formula, true); + + result = mdpModelchecker->check(task); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.0555555224418640136, quantitativeResult3[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); + task = storm::modelchecker::CheckTask(*formula, true); + + result = mdpModelchecker->check(task); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.0555555224418640136, quantitativeResult4[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); + task = storm::modelchecker::CheckTask(*formula, true); + + result = mdpModelchecker->check(task); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.083333283662796020508, quantitativeResult5[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); + task = storm::modelchecker::CheckTask(*formula, true); + + result = mdpModelchecker->check(task); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.083333283662796020508, quantitativeResult6[0], storm::settings::getModule().getPrecision()); +} + +TEST(GameBasedMdpModelCheckerTest, AsynchronousLeader_Cudd) { + std::string programFile = STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.nm"; + std::string formulaFile = STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader.prctl"; + + storm::prism::Program program = storm::parseProgram(programFile); + // Build the die model +#ifdef WINDOWS + storm::builder::DdPrismModelBuilder::Options options; +#else + typename storm::builder::DdPrismModelBuilder::Options options; +#endif + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); + + ASSERT_EQ(3172ull, model->getNumberOfStates()); + ASSERT_EQ(7144ull, model->getNumberOfTransitions()); + + std::shared_ptr> mdp = model->as>(); + auto mdpModelchecker = std::make_shared>>(program); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); + storm::modelchecker::CheckTask task(*formula, true); + + std::unique_ptr result = mdpModelchecker->check(task); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1, quantitativeResult1[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); + task = storm::modelchecker::CheckTask(*formula, true); + + result = mdpModelchecker->check(task); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1, quantitativeResult2[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); + task = storm::modelchecker::CheckTask(*formula, true); + + result = mdpModelchecker->check(task); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.0625, quantitativeResult3[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); + task = storm::modelchecker::CheckTask(*formula, true); + + result = mdpModelchecker->check(task); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.0625, quantitativeResult4[0], storm::settings::getModule().getPrecision()); +}