Sparse MDP model checker now correctly computes (memoryless) schedulers for Until and Reachability Reward formulas.

Former-commit-id: c756093fd4

examples/mdp/tiny/tiny.pctl

@@ -0,0 +1,2 @@
+Pmin=? [ F a ]
+Pmax=? [ F a ]

src/counterexamples/MILPMinimalLabelSetGenerator.h

@@ -1275,7 +1275,7 @@ namespace storm {
                 // (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set.
                 double maximalReachabilityProbability = 0;
                 storm::modelchecker::prctl::SparseMdpPrctlModelChecker<T> modelchecker(labeledMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver<T>());
-                std::vector<T> result = modelchecker.checkUntil(false, phiStates, psiStates, false, nullptr);
+                std::vector<T> result = modelchecker.checkUntil(false, phiStates, psiStates, false).first;
                 for (auto state : labeledMdp.getInitialStates()) {
                     maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]);
                 }

src/counterexamples/SMTMinimalCommandSetGenerator.h

@@ -1454,7 +1454,7 @@ namespace storm {
                 // (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set.
                 double maximalReachabilityProbability = 0;
                 storm::modelchecker::prctl::SparseMdpPrctlModelChecker<T> modelchecker(labeledMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver<T>());
-                std::vector<T> result = modelchecker.checkUntil(false, phiStates, psiStates, false, nullptr);
+                std::vector<T> result = modelchecker.checkUntil(false, phiStates, psiStates, false).first;
                 for (auto state : labeledMdp.getInitialStates()) {
                     maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]);
                 }
