scheduler support for LTL-MC

Conflicts:
	src/storm/storage/Scheduler.cpp

src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp

@@ -144,7 +144,7 @@ namespace storm {
                 modelDot.close();
             }
 
-            storm::modelchecker::helper::SparseLTLHelper<ValueType, true> helper(embeddedMdp.getTransitionMatrix(), this->getModel().getNumberOfStates());
+            storm::modelchecker::helper::SparseLTLHelper<ValueType, true> helper(embeddedMdp.getTransitionMatrix(), embeddedMdp.getNumberOfStates());
             storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, embeddedMdp);
 
             // Compute Satisfaction sets for APs

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

@@ -1,8 +1,5 @@
-#include <modelchecker/results/ExplicitQualitativeCheckResult.h>
-#include <logic/ExtractMaximalStateFormulasVisitor.h>
 #include "SparseLTLHelper.h"
 
-#include "storm/transformer/DAProductBuilder.h"
 #include "storm/automata/LTL2DeterministicAutomaton.h"
 
 #include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h"
@@ -10,6 +7,8 @@
 
 #include "storm/storage/StronglyConnectedComponentDecomposition.h"
 #include "storm/storage/MaximalEndComponentDecomposition.h"
+#include "storm/storage/memorystructure/MemoryStructure.h"
+#include "storm/storage/memorystructure/MemoryStructureBuilder.h"
 
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/DebugSettings.h"
@@ -26,6 +25,55 @@ namespace storm {
                 // Intentionally left empty.
             }
 
+
+            template <typename ValueType, bool Nondeterministic>
+            storm::storage::Scheduler<ValueType> SparseLTLHelper<ValueType, Nondeterministic>::SparseLTLHelper::extractScheduler(storm::models::sparse::Model<ValueType> const& model) {
+                STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested.");
+                STORM_LOG_ASSERT(this->_productChoices.is_initialized(), "Trying to extract the produced scheduler but none is available. Was there a computation call before?");
+                STORM_LOG_ASSERT(this->_memoryTransitions.is_initialized(), "Trying to extract the DA transition structure but none is available. Was there a computation call before?");
+                STORM_LOG_ASSERT(this->_memoryInitialStates.is_initialized(), "Trying to extract the initial states of the DA but there are none available. Was there a computation call before?");
+
+                // Create a memory structure for the MDP scheduler with memory.
+                typename storm::storage::MemoryStructureBuilder<ValueType>::MemoryStructureBuilder memoryBuilder(this->_memoryTransitions.get().size(), model);
+
+                // Build the transitions between the memory states:  startState--- modelStates (transitionVector) --->goalState
+                for (storm::storage::sparse::state_type startState = 0; startState < this->_memoryTransitions.get().size(); ++startState) {
+                    for (storm::storage::sparse::state_type goalState = 0; goalState < this->_memoryTransitions.get().size(); ++goalState) {
+                        // Bitvector that represents modelStates the model states that trigger this transition.
+                        memoryBuilder.setTransition(startState, goalState, this->_memoryTransitions.get()[startState][goalState]);
+                    }
+                }
+
+                /*
+                memoryStateLabeling: Label the memory states to specify, e.g., accepting states // TODO where are these labels used?
+                for (storm::storage::sparse::state_type q : set) {
+                    memoryBuilder.setLabel(q,//todo);
+                }
+                */
+
+                // initialMemoryStates: Assign an initial memory state to each initial state of the model.
+                for (uint_fast64_t s0 : model.getInitialStates()) {
+                    // Label the state as initial TODO unnecessary?
+                    //memoryBuilder.setLabel(q, "Initial for model state " s0)
+                    memoryBuilder.setInitialMemoryState(s0, this->_memoryInitialStates.get()[s0]);
+                }
+
+
+                // Finally, we can build the memoryStructure.
+                storm::storage::MemoryStructure memoryStructure = memoryBuilder.build();
+
+                // Create a scheduler (with memory of size DA) for the model from the scheduler of the MDP-DA-product model.
+                storm::storage::Scheduler<ValueType> scheduler(this->_transitionMatrix.getRowGroupCount(), memoryStructure);
+
+                // Use choices in the product model to create a choice based on model state and memory state
+                for (const auto &choice : this->_productChoices.get()) {
+                    uint_fast64_t modelState = choice.first.first;
+                    uint_fast64_t memoryState = choice.first.second;
+                    scheduler.setChoice(choice.second, modelState, memoryState);
+                }
+
+                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;
@@ -141,7 +189,10 @@ namespace storm {
                         if (accepting) {
                             accMECs++;
                             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);
                             }
                         }
