From 1191e3068fff7ec6a710e1aeba5c7b680b257309 Mon Sep 17 00:00:00 2001 From: hannah Date: Fri, 16 Jul 2021 16:40:41 +0200 Subject: [PATCH] more ltl scheduler tests --- ...ulerGenerationMdpPrctlModelCheckerTest.cpp | 87 +++++++++++++++++-- 1 file changed, 78 insertions(+), 9 deletions(-) diff --git a/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp index 683cb14c7..e7ee44930 100755 --- a/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp @@ -208,7 +208,7 @@ namespace { typedef typename TestFixture::ValueType ValueType; // TODO skip without LTL support - std::string formulasString = "Pmax=? [X X \"target\"]; Pmin=? [G F \"target\"]; Pmax=? [(G F s>2) & (F G !(s=3))];"; + std::string formulasString = "Pmax=? [X X s=0]; Pmin=? [G F \"target\"]; Pmax=? [(G F s>2) & (F G !(s=3))];"; auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/scheduler_generation.nm", formulasString); auto mdp = std::move(modelFormulas.first); @@ -223,9 +223,11 @@ namespace { { auto result = checker.check(this->env(), tasks[0]); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(this->parseNumber("81/100"), result->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()],storm::settings::getModule().getPrecision()); ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult().hasScheduler()); storm::storage::Scheduler const &scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); + EXPECT_TRUE(scheduler.isDeterministicScheduler()); EXPECT_TRUE(!scheduler.isMemorylessScheduler()); EXPECT_TRUE(scheduler.isPartialScheduler()); @@ -238,11 +240,12 @@ namespace { storm::modelchecker::SparseMdpPrctlModelChecker> inducedChecker(*inducedMdp); auto inducedResult = inducedChecker.check(this->env(), tasks[0]); ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(this->parseNumber("9/10"), inducedResult->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()],storm::settings::getModule().getPrecision()); + EXPECT_NEAR(this->parseNumber("81/100"), inducedResult->template asExplicitQuantitativeCheckResult()[*inducedMdp->getInitialStates().begin()],storm::settings::getModule().getPrecision()); } { auto result = checker.check(this->env(), tasks[1]); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(this->parseNumber("1/2"), result->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()],storm::settings::getModule().getPrecision()); ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult().hasScheduler()); storm::storage::Scheduler const &scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); @@ -256,14 +259,14 @@ namespace { storm::modelchecker::SparseMdpPrctlModelChecker> inducedChecker( *inducedMdp); auto inducedResult = inducedChecker.check(this->env(), tasks[1]); ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(this->parseNumber("1/2"),inducedResult->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()],storm::settings::getModule().getPrecision()); + EXPECT_NEAR(this->parseNumber("1/2"),inducedResult->template asExplicitQuantitativeCheckResult()[*inducedMdp->getInitialStates().begin()],storm::settings::getModule().getPrecision()); } { auto result = checker.check(this->env(), tasks[2]); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); EXPECT_NEAR(this->parseNumber("1/2"), result->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], storm::settings::getModule().getPrecision()); - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult().hasScheduler()); storm::storage::Scheduler const &scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); @@ -279,14 +282,12 @@ namespace { auto inducedResult = inducedChecker.check(this->env(), tasks[2]); ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult()); EXPECT_NEAR(this->parseNumber("1/2"), - inducedResult->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], + inducedResult->template asExplicitQuantitativeCheckResult()[*inducedMdp->getInitialStates().begin()], storm::settings::getModule().getPrecision()); } - } - - TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, ltlMec) { + TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, ltlNondetChoice) { typedef typename TestFixture::ValueType ValueType; // TODO skip without LTL support // Nondeterministic choice in an accepting EC. @@ -305,6 +306,8 @@ namespace { { auto result = checker.check(this->env(), tasks[0]); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(this->parseNumber("0.5"),result->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], + storm::settings::getModule().getPrecision()); ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult().hasScheduler()); storm::storage::Scheduler const &scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); @@ -315,7 +318,7 @@ namespace { ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp); - auto const &inducedMdp = inducedModel->template as>(); // TODO DTMC! + auto const &inducedMdp = inducedModel->template as>(); EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates()); storm::modelchecker::SparseMdpPrctlModelChecker> inducedChecker(*inducedMdp); @@ -326,4 +329,70 @@ namespace { } + + TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, ltlUnsat) { + typedef typename TestFixture::ValueType ValueType; + // TODO skip without LTL support + // Nondeterministic choice in an accepting EC, Pmax unsatisfiable, Pmin tautology (compute 1-Pmax(!phi)) + std::string formulasString = "Pmax=? [(X X !(s=0)) & (X X (s=0))]; Pmin=? [(X X !(s=0)) | (X X (s=0))];"; + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/scheduler_generation.nm", formulasString); + + auto mdp = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(4ull, mdp->getNumberOfStates()); + EXPECT_EQ(11ull, mdp->getNumberOfTransitions()); + ASSERT_EQ(mdp->getType(), storm::models::ModelType::Mdp); + EXPECT_EQ(7ull, mdp->getNumberOfChoices()); + + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); + + { + auto result = checker.check(this->env(), tasks[0]); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(this->parseNumber("0"),result->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], + storm::settings::getModule().getPrecision()); + ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult().hasScheduler()); + storm::storage::Scheduler const &scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); + + EXPECT_TRUE(scheduler.isDeterministicScheduler()); + EXPECT_TRUE(scheduler.isMemorylessScheduler()); + EXPECT_TRUE(!scheduler.isPartialScheduler()); + auto inducedModel = mdp->applyScheduler(scheduler, true); + + ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp); + auto const &inducedMdp = inducedModel->template as>(); + EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates()); + + storm::modelchecker::SparseMdpPrctlModelChecker> inducedChecker(*inducedMdp); + auto inducedResult = inducedChecker.check(this->env(), tasks[0]); + ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(this->parseNumber("0"), inducedResult->template asExplicitQuantitativeCheckResult()[*inducedMdp->getInitialStates().begin()], storm::settings::getModule().getPrecision()); + } + + { + auto result = checker.check(this->env(), tasks[1]); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult().hasScheduler()); + EXPECT_NEAR(this->parseNumber("1"),result->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], + storm::settings::getModule().getPrecision()); + storm::storage::Scheduler const &scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); + + EXPECT_TRUE(scheduler.isDeterministicScheduler()); + EXPECT_TRUE(scheduler.isMemorylessScheduler()); + EXPECT_TRUE(!scheduler.isPartialScheduler()); + auto inducedModel = mdp->applyScheduler(scheduler, true); + + + ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp); + auto const &inducedMdp = inducedModel->template as>(); + EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates()); + + storm::modelchecker::SparseMdpPrctlModelChecker> inducedChecker(*inducedMdp); + auto inducedResult = inducedChecker.check(this->env(), tasks[1]); + ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(this->parseNumber("1"), inducedResult->template asExplicitQuantitativeCheckResult()[*inducedMdp->getInitialStates().begin()], storm::settings::getModule().getPrecision()); + } + + } + } \ No newline at end of file