From ebdfb2def84f6f3585dab4d9325de781af804a46 Mon Sep 17 00:00:00 2001 From: hannah Date: Thu, 29 Jul 2021 23:36:10 +0200 Subject: [PATCH] keep the original modeltype during product construction --- src/storm/storage/Scheduler.cpp | 2 +- .../SparseModelMemoryProduct.cpp | 10 +-- ...ulerGenerationMdpPrctlModelCheckerTest.cpp | 64 +++++++++---------- 3 files changed, 34 insertions(+), 42 deletions(-) diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp index 268fb3b0b..ff745ed09 100644 --- a/src/storm/storage/Scheduler.cpp +++ b/src/storm/storage/Scheduler.cpp @@ -95,7 +95,7 @@ namespace storm { dontCareStates[memoryState].set(modelState, true); ++numOfDontCareStates; - // Choices for unreachable states are not considered undefined or deterministic + // Choices for dontCare states are not considered undefined or deterministic if (!schedulerChoice.isDefined()) { --numOfUndefinedChoices; } else if (schedulerChoice.isDeterministic()) { diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp index fd9163fa5..b80910704 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp @@ -516,15 +516,7 @@ namespace storm { components.exitRates = std::move(resultExitRates); } - storm::models::ModelType resultType = model.getType(); - if (scheduler && !scheduler->isPartialScheduler()) { - if (model.isOfType(storm::models::ModelType::Mdp)) { - resultType = storm::models::ModelType::Dtmc; - } - // Note that converting deterministic MAs to CTMCs via state elimination does not preserve all properties (e.g. step bounded) - } - - return storm::utility::builder::buildModelFromComponents(resultType, std::move(components)); + return storm::utility::builder::buildModelFromComponents(model.getType(), std::move(components)); } template diff --git a/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp index 33f97bed2..63f4fd2d5 100755 --- a/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp @@ -235,17 +235,17 @@ namespace { EXPECT_TRUE(!scheduler.isPartialScheduler()); auto inducedModel = mdp->applyScheduler(scheduler); - ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Dtmc); - auto const &inducedDtmc = inducedModel->template as>(); - EXPECT_EQ(inducedDtmc->getNumberOfChoices(), inducedDtmc->getNumberOfStates()); + ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp); + auto const &inducedMdp = inducedModel->template as>(); + EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates()); - storm::modelchecker::SparseDtmcPrctlModelChecker> inducedChecker(*inducedDtmc); + storm::modelchecker::SparseMdpPrctlModelChecker> inducedChecker(*inducedMdp); auto inducedResult = inducedChecker.check(this->env(), tasks[0]); ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(this->parseNumber("81/100"), inducedResult->template asExplicitQuantitativeCheckResult()[*inducedDtmc->getInitialStates().begin()],storm::settings::getModule().getPrecision()); + EXPECT_NEAR(this->parseNumber("81/100"), inducedResult->template asExplicitQuantitativeCheckResult()[*inducedMdp->getInitialStates().begin()],storm::settings::getModule().getPrecision()); } { - tasks[1].setOnlyInitialStatesRelevant(false); + tasks[1].setOnlyInitialStatesRelevant(true); 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()); @@ -257,23 +257,21 @@ namespace { EXPECT_TRUE(!scheduler.isPartialScheduler()); auto inducedModel = mdp->applyScheduler(scheduler); - ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Dtmc); - auto const &inducedDtmc = inducedModel->template as>(); - EXPECT_EQ(inducedDtmc->getNumberOfChoices(), inducedDtmc->getNumberOfStates()); + ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp); + auto const &inducedMdp = inducedModel->template as>(); + EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates()); - storm::modelchecker::SparseDtmcPrctlModelChecker> inducedChecker(*inducedDtmc); + 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()[*inducedDtmc->getInitialStates().begin()],storm::settings::getModule().getPrecision()); - // TODO EXPECT_NEAR(this->parseNumber("1/2"),inducedResult->template asExplicitQuantitativeCheckResult()[*std::next(inducedDtmc->getInitialStates().begin())],storm::settings::getModule().getPrecision()); + + EXPECT_NEAR(this->parseNumber("1/2"),inducedResult->template asExplicitQuantitativeCheckResult()[*inducedMdp->getInitialStates().begin()],storm::settings::getModule().getPrecision()); } { - tasks[2].setOnlyInitialStatesRelevant(true); + tasks[2].setOnlyInitialStatesRelevant(false); 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()); + 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(); @@ -281,16 +279,19 @@ namespace { EXPECT_TRUE(!scheduler.isMemorylessScheduler()); EXPECT_TRUE(!scheduler.isPartialScheduler()); auto inducedModel = mdp->applyScheduler(scheduler); - ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Dtmc); - auto const &inducedDtmc = inducedModel->template as>(); - EXPECT_EQ(inducedDtmc->getNumberOfChoices(), inducedDtmc->getNumberOfStates()); - storm::modelchecker::SparseDtmcPrctlModelChecker> inducedChecker(*inducedDtmc); + 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[2]); ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(this->parseNumber("1/2"), - inducedResult->template asExplicitQuantitativeCheckResult()[*inducedDtmc->getInitialStates().begin()], - storm::settings::getModule().getPrecision()); + + auto test = inducedResult->template asExplicitQuantitativeCheckResult().getValueVector(); + EXPECT_NEAR(this->parseNumber("1/2"), inducedResult->template asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(this->parseNumber("1"), inducedResult->template asExplicitQuantitativeCheckResult()[1], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(this->parseNumber("0"), inducedResult->template asExplicitQuantitativeCheckResult()[2], storm::settings::getModule().getPrecision()); } #else GTEST_SKIP(); @@ -325,16 +326,16 @@ namespace { EXPECT_TRUE(scheduler.isDeterministicScheduler()); EXPECT_TRUE(!scheduler.isMemorylessScheduler()); EXPECT_TRUE(!scheduler.isPartialScheduler()); - auto inducedModel = mdp->applyScheduler(scheduler, true); + auto inducedModel = mdp->applyScheduler(scheduler); - ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Dtmc); - auto const &inducedDtmc = inducedModel->template as>(); - EXPECT_EQ(inducedDtmc->getNumberOfChoices(), inducedDtmc->getNumberOfStates()); + ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp); + auto const &inducedMdp = inducedModel->template as>(); + EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates()); - storm::modelchecker::SparseDtmcPrctlModelChecker> inducedChecker(*inducedDtmc); + storm::modelchecker::SparseMdpPrctlModelChecker> inducedChecker(*inducedMdp); auto inducedResult = inducedChecker.check(this->env(), tasks[0]); ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(this->parseNumber("1"), inducedResult->template asExplicitQuantitativeCheckResult()[*inducedDtmc->getInitialStates().begin()], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(this->parseNumber("1"), inducedResult->template asExplicitQuantitativeCheckResult()[*inducedMdp->getInitialStates().begin()], storm::settings::getModule().getPrecision()); } #else GTEST_SKIP(); @@ -371,9 +372,8 @@ namespace { EXPECT_TRUE(scheduler.isDeterministicScheduler()); EXPECT_TRUE(scheduler.isMemorylessScheduler()); EXPECT_TRUE(!scheduler.isPartialScheduler()); - auto inducedModel = mdp->applyScheduler(scheduler, true); + auto inducedModel = mdp->applyScheduler(scheduler); - // TODO not DTMC? ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp); auto const &inducedMdp = inducedModel->template as>(); EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates()); @@ -396,7 +396,7 @@ namespace { EXPECT_TRUE(scheduler.isDeterministicScheduler()); EXPECT_TRUE(scheduler.isMemorylessScheduler()); EXPECT_TRUE(!scheduler.isPartialScheduler()); - auto inducedModel = mdp->applyScheduler(scheduler, true); + auto inducedModel = mdp->applyScheduler(scheduler); ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp);