fixed bug in prob1E. added functions to retrieve schedulers for prob0E, probGreater0E and prob1E states of MDPs

Former-commit-id: aea5fe773b

src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h

@@ -53,8 +53,6 @@ namespace storm {
                 
                 static std::vector<ValueType> computeLongRunAverage(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
 
-                
-                
             private:
                 static std::vector<ValueType> computeReachabilityRewardsHelper(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
     

src/utility/graph.cpp

@@ -238,6 +238,110 @@ namespace storm {
                 return result;
             }
             
+            template <typename T>
+            storm::storage::PartialScheduler computeSchedulerStayingInStates(storm::storage::BitVector const& states, storm::storage::SparseMatrix<T> const& transitionMatrix) {
+                storm::storage::PartialScheduler result;
+                std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices();
+                
+                for (auto const& state : states) {
+                    for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) {
+                        bool allSuccessorsInStates = true;
+                        for (auto const& element : transitionMatrix.getRow(choice)) {
+                            if (!states.get(element.getColumn())) {
+                                allSuccessorsInStates = false;
+                                break;
+                            }
+                        }
+                        if (allSuccessorsInStates) {
+                            result.setChoice(state, choice);
+                            break;
+                        }
+                    }
+                }
+                
+                return result;
+            }
+            
+            template <typename T>
+            storm::storage::PartialScheduler computeSchedulerWithOneSuccessorInStates(storm::storage::BitVector const& states, storm::storage::SparseMatrix<T> const& transitionMatrix) {
+                storm::storage::PartialScheduler result;
+                std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices();
+                
+                for (auto const& state : states) {
+                    for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) {
+                        bool oneSuccessorInStates = false;
+                        for (auto const& element : transitionMatrix.getRow(choice)) {
+                            if (states.get(element.getColumn())) {
+                                oneSuccessorInStates = true;
+                                break;
+                            }
+                        }
+                        if (oneSuccessorInStates) {
+                            result.setChoice(state, choice);
+                            break;
+                        }
+                    }
+                }
+                
+                return result;
+            }
+            
+            template <typename T>
+            storm::storage::PartialScheduler computeSchedulerProbGreater0E(storm::storage::BitVector const& probGreater0EStates, storm::storage::SparseMatrix<T> const& transitionMatrix) {
+                return computeSchedulerWithOneSuccessorInStates(probGreater0EStates, transitionMatrix);
+            }
+            
+            template <typename T>
+            storm::storage::PartialScheduler computeSchedulerProb0E(storm::storage::BitVector const& prob0EStates, storm::storage::SparseMatrix<T> const& transitionMatrix) {
+                return computeSchedulerStayingInStates(prob0EStates, transitionMatrix);
+            }
+            
+            template <typename T>
+            storm::storage::PartialScheduler computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+                
+                storm::storage::PartialScheduler result;
+                std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices();
+                std::vector<uint_fast64_t> stack;
+                storm::storage::BitVector currentStates(psiStates);
+                stack.insert(stack.end(), currentStates.begin(), currentStates.end());
+                uint_fast64_t currentState = 0;
+                
+                while (!stack.empty()) {
+                    currentState = stack.back();
+                    stack.pop_back();
+                    
+                    for (typename storm::storage::SparseMatrix<T>::const_iterator predecessorEntryIt = backwardTransitions.begin(currentState), predecessorEntryIte = backwardTransitions.end(currentState); predecessorEntryIt != predecessorEntryIte; ++predecessorEntryIt) {
+                        if (phiStates.get(predecessorEntryIt->getColumn()) && !currentStates.get(predecessorEntryIt->getColumn())) {
+                            // Check whether the predecessor has only successors in the prob1E state set for one of the
+                            // nondeterminstic choices.
+                            for (uint_fast64_t row = nondeterministicChoiceIndices[predecessorEntryIt->getColumn()]; row < nondeterministicChoiceIndices[predecessorEntryIt->getColumn() + 1]; ++row) {
+                                bool allSuccessorsInProb1EStates = true;
+                                bool hasSuccessorInCurrentStates = false;
+                                for (typename storm::storage::SparseMatrix<T>::const_iterator successorEntryIt = transitionMatrix.begin(row), successorEntryIte = transitionMatrix.end(row); successorEntryIt != successorEntryIte; ++successorEntryIt) {
+                                    if (!prob1EStates.get(successorEntryIt->getColumn())) {
+                                        allSuccessorsInProb1EStates = false;
+                                        break;
+                                    } else if (currentStates.get(successorEntryIt->getColumn())) {
+                                        hasSuccessorInCurrentStates = true;
+                                    }
+                                }
+                                
+                                // If all successors for a given nondeterministic choice are in the prob1E state set, we
+                                // perform a backward search from that state.
+                                if (allSuccessorsInProb1EStates && hasSuccessorInCurrentStates) {
+                                    result.setChoice(predecessorEntryIt->getColumn(), row);
+                                    currentStates.set(predecessorEntryIt->getColumn(), true);
+                                    stack.push_back(predecessorEntryIt->getColumn());
+                                    break;
+                                }
+                            }
+                        }
+                    }
+                }
+                
+                return result;
+            }
+            
             template <typename T>
             storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound, uint_fast64_t maximalSteps) {
                 size_t numberOfStates = phiStates.size();
@@ -333,17 +437,20 @@ namespace storm {
                                 // nondeterminstic choices.
                                 for (uint_fast64_t row = nondeterministicChoiceIndices[predecessorEntryIt->getColumn()]; row < nondeterministicChoiceIndices[predecessorEntryIt->getColumn() + 1]; ++row) {
                                     bool allSuccessorsInCurrentStates = true;
+                                    bool hasNextStateSuccessor = false;
                                     for (typename storm::storage::SparseMatrix<T>::const_iterator successorEntryIt = transitionMatrix.begin(row), successorEntryIte = transitionMatrix.end(row); successorEntryIt != successorEntryIte; ++successorEntryIt) {
                                         if (!currentStates.get(successorEntryIt->getColumn())) {
                                             allSuccessorsInCurrentStates = false;
                                             break;
+                                        } else if (nextStates.get(successorEntryIt->getColumn())) {
+                                            hasNextStateSuccessor = true;
                                         }
                                     }
                                     
                                     // If all successors for a given nondeterministic choice are in the current state set, we
                                     // add it to the set of states for the next iteration and perform a backward search from
                                     // that state.
-                                    if (allSuccessorsInCurrentStates) {
+                                    if (allSuccessorsInCurrentStates && hasNextStateSuccessor) {
                                         nextStates.set(predecessorEntryIt->getColumn(), true);
                                         stack.push_back(predecessorEntryIt->getColumn());
                                         break;
@@ -843,6 +950,12 @@ namespace storm {
             
             
             
+            template storm::storage::PartialScheduler computeSchedulerProbGreater0E(storm::storage::BitVector const& probGreater0EStates, storm::storage::SparseMatrix<double> const& transitionMatrix);
+            
+            template storm::storage::PartialScheduler computeSchedulerProb0E(storm::storage::BitVector const& prob0EStates, storm::storage::SparseMatrix<double> const& transitionMatrix);
+            
+            template storm::storage::PartialScheduler computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+            
             template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ;
             
             template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);

src/utility/graph.h

@@ -7,6 +7,7 @@
 #include "utility/OsDetection.h"
 
 #include "src/storage/sparse/StateType.h"
+#include "src/storage/PartialScheduler.h"
 #include "src/models/sparse/NondeterministicModel.h"
 #include "src/models/sparse/DeterministicModel.h"
 #include "src/storage/dd/DdType.h"
@@ -49,6 +50,7 @@ namespace storm {
              */
             template<typename T>
             storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates);
+            
             /*!
              * Performs a breadth-first search through the underlying graph structure to compute the distance from all
              * states to the starting states of the search.
@@ -74,6 +76,7 @@ namespace storm {
              */
             template <typename T>
             storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0);
+            
             /*!
              * Computes the set of states of the given model for which all paths lead to
              * the given set of target states and only visit states from the filter set
@@ -132,7 +135,6 @@ namespace storm {
             template <typename T>
             std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01(storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
             
-            
             /*!
              * Computes the set of states that has a positive probability of reaching psi states after only passing
              * through phi states before.
@@ -199,6 +201,54 @@ namespace storm {
             template <storm::dd::DdType Type>
             std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> performProb01(storm::models::symbolic::Model<Type> const& model, storm::dd::Add<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates);
             
+            /*!
+             * Computes a scheduler for the given states that chooses an action that stays completely in the very same set.
+             * Note that this assumes that there is a legal choice for each of the states.
+             *
+             * @param states The set of states for which to compute the scheduler that stays in this very set.
+             * @param transitionMatrix The transition matrix.
+             */
+            template <typename T>
+            storm::storage::PartialScheduler computeSchedulerStayingInStates(storm::storage::BitVector const& states, storm::storage::SparseMatrix<T> const& transitionMatrix);
+
+            /*!
+             * Computes a scheduler for the given states that chooses an action that has at least one successor in the
+             * given set of states. Note that this assumes that there is a legal choice for each of the states.
+             *
+             * @param states The set of states for which to compute the scheduler that chooses an action with a successor
+             * in this very set.
+             * @param transitionMatrix The transition matrix.
+             */
+            template <typename T>
+            storm::storage::PartialScheduler computeSchedulerWithOneSuccessorInStates(storm::storage::BitVector const& states, storm::storage::SparseMatrix<T> const& transitionMatrix);
+            
+            /*!
+             * Computes a scheduler for the given states that have a scheduler that has a probability greater 0.
+             *
+             * @param probGreater0EStates The states that have a scheduler achieving a probablity greater 0.
+             * @param transitionMatrix The transition matrix of the system.
+             */
+            template <typename T>
+            storm::storage::PartialScheduler computeSchedulerProbGreater0E(storm::storage::BitVector const& probGreater0EStates, storm::storage::SparseMatrix<T> const& transitionMatrix);
+
+            /*!
+             * Computes a scheduler for the given states that have a scheduler that has a probability 0.
+             *
+             * @param prob0EStates The states that have a scheduler achieving probablity 0.
+             * @param transitionMatrix The transition matrix of the system.
+             */
+            template <typename T>
+            storm::storage::PartialScheduler computeSchedulerProb0E(storm::storage::BitVector const& prob0EStates, storm::storage::SparseMatrix<T> const& transitionMatrix);
+
+            /*!
+             * Computes a scheduler for the given states that have a scheduler that has a probability 0.
+             *
+             * @param prob1EStates The states that have a scheduler achieving probablity 1.
+             * @param transitionMatrix The transition matrix of the system.
+             */
+            template <typename T>
+            storm::storage::PartialScheduler computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+            
             /*!
              * Computes the sets of states that have probability greater 0 of satisfying phi until psi under at least
              * one possible resolution of non-determinism in a non-deterministic model. Stated differently,
@@ -361,6 +411,7 @@ namespace storm {
              */
             template <storm::dd::DdType Type>
             storm::dd::Bdd<Type> performProbGreater0E(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates);
+            
             /*!
              * Computes the set of states for which there does not exist a scheduler that achieves a probability greater
              * than zero of satisfying phi until psi.
@@ -372,7 +423,8 @@ namespace storm {
              * @return A BDD representing all such states.
              */
             template <storm::dd::DdType Type>
-            storm::dd::Bdd<Type> performProb0A(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates) ;
+            storm::dd::Bdd<Type> performProb0A(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates);
+            
             /*!
              * Computes the set of states for which all schedulers achieve a probability greater than zero of satisfying
              * phi until psi.
@@ -384,7 +436,8 @@ namespace storm {
              * @return A BDD representing all such states.
              */
             template <storm::dd::DdType Type>
-            storm::dd::Bdd<Type> performProbGreater0A(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates) ;
+            storm::dd::Bdd<Type> performProbGreater0A(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates);
+            
             /*!
              * Computes the set of states for which there exists a scheduler that achieves probability zero of satisfying
              * phi until psi.