@@ -180,12 +231,13 @@ namespace storm {
             std::vector<ValueType> SparseLTLHelper<ValueType, Nondeterministic>::computeDAProductProbabilities(Environment const& env, storm::automata::DeterministicAutomaton const& da, std::map<std::string, storm::storage::BitVector>& apSatSets) {
                 const storm::automata::APSet& apSet = da.getAPSet();
 
-                std::vector<storm::storage::BitVector> apLabels;
+
+                std::vector<storm::storage::BitVector> statesForAP;
                 for (const std::string& ap : apSet.getAPs()) {
                     auto it = apSatSets.find(ap);
                     STORM_LOG_THROW(it != apSatSets.end(), storm::exceptions::InvalidOperationException, "Deterministic automaton has AP " << ap << ", does not appear in formula");
 
-                    apLabels.push_back(std::move(it->second));
+                    statesForAP.push_back(std::move(it->second));
                 }
 
                 storm::storage::BitVector statesOfInterest;
@@ -199,9 +251,10 @@ namespace storm {
 
 
                 STORM_LOG_INFO("Building "+ (Nondeterministic ? std::string("MDP-DA") : std::string("DTMC-DA")) +"product with deterministic automaton, starting from " << statesOfInterest.getNumberOfSetBits() << " model states...");
-                storm::transformer::DAProductBuilder productBuilder(da, apLabels);
+                transformer::DAProductBuilder productBuilder(da, statesForAP);
+
+                typename transformer::DAProduct<productModelType>::ptr product = productBuilder.build<productModelType>(this->_transitionMatrix, statesOfInterest);
 
-                auto product = productBuilder.build<productModelType>(this->_transitionMatrix, statesOfInterest);
 
                 STORM_LOG_INFO("Product "+ (Nondeterministic ? std::string("MDP-DA") : std::string("DTMC-DA")) +" has " << product->getProductModel().getNumberOfStates() << " states and "
                                                    << product->getProductModel().getNumberOfTransitions() << " transitions.");
@@ -254,15 +307,56 @@ namespace storm {
 
 
                 if (Nondeterministic) {
-                    prodNumericResult = std::move(storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(env,
+                    MDPSparseModelCheckingHelperReturnType<ValueType> prodCheckResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(env,
                                                                                                                               std::move(solveGoalProduct),
                                                                                                                               product->getProductModel().getTransitionMatrix(),
                                                                                                                               product->getProductModel().getBackwardTransitions(),
                                                                                                                               bvTrue,
                                                                                                                               acceptingStates,
                                                                                                                               this->isQualitativeSet(),
-                                                                                                                                          false  // no schedulers (at the moment)
-                                                                                                                                ).values);
+                                                                                                                              this->isProduceSchedulerSet() // Whether to create memoryless scheduler for the Model-DA Product.
+                                                                                                                              );
+                    prodNumericResult = std::move(prodCheckResult.values);
+
+                    if (this->isProduceSchedulerSet()) {
+                        // Extract the choices of the scheduler for the MDP-DA product: <s,q> -> choice
+                        this->_productChoices.emplace();
+                        for (storm::storage::sparse::state_type pState = 0;
+                            pState < product->getProductModel().getNumberOfStates(); ++pState) {
+                            this->_productChoices.get().insert({std::make_pair(product->getModelState(pState), product->getAutomatonState(pState)), prodCheckResult.scheduler->getChoice(pState)});
+                        }
+
+
+                        // Prepare the memory structure. For that, we need: transitions,  initialMemoryStates (and todo: memoryStateLabeling)
+
+                        // The next move function of the memory, will be build based on the transitions of the DA.
+                        this->_memoryTransitions.emplace(da.getNumberOfStates(), std::vector<storm::storage::BitVector>(da.getNumberOfStates()));
+
+                        for (storm::storage::sparse::state_type startState = 0; startState < da.getNumberOfStates(); ++startState) {
+                            for (storm::storage::sparse::state_type goalState = 0;
+                                 goalState < da.getNumberOfStates(); ++goalState) {
+                                // Bitvector that represents modelStates the model states that trigger this transition.
+                                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)) {
+                                        modelStates.set(modelState);
+                                    }
+                                }
+                                // Insert a transition: startState--{modelStates}-->goalState
+                                this->_memoryTransitions.get()[startState][goalState] = std::move(modelStates);
+                            }
+                        }
+
+                        this->_memoryInitialStates.emplace();
+                        this->_memoryInitialStates->resize(this->_transitionMatrix.getRowGroupCount());
+                        // Save for each automaton state for which model state it is initial.
+                        for (storm::storage::sparse::state_type modelState = 0; modelState< this->_transitionMatrix.getRowGroupCount(); ++modelState) {
+                            this->_memoryInitialStates.get().at(modelState) = productBuilder.getInitialState(modelState);
+                        }
+
+                        // TODO labels (e.g. the accepting set?) for the automaton states
+                    }
 
                 } else {
                     prodNumericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeUntilProbabilities(env,
@@ -275,6 +369,7 @@ namespace storm {
                     }
 
                 std::vector<ValueType> numericResult = product->projectToOriginalModel(this->_numberOfStates, prodNumericResult);
+
                 return numericResult;
             }
 

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

@@ -1,10 +1,12 @@
 #include "storm/modelchecker/helper/SingleValueModelCheckerHelper.h"
+#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
 #include "storm/automata/DeterministicAutomaton.h"
 #include "storm/storage/SparseMatrix.h"
 #include "storm/solver/SolveGoal.h"
 #include "storm/models/sparse/Dtmc.h"
 #include "storm/models/sparse/Mdp.h"
 #include "storm/logic/ExtractMaximalStateFormulasVisitor.h"
+#include "storm/transformer/DAProductBuilder.h"
 
 
 namespace storm {
@@ -34,6 +36,14 @@ namespace storm {
                  */
                 SparseLTLHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::size_t numberOfSates);
 
+
+                /*!
+                 * @pre before calling this, a computation call should have been performed during which scheduler production was enabled.
+                 * @param TODO
+                 * @return a new scheduler containing optimal choices for each state that yield the long run average values of the most recent call.
+                 */
+                storm::storage::Scheduler<ValueType> extractScheduler(storm::models::sparse::Model<ValueType> const& model);
+
                 /*!
                  * todo computes Sat sets of AP
                  * @param
@@ -73,18 +83,23 @@ namespace storm {
                  * @param the transition matrix of the model
                  * @param the reversed transition relation
                  */
-                static storm::storage::BitVector computeAcceptingECs(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions);
+                storm::storage::BitVector computeAcceptingECs(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions);
 
                 /**
                 * Compute a set S of states that are contained in BSCCs that satisfy the given acceptance conditon.
                 * @tparam the acceptance condition
                 * @tparam the transition matrix of the model
                 */
-                static storm::storage::BitVector computeAcceptingBCCs(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix<ValueType> const& transitionMatrix);
+                storm::storage::BitVector computeAcceptingBCCs(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix<ValueType> const& transitionMatrix);
 
 
                 storm::storage::SparseMatrix<ValueType> const& _transitionMatrix;
-                std::size_t _numberOfStates;
+                std::size_t _numberOfStates;  //TODO just use _transitionMatrix.getRowGroupCount instead?
+
+                // 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<uint_fast64_t>> _memoryInitialStates; // Saves for each modelState which automaton state is reached from the initial state //TODO improve
 
             };
         }

src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp

@@ -164,7 +164,7 @@ namespace storm {
                 modelDot.close();
             }
 
-            storm::modelchecker::helper::SparseLTLHelper<ValueType, false> helper(dtmc.getTransitionMatrix(), this->getModel().getNumberOfStates());
+            storm::modelchecker::helper::SparseLTLHelper<ValueType, false> helper(dtmc.getTransitionMatrix(), dtmc.getNumberOfStates());
             storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, dtmc);
 
             // Compute Satisfaction sets for APs

