diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp index c102b800b..bd782df1e 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp @@ -50,7 +50,7 @@ namespace storm { } // initialMemoryStates: Assign an initial memory state to each initial state of the model. - for (uint_fast64_t s0 : model.getInitialStates()) { + for (uint_fast64_t s0 : model.getInitialStates()) { // TODO should be relevantStates? memoryBuilder.setInitialMemoryState(s0, this->_memoryInitialStates.get()[s0]); } diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp index f834434ca..8b8431e24 100644 --- a/src/storm/storage/Scheduler.cpp +++ b/src/storm/storage/Scheduler.cpp @@ -145,7 +145,7 @@ namespace storm { } out << ":" << std::endl; STORM_LOG_WARN_COND(!(skipUniqueChoices && model == nullptr), "Can not skip unique choices if the model is not given."); - out << std::setw(widthOfStates) << "model state:" << " " << (isMemorylessScheduler() ? "" : " memory: ") << "choice(s)" << std::endl; + out << std::setw(widthOfStates) << "model state:" << " " << (isMemorylessScheduler() ? "" : " memory: ") << "choice(s)" << (isMemorylessScheduler() ? "" : " memory updates: ") << std::endl; for (uint_fast64_t state = 0; state < schedulerChoices.front().size(); ++state) { std::stringstream stateString; // Check whether the state is skipped @@ -215,11 +215,12 @@ namespace storm { stateString << "undefined."; } + // Print memory updates if(!isMemorylessScheduler()) { - stateString << " "; + out << " "; for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) { for (auto entryIt = model->getTransitionMatrix().getRow(state + choiceProbPair.first).begin(); entryIt < model->getTransitionMatrix().getRow(state + choiceProbPair.first).end(); ++entryIt) { - out << ", model state' = " << entryIt->getColumn() << ": (transition = " << state+choiceProbPair.first << ") -> " << "(m' = "<memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")"; + out << ", model state' = " << entryIt->getColumn() << ": (transition = " << entryIt - model->getTransitionMatrix().begin() << ") -> " << "(m' = "<memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")"; } } @@ -227,7 +228,6 @@ namespace storm { stateString << std::endl; } - // Todo: print memory updates out << stateString.str(); out << std::endl; } diff --git a/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp index dd8846f74..ba1e350dd 100755 --- a/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp @@ -204,10 +204,10 @@ namespace { } - TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, ltl) { 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))];"; auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/scheduler_generation.nm", formulasString); @@ -238,11 +238,8 @@ 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()], //TODO other states, too - storm::settings::getModule().getPrecision()); + EXPECT_NEAR(this->parseNumber("9/10"), inducedResult->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()],storm::settings::getModule().getPrecision()); } - { auto result = checker.check(this->env(), tasks[1]); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); @@ -256,15 +253,11 @@ namespace { 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); + 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()[*mdp->getInitialStates().begin()],storm::settings::getModule().getPrecision()); } - { auto result = checker.check(this->env(), tasks[2]); EXPECT_NEAR(this->parseNumber("1/2"), @@ -293,11 +286,10 @@ namespace { } - TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, ltl2) { + TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, ltlMec) { typedef typename TestFixture::ValueType ValueType; - //TODO find noMEC-scheduler-error (need nondet in EC) - - // Todo unreachable Product state error + // TODO skip without LTL support + // Nondeterministic choice in an accepting EC. std::string formulasString = "Pmax=? [X X !(x=0)];"; auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/prism-mec-example1.nm", formulasString); @@ -329,7 +321,7 @@ namespace { storm::modelchecker::SparseMdpPrctlModelChecker> inducedChecker(*inducedMdp); auto inducedResult = inducedChecker.check(this->env(), tasks[0]); ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult()); - // EXPECT_NEAR(this->parseNumber("todo"), inducedResult->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(this->parseNumber("0.5"), inducedResult->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], storm::settings::getModule().getPrecision()); } }