new Test

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<std::Bitvector>> reachableSchedulerChoices; und isChoiceReachable(..))
 
                 return scheduler;
             }
+
             template<typename ValueType, bool Nondeterministic>
             std::map<std::string, storm::storage::BitVector> SparseLTLHelper<ValueType, Nondeterministic>::computeApSets(std::map<std::string, std::shared_ptr<storm::logic::Formula const>> const& extracted, std::function<std::unique_ptr<CheckResult>(std::shared_ptr<storm::logic::Formula const> const& formula)> formulaChecker){
                 std::map<std::string, storm::storage::BitVector> 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);
                                     }
                                 }

src/storm/modelchecker/helper/ltl/SparseLTLHelper.h

@@ -96,11 +96,15 @@ namespace storm {
                 storm::storage::SparseMatrix<ValueType> const& _transitionMatrix;
                 std::size_t _numberOfStates;  //TODO just use _transitionMatrix.getRowGroupCount instead?
 
-                // scheduler
+                // REACH scheduler
                 boost::optional<std::map<std::pair<uint_fast64_t, uint_fast64_t>, storm::storage::SchedulerChoice<ValueType>>> _productChoices;   // <s, q> --> choice
-                boost::optional<std::vector<std::vector<storm::storage::BitVector>>> _memoryTransitions;  // BitVector contains the model states that lead from startState to goalSate of teh DA
+                boost::optional<std::vector<std::vector<storm::storage::BitVector>>> _memoryTransitions;  // BitVector contains the model states that lead from startState to goalSate of the DA
                 boost::optional<std::vector<uint_fast64_t>> _memoryInitialStates; // Saves for each modelState which automaton state is reached from the initial state //TODO improve
 
+                // MEC scheduler
+                boost::optional<std::map <std::pair<uint_fast64_t,std::pair<uint_fast64_t, uint_fast64_t>> , storm::storage::SchedulerChoice<ValueType>>> _mecProductChoices;   //  <#literal, <s, daState>> ---> choice
+                boost::optional<std::vector<std::vector<storm::storage::BitVector>>> _mecMemoryTransitions;  // BitVector contains the model states that lead from #INF(i) to #INF(i+1) of the AccCondition (#INF(1) AND #INF(2) ....) OR (..)
+
             };
         }
     }

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<storm::models::sparse::Mdp<ValueType>>();
+            auto const& inducedMdp = inducedModel->template as<storm::models::sparse::Mdp<ValueType>>(); // TODO DTMC!
             EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates());
             storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> 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<ValueType>()[*mdp->getInitialStates().begin()], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
         }
+        {
+            auto result = checker.check(this->env(), tasks[2]);
+            EXPECT_NEAR(this->parseNumber("1/2"), result->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+
+            ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+            ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
+            storm::storage::Scheduler<ValueType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().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<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>()[*mdp->getInitialStates().begin()], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+        }
     }
     
 }