sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

keep the original modeltype during product construction

tempestpy_adaptions
hannah 3 years ago
committed by Stefan Pranger
parent
c80a62ce06
commit
ebdfb2def8
3 changed files with 34 additions and 42 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      src/storm/storage/Scheduler.cpp
  2. 10
      src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp
  3. 64
      src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp

2
src/storm/storage/Scheduler.cpp
View File

@ -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()) {

10
src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp
View File

@ -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 <typename ValueType, typename RewardModelType>

64
src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp
View File

@ -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<storm::models::sparse::Dtmc<ValueType>>();
EXPECT_EQ(inducedDtmc->getNumberOfChoices(), inducedDtmc->getNumberOfStates());
ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp);
auto const &inducedMdp = inducedModel->template as<storm::models::sparse::Mdp<ValueType>>();
EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates());
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> inducedChecker(*inducedDtmc);
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> inducedChecker(*inducedMdp);
auto inducedResult = inducedChecker.check(this->env(), tasks[0]);
ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
EXPECT_NEAR(this->parseNumber("81/100"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedDtmc->getInitialStates().begin()],storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(this->parseNumber("81/100"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedMdp->getInitialStates().begin()],storm::settings::getModule<storm::settings::modules::GeneralSettings>().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<ValueType>()[*mdp->getInitialStates().begin()],storm::settings::getModule<storm::settings::modules::GeneralSettings>().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<storm::models::sparse::Dtmc<ValueType>>();
EXPECT_EQ(inducedDtmc->getNumberOfChoices(), inducedDtmc->getNumberOfStates());
ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp);
auto const &inducedMdp = inducedModel->template as<storm::models::sparse::Mdp<ValueType>>();
EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates());
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> inducedChecker(*inducedDtmc);
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> inducedChecker(*inducedMdp);
auto inducedResult = inducedChecker.check(this->env(), tasks[1]);
ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
EXPECT_NEAR(this->parseNumber("1/2"),inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedDtmc->getInitialStates().begin()],storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
// TODO EXPECT_NEAR(this->parseNumber("1/2"),inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*std::next(inducedDtmc->getInitialStates().begin())],storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(this->parseNumber("1/2"),inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedMdp->getInitialStates().begin()],storm::settings::getModule<storm::settings::modules::GeneralSettings>().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<ValueType>()[*mdp->getInitialStates().begin()],
storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(this->parseNumber("1/2"), result->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
storm::storage::Scheduler<ValueType> const &scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().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<storm::models::sparse::Dtmc<ValueType>>();
EXPECT_EQ(inducedDtmc->getNumberOfChoices(), inducedDtmc->getNumberOfStates());
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> inducedChecker(*inducedDtmc);
ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp);
auto const &inducedMdp = inducedModel->template as<storm::models::sparse::Mdp<ValueType>>();
EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates());
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> inducedChecker(*inducedMdp);
auto inducedResult = inducedChecker.check(this->env(), tasks[2]);
ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
EXPECT_NEAR(this->parseNumber("1/2"),
inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedDtmc->getInitialStates().begin()],
storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
auto test = inducedResult->template asExplicitQuantitativeCheckResult<ValueType>().getValueVector();
EXPECT_NEAR(this->parseNumber("1/2"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(this->parseNumber("1"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[1], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(this->parseNumber("0"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[2], storm::settings::getModule<storm::settings::modules::GeneralSettings>().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<storm::models::sparse::Dtmc<ValueType>>();
EXPECT_EQ(inducedDtmc->getNumberOfChoices(), inducedDtmc->getNumberOfStates());
ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp);
auto const &inducedMdp = inducedModel->template as<storm::models::sparse::Mdp<ValueType>>();
EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates());
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> inducedChecker(*inducedDtmc);
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> inducedChecker(*inducedMdp);
auto inducedResult = inducedChecker.check(this->env(), tasks[0]);
ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
EXPECT_NEAR(this->parseNumber("1"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedDtmc->getInitialStates().begin()], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(this->parseNumber("1"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedMdp->getInitialStates().begin()], storm::settings::getModule<storm::settings::modules::GeneralSettings>().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<storm::models::sparse::Mdp<ValueType>>();
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);

Write Preview
Loading…
Cancel
Save