diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp index 8a59e5252..07940e3a7 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp @@ -71,9 +71,11 @@ namespace storm { uint_fast64_t memoryState = choice.first.second; scheduler.setChoice(choice.second, modelState, memoryState); } + // TODO set non-reachable (modelState,memoryState)-Pairs (i.e. those that are not contained in _productChoices) to "unreachable", (extend Scheduler by something like std::vector> reachableSchedulerChoices; und isChoiceReachable(..)) return scheduler; } + template std::map SparseLTLHelper::computeApSets(std::map> const& extracted, std::function(std::shared_ptr const& formula)> formulaChecker){ std::map apSets; @@ -191,8 +193,6 @@ namespace storm { STORM_LOG_DEBUG("MEC is accepting"); for (auto const& stateChoicePair : mec) { - // TODO extend scheduler by mec choices (which?) - // need adversary which forces (to remain in mec and) to visit all states of the mec inf. often with prob. 1 acceptingStates.set(stateChoicePair.first); } } @@ -339,7 +339,7 @@ namespace storm { storm::storage::BitVector modelStates(this->_transitionMatrix.getRowGroupCount(), false); for (storm::storage::sparse::state_type modelState = 0; modelState < this->_transitionMatrix.getRowGroupCount(); ++modelState) { - if (goalState == productBuilder.getSuccessor(modelState, startState, modelState)) { + if (goalState == productBuilder.getSuccessor(modelState, startState, modelState)) { //todo remove first parameter modelStates.set(modelState); } } diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h index 3df887979..0e7277b54 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h @@ -96,11 +96,15 @@ namespace storm { storm::storage::SparseMatrix const& _transitionMatrix; std::size_t _numberOfStates; //TODO just use _transitionMatrix.getRowGroupCount instead? - // scheduler + // REACH scheduler boost::optional, storm::storage::SchedulerChoice>> _productChoices; // --> choice - boost::optional>> _memoryTransitions; // BitVector contains the model states that lead from startState to goalSate of teh DA + boost::optional>> _memoryTransitions; // BitVector contains the model states that lead from startState to goalSate of the DA boost::optional> _memoryInitialStates; // Saves for each modelState which automaton state is reached from the initial state //TODO improve + // MEC scheduler + boost::optional> , storm::storage::SchedulerChoice>> _mecProductChoices; // <#literal, > ---> choice + boost::optional>> _mecMemoryTransitions; // BitVector contains the model states that lead from #INF(i) to #INF(i+1) of the AccCondition (#INF(1) AND #INF(2) ....) OR (..) + }; } } diff --git a/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp index a1844888b..45362994a 100755 --- a/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp @@ -206,7 +206,7 @@ namespace { TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, ltl) { typedef typename TestFixture::ValueType ValueType; - std::string formulasString = "Pmax=? [X X \"target\"]; Pmin=? [G F \"target\"];"; + std::string formulasString = "Pmax=? [X X \"target\"]; 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); auto tasks = this->getTasks(modelFormulas.second); @@ -228,7 +228,7 @@ namespace { EXPECT_TRUE(scheduler.isPartialScheduler()); auto inducedModel = mdp->applyScheduler(scheduler); ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp); - auto const& inducedMdp = inducedModel->template as>(); + auto const& inducedMdp = inducedModel->template as>(); // TODO DTMC! EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates()); storm::modelchecker::SparseMdpPrctlModelChecker> inducedChecker(*inducedMdp); auto inducedResult = inducedChecker.check(this->env(), tasks[0]); @@ -253,6 +253,26 @@ namespace { ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult()); EXPECT_NEAR(this->parseNumber("1/2"), inducedResult->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], storm::settings::getModule().getPrecision()); } + { + auto result = checker.check(this->env(), tasks[2]); + 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(); + + EXPECT_TRUE(scheduler.isDeterministicScheduler()); + EXPECT_TRUE(!scheduler.isMemorylessScheduler()); + EXPECT_TRUE(scheduler.isPartialScheduler()); + auto inducedModel = mdp->applyScheduler(scheduler); + 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()[*mdp->getInitialStates().begin()], storm::settings::getModule().getPrecision()); + } } } \ No newline at end of file