src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@@ -14,9 +14,7 @@
 
 #include "storm/logic/FragmentSpecification.h"
 
-#include "storm/transformer/DAProductBuilder.h"
 #include "storm/logic/ExtractMaximalStateFormulasVisitor.h"
-#include "storm/automata/LTL2DeterministicAutomaton.h"
 
 #include "storm/models/sparse/StandardRewardModel.h"
 
@@ -199,6 +197,7 @@ namespace storm {
                 modelDot.close();
             }
 
+
             storm::modelchecker::helper::SparseLTLHelper<ValueType, true> helper(mdp.getTransitionMatrix(), mdp.getNumberOfStates());
             storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, mdp);
 
@@ -208,7 +207,13 @@ namespace storm {
 
             std::vector<ValueType> numericResult = helper.computeLTLProbabilities(env, *ltlFormula, apSets);
 
-            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
+            //TODO for MA too
+            std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
+            if (checkTask.isProduceSchedulersSet()) {
+                result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::make_unique<storm::storage::Scheduler<ValueType>>(helper.extractScheduler(mdp)));
+            }
+
+            return result;
         }
 
         template<typename SparseMdpModelType>

src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h

@@ -19,10 +19,6 @@ namespace storm {
     // fwd
     class Environment;
 
-    namespace automata {
-        class DeterministicAutomaton;
-    }
-
     namespace models {
         namespace sparse {
             template <typename ValueType, typename RewardModelType> class Dtmc;

src/storm/storage/Scheduler.cpp

@@ -224,6 +224,10 @@ namespace storm {
                 out << "Skipped " << numOfSkippedStatesWithUniqueChoice << " deterministic states with unique choice." << std::endl;
             }
             out << "___________________________________________________________________" << std::endl;
+
+            // TODO only for tests:
+            out << memoryStructure->toString();
+            out << std::endl;
         }
 
         template <>

src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp

@@ -288,7 +288,7 @@ namespace storm {
                             uint64_t transitionId = entryIt - model.getTransitionMatrix().begin();
                             uint64_t successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState];
                             builder.addNextValue(currentRow, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue());
-                        }
+                        } //TODO  successor MemoryState is a problem here 8382838738483264 oder so
                     } else {
                         std::map<uint64_t, ValueType> transitions;
                         for (auto const& choiceIndex : choice.getChoiceAsDistribution()) {

src/storm/transformer/DAProductBuilder.h

@@ -35,7 +35,7 @@ namespace storm {
                 return da.getSuccessor(da.getInitialState(), getLabelForState(modelState));
             }
 
-            storm::storage::sparse::state_type getSuccessor(storm::storage::sparse::state_type modelFrom,
+            storm::storage::sparse::state_type getSuccessor(storm::storage::sparse::state_type modelFrom,  //TODO delete modelFrom?
                                                             storm::storage::sparse::state_type automatonFrom,
                                                             storm::storage::sparse::state_type modelTo) const {
                 return da.getSuccessor(automatonFrom, getLabelForState(modelTo));

src/storm/transformer/ProductBuilder.h

@@ -33,7 +33,6 @@ namespace storm {
                 // use of the SparseMatrixBuilder that can only handle linear addNextValue
                 // calls
                 std::deque<state_type> todo;
-
                 for (state_type s_0 : statesOfInterest) {
                     state_type q_0 = prodOp.getInitialState(s_0);
 

src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp

@@ -173,6 +173,7 @@ namespace {
             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>>();
@@ -202,4 +203,56 @@ namespace {
         }
     }
 
+    TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, ltl) {
+        typedef typename TestFixture::ValueType ValueType;
+
+        std::string formulasString = "Pmax=? [X X \"target\"]; Pmin=? [G F \"target\"];";
+        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);
+        EXPECT_EQ(4ull, mdp->getNumberOfStates());
+        EXPECT_EQ(11ull, mdp->getNumberOfTransitions());
+        ASSERT_EQ(mdp->getType(), storm::models::ModelType::Mdp);
+        EXPECT_EQ(7ull, mdp->getNumberOfChoices());
+
+        storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
+
+        {
+            auto result = checker.check(this->env(), tasks[0]);
+            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[0]);
+            ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
+            EXPECT_NEAR(this->parseNumber("9/10"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+        }
+        {
+            auto result = checker.check(this->env(), tasks[1]);
+            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[1]);
+            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());
+        }
+    }
+    
 }