From 5149a7a9436387cd4fe9d9f0a5a9cc1d3d598de3 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 14 May 2013 15:01:01 +0200 Subject: [PATCH] Added lab files for asynch_leader and corrected pctl file a bit. Included first (incorrect) tests for performance test suite. --- examples/mdp/asynchronous_leader/leader.pctl | 6 +- .../GmmxxDtmcPrctModelCheckerTest.cpp | 116 ++++++++++ .../GmmxxMdpPrctModelCheckerTest.cpp | 217 ++++++++++++++++++ 3 files changed, 336 insertions(+), 3 deletions(-) create mode 100644 test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp create mode 100644 test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp diff --git a/examples/mdp/asynchronous_leader/leader.pctl b/examples/mdp/asynchronous_leader/leader.pctl index bb8fb1b82..2c87c7f27 100644 --- a/examples/mdp/asynchronous_leader/leader.pctl +++ b/examples/mdp/asynchronous_leader/leader.pctl @@ -1,8 +1,8 @@ Pmin=? [ F elected ] -const int K = 25; -Pmin=? [ F<=K elected ] -Pmax=? [ F<=K elected ] +// const int K = 25; +Pmin=? [ F<=25 elected ] +Pmax=? [ F<=25 elected ] Rmin=? [ F elected ] Rmax=? [ F elected ] diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp new file mode 100644 index 000000000..87bcf8ef6 --- /dev/null +++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp @@ -0,0 +1,116 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "src/utility/Settings.h" +#include "src/modelchecker/GmmxxDtmcPrctlModelChecker.h" +#include "src/parser/AutoParser.h" + +TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) { + storm::settings::Settings* s = storm::settings::instance(); + s->set("fix-deadlocks"); + storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", ""); + + ASSERT_EQ(parser.getType(), storm::models::DTMC); + + std::shared_ptr> dtmc = parser.getModel>(); + + ASSERT_EQ(dtmc->getNumberOfStates(), 8607u); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 22460u); + + storm::modelchecker::GmmxxDtmcPrctlModelChecker mc(*dtmc); + + storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("observe0Greater1"); + storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); + storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); + + std::vector* result = probFormula->check(mc); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 0.3328800375801578281), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("observeIGreater1"); + eventuallyFormula = new storm::property::prctl::Eventually(apFormula); + probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); + + result = probFormula->check(mc); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 0.1522173670950556501), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("observeOnlyTrueSender"); + eventuallyFormula = new storm::property::prctl::Eventually(apFormula); + probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); + + result = probFormula->check(mc); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 0.32153724292835045), s->get("precision")); + + delete probFormula; + delete result; +} + +/* +TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) { + storm::settings::Settings* s = storm::settings::instance(); + s->set("fix-deadlocks"); + storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.pick.trans.rew"); + + ASSERT_EQ(parser.getType(), storm::models::DTMC); + + std::shared_ptr> dtmc = parser.getModel>(); + + ASSERT_EQ(dtmc->getNumberOfStates(), 12400u); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 28894u); + + storm::modelchecker::GmmxxDtmcPrctlModelChecker mc(*dtmc); + + storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("elected"); + storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); + storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); + + std::vector* result = probFormula->check(mc); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 1), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("elected"); + storm::property::prctl::BoundedUntil* boundedUntilFormula = new storm::property::prctl::BoundedUntil(new storm::property::prctl::Ap("true"), apFormula, 20); + probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedUntilFormula); + + result = probFormula->check(mc); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 0.9999965911265462636), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("elected"); + storm::property::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); + storm::property::prctl::RewardNoBoundOperator* rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula); + + result = rewardFormula->check(mc); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 1.0448979591835938496), s->get("precision")); + + delete rewardFormula; + delete result; +} +*/ \ No newline at end of file diff --git a/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp new file mode 100644 index 000000000..322dafe8e --- /dev/null +++ b/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp @@ -0,0 +1,217 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "src/utility/Settings.h" +#include "src/modelchecker/GmmxxMdpPrctlModelChecker.h" +#include "src/parser/AutoParser.h" + +TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { + storm::settings::Settings* s = storm::settings::instance(); + storm::parser::AutoParser parser(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(parser.getType(), storm::models::MDP); + + std::shared_ptr> mdp = parser.getModel>(); + + ASSERT_EQ(mdp->getNumberOfStates(), 3172u); + ASSERT_EQ(mdp->getNumberOfTransitions(), 7144u); + + storm::modelchecker::GmmxxMdpPrctlModelChecker mc(*mdp); + + storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("elected"); + storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); + storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); + + std::vector* result = mc.checkNoBoundOperator(*probFormula); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 1), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("elected"); + eventuallyFormula = new storm::property::prctl::Eventually(apFormula); + probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); + + result = mc.checkNoBoundOperator(*probFormula); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 1), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("elected"); + storm::property::prctl::BoundedEventually* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 25); + probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, true); + + result = mc.checkNoBoundOperator(*probFormula); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("elected"); + boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 25); + probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, false); + + result = mc.checkNoBoundOperator(*probFormula); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("elected"); + storm::property::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); + storm::property::prctl::RewardNoBoundOperator* rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); + + result = mc.checkNoBoundOperator(*rewardFormula); + + ASSERT_LT(std::abs((*result)[0] - 4.28568908480604982), s->get("precision")); + + delete rewardFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("elected"); + reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); + rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); + + result = mc.checkNoBoundOperator(*rewardFormula);; + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 4.2856904354441400784), s->get("precision")); + + delete rewardFormula; + delete result; +} + +TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { + storm::settings::Settings* s = storm::settings::instance(); + storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_6.steps.state.rew", ""); + + ASSERT_EQ(parser.getType(), storm::models::MDP); + + std::shared_ptr> mdp = parser.getModel>(); + + storm::modelchecker::GmmxxMdpPrctlModelChecker mc(*mdp); + + storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("finished"); + storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); + storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); + + std::vector* result = mc.checkNoBoundOperator(*probFormula); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 1), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("finished"); + storm::property::prctl::Ap* apFormula2 = new storm::property::prctl::Ap("all_coins_equal_0"); + storm::property::prctl::And* andFormula = new storm::property::prctl::And(apFormula, apFormula2); + eventuallyFormula = new storm::property::prctl::Eventually(andFormula); + probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); + + result = mc.checkNoBoundOperator(*probFormula); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 1), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("finished"); + apFormula2 = new storm::property::prctl::Ap("all_coins_equal_1"); + andFormula = new storm::property::prctl::And(apFormula, apFormula2); + eventuallyFormula = new storm::property::prctl::Eventually(andFormula); + probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); + + result = mc.checkNoBoundOperator(*probFormula); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 1), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("finished"); + apFormula2 = new storm::property::prctl::Ap("agree"); + storm::property::prctl::Not* notFormula = new storm::property::prctl::Not(apFormula2); + andFormula = new storm::property::prctl::And(apFormula, notFormula); + eventuallyFormula = new storm::property::prctl::Eventually(andFormula); + probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); + + result = mc.checkNoBoundOperator(*probFormula); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 1), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("finished"); + storm::property::prctl::BoundedEventually* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 50); + probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, true); + + result = mc.checkNoBoundOperator(*probFormula); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("finished"); + boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 50); + probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, false); + + result = mc.checkNoBoundOperator(*probFormula); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("finished"); + storm::property::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); + storm::property::prctl::RewardNoBoundOperator* rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); + + result = mc.checkNoBoundOperator(*rewardFormula); + + ASSERT_LT(std::abs((*result)[0] - 4.28568908480604982), s->get("precision")); + + delete rewardFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("finished"); + reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); + rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); + + result = mc.checkNoBoundOperator(*rewardFormula);; + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 4.2856904354441400784), s->get("precision")); + + delete rewardFormula; + delete result; + +} \ No newline at end of file