@@ -1517,7 +1517,7 @@ namespace storm {
                     storm::models::Mdp<T> subMdp = labeledMdp.restrictChoiceLabels(commandSet);
                     storm::modelchecker::prctl::SparseMdpPrctlModelChecker<T> modelchecker(subMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver<T>());
                     LOG4CPLUS_DEBUG(logger, "Invoking model checker.");
-                    std::vector<T> result = modelchecker.checkUntil(false, phiStates, psiStates, false, nullptr);
+                    std::vector<T> result = modelchecker.checkUntil(false, phiStates, psiStates, false).first;
                     LOG4CPLUS_DEBUG(logger, "Computed model checking results.");
                     totalModelCheckingTime += std::chrono::high_resolution_clock::now() - modelCheckingClock;
                     

src/modelchecker/prctl/SparseMdpPrctlModelChecker.h

@@ -19,6 +19,7 @@
 #include "src/utility/vector.h"
 #include "src/utility/graph.h"
 #include "src/settings/Settings.h"
+#include "src/storage/TotalScheduler.h"
 
 namespace storm {
     namespace modelchecker {
@@ -265,7 +266,7 @@ namespace storm {
                  * checker. If the qualitative flag is set, exact probabilities might not be computed.
                  */
                 virtual std::vector<Type> checkUntil(const storm::property::prctl::Until<Type>& formula, bool qualitative) const {
-                    return this->checkUntil(this->minimumOperatorStack.top(), formula.getLeft().check(*this), formula.getRight().check(*this), qualitative, nullptr);
+                    return this->checkUntil(this->minimumOperatorStack.top(), formula.getLeft().check(*this), formula.getRight().check(*this), qualitative).first;
                 }
                 
                 /*!
@@ -284,7 +285,7 @@ namespace storm {
                  * @return The probabilities for the satisfying phi until psi for each state of the model. If the
                  * qualitative flag is set, exact probabilities might not be computed.
                  */
-                std::vector<Type> checkUntil(bool minimize, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, std::vector<uint_fast64_t>* scheduler) const {
+                std::pair<std::vector<Type>, storm::storage::TotalScheduler> checkUntil(bool minimize, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) const {
                     // We need to identify the states which have to be taken out of the matrix, i.e.
                     // all states that have probability 0 and 1 of satisfying the until-formula.
                     std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01;
@@ -347,12 +348,10 @@ namespace storm {
                     storm::utility::vector::setVectorValues<Type>(result, statesWithProbability0, storm::utility::constGetZero<Type>());
                     storm::utility::vector::setVectorValues<Type>(result, statesWithProbability1, storm::utility::constGetOne<Type>());
                                         
-                    // If we were required to generate a scheduler, do so now.
-                    if (scheduler != nullptr) {
-                        this->computeTakenChoices(this->minimumOperatorStack.top(), false, result, *scheduler, this->getModel().getNondeterministicChoiceIndices());
-                    }
+                    // Finally, compute a scheduler that achieves the extramal value.
+                    storm::storage::TotalScheduler scheduler = this->computeExtremalScheduler(this->minimumOperatorStack.top(), false, result);
                     
-                    return result;
+                    return std::make_pair(result, scheduler);
                 }
                 
                 /*!
@@ -443,7 +442,7 @@ namespace storm {
                  * checker. If the qualitative flag is set, exact values might not be computed.
                  */
                 virtual std::vector<Type> checkReachabilityReward(const storm::property::prctl::ReachabilityReward<Type>& formula, bool qualitative) const {
-                    return this->checkReachabilityReward(this->minimumOperatorStack.top(), formula.getChild().check(*this), qualitative, nullptr);
+                    return this->checkReachabilityReward(this->minimumOperatorStack.top(), formula.getChild().check(*this), qualitative).first;
                 }
                 
                 /*!
@@ -461,7 +460,7 @@ namespace storm {
                  * @return The expected reward values gained before a target state is reached for each state. If the
                  * qualitative flag is set, exact values might not be computed.
                  */
-                virtual std::vector<Type> checkReachabilityReward(bool minimize, storm::storage::BitVector const& targetStates, bool qualitative, std::vector<uint_fast64_t>* scheduler) const {
+                virtual std::pair<std::vector<Type>, storm::storage::TotalScheduler> checkReachabilityReward(bool minimize, storm::storage::BitVector const& targetStates, bool qualitative) const {
                     // Only compute the result if the model has at least one reward model.
                     if (!(this->getModel().hasStateRewards() || this->getModel().hasTransitionRewards())) {
                         LOG4CPLUS_ERROR(logger, "Missing reward model for formula.");
@@ -548,12 +547,10 @@ namespace storm {
                     storm::utility::vector::setVectorValues(result, targetStates, storm::utility::constGetZero<Type>());
                     storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::constGetInfinity<Type>());
                     
-                    // If we were required to generate a scheduler, do so now.
-                    if (scheduler != nullptr) {
-                        this->computeTakenChoices(this->minimumOperatorStack.top(), true, result, *scheduler, this->getModel().getNondeterministicChoiceIndices());
-                    }
+                    // Finally, compute a scheduler that achieves the extramal value.
+                    storm::storage::TotalScheduler scheduler = this->computeExtremalScheduler(this->minimumOperatorStack.top(), false, result);
                     
-                    return result;
+                    return std::make_pair(result, scheduler);
                 }
                 
             protected:
@@ -565,8 +562,8 @@ namespace storm {
                  * @param takenChoices The output vector that is to store the taken choices.
                  * @param nondeterministicChoiceIndices The assignment of states to their nondeterministic choices in the matrix.
                  */
-                void computeTakenChoices(bool minimize, bool addRewards, std::vector<Type> const& result, std::vector<uint_fast64_t>& takenChoices, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices) const {
-                    std::vector<Type> temporaryResult(nondeterministicChoiceIndices.size() - 1);
+                storm::storage::TotalScheduler computeExtremalScheduler(bool minimize, bool addRewards, std::vector<Type> const& result) const {
+                    std::vector<Type> temporaryResult(this->getModel().getNondeterministicChoiceIndices().size() - 1);
                     std::vector<Type> nondeterministicResult(result);
                     storm::solver::GmmxxLinearEquationSolver<Type> solver;
                     solver.performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), nondeterministicResult, nullptr, 1);
@@ -585,11 +582,16 @@ namespace storm {
                         }
                         storm::utility::vector::addVectorsInPlace(nondeterministicResult, totalRewardVector);
                     }
+                    
+                    std::vector<uint_fast64_t> choices(this->getModel().getNumberOfStates());
+                    
                     if (minimize) {
-                        storm::utility::vector::reduceVectorMin(nondeterministicResult, temporaryResult, nondeterministicChoiceIndices, &takenChoices);
+                        storm::utility::vector::reduceVectorMin(nondeterministicResult, temporaryResult, this->getModel().getNondeterministicChoiceIndices(), &choices);
                     } else {
-                        storm::utility::vector::reduceVectorMax(nondeterministicResult, temporaryResult, nondeterministicChoiceIndices, &takenChoices);
+                        storm::utility::vector::reduceVectorMax(nondeterministicResult, temporaryResult, this->getModel().getNondeterministicChoiceIndices(), &choices);
                     }
+                    
+                    return storm::storage::TotalScheduler(choices);
                 }
                 
                 /*!

src/storage/PartialScheduler.cpp

@@ -18,6 +18,22 @@ namespace storm {
             if (stateChoicePair == choices.end()) {
                 throw storm::exceptions::InvalidArgumentException() << "Scheduler does not define a choice for state " << state;
             }
+            
+            return stateChoicePair->second;
+        }
+        
+        std::ostream& operator<<(std::ostream& out, PartialScheduler const& scheduler) {
+            out << "partial scheduler (defined on " << scheduler.choices.size() << " states) [ ";
+            uint_fast64_t remainingEntries = scheduler.choices.size();
+            for (auto stateChoicePair : scheduler.choices) {
+                out << stateChoicePair.first << " -> " << stateChoicePair.second;
+                --remainingEntries;
+                if (remainingEntries > 0) {
+                    out << ", ";
+                }
+            }
+            out << "]";
+            return out;
         }
         
     } // namespace storage

src/storage/PartialScheduler.h

@@ -1,6 +1,9 @@
 #ifndef STORM_STORAGE_PARTIALSCHEDULER_H_
 #define STORM_STORAGE_PARTIALSCHEDULER_H_
 
+#include <unordered_map>
+#include <ostream>
+
 #include "src/storage/Scheduler.h"
 
 namespace storm {
@@ -14,9 +17,11 @@ namespace storm {
             
             uint_fast64_t getChoice(uint_fast64_t state) const override;
             
+            friend std::ostream& operator<<(std::ostream& out, PartialScheduler const& scheduler);
+
         private:
             // A mapping from all states that have defined choices to their respective choices.
-            std::unsorted_map<uint_fast64_t, uint_fast64_t> choices;
+            std::unordered_map<uint_fast64_t, uint_fast64_t> choices;
         };
     }
 }

src/storage/Scheduler.h

@@ -1,6 +1,8 @@
 #ifndef STORM_STORAGE_SCHEDULER_H_
 #define STORM_STORAGE_SCHEDULER_H_
 
+#include <cstdint>
+
 namespace storm {
     namespace storage {
         

src/storage/TotalScheduler.cpp

@@ -6,16 +6,32 @@ namespace storm {
             // Intentionally left empty.
         }
         
-        void setChoice(uint_fast64_t state, uint_fast64_t choice) override {
+        TotalScheduler::TotalScheduler(std::vector<uint_fast64_t> const& choices) : choices(choices) {
+            // Intentionally left empty.
+        }
+        
+        void TotalScheduler::setChoice(uint_fast64_t state, uint_fast64_t choice) {
             choices[state] = choice;
         }
         
-        bool isChoiceDefined(uint_fast64_t state) const override {
+        bool TotalScheduler::isChoiceDefined(uint_fast64_t state) const {
             return true;
         }
         
-        uint_fast64_t getChoice(uint_fast64_t state) const override {
+        uint_fast64_t TotalScheduler::getChoice(uint_fast64_t state) const {
             return choices[state];
         }
+        
+        std::ostream& operator<<(std::ostream& out, TotalScheduler const& scheduler) {
+            out << "total scheduler (defined on " << scheduler.choices.size() << " states) [ ";
+            for (uint_fast64_t state = 0; state < scheduler.choices.size() - 1; ++state) {
+                out << state << " -> " << scheduler.choices[state] << ", ";
+            }
+            if (scheduler.choices.size() > 0) {
+                out << (scheduler.choices.size() - 1) << " -> " << scheduler.choices[scheduler.choices.size() - 1] << " ]";
+            }
+            return out;
+        }
+
     }
 }

src/storage/TotalScheduler.h

@@ -1,6 +1,9 @@
 #ifndef STORM_STORAGE_TOTALSCHEDULER_H_
 #define STORM_STORAGE_TOTALSCHEDULER_H_
 
+#include <vector>
+#include <ostream>
+
 #include "src/storage/Scheduler.h"
 
 namespace storm {
@@ -10,12 +13,16 @@ namespace storm {
         public:
             TotalScheduler(uint_fast64_t numberOfStates);
             
+            TotalScheduler(std::vector<uint_fast64_t> const& choices);
+            
             void setChoice(uint_fast64_t state, uint_fast64_t choice) override;
             
             bool isChoiceDefined(uint_fast64_t state) const override;
             
             uint_fast64_t getChoice(uint_fast64_t state) const override;
             
+            friend std::ostream& operator<<(std::ostream& out, TotalScheduler const& scheduler);
+            
         private:
             // A vector that stores the choice for each state.
             std::vector<uint_fast64_t> choices;