fixed computeSchedulerProbGreater0E.

Previously, it did not enforce that psiStates are actually reached. For instance, it was ok to chose a probability 1 selfloop.


Former-commit-id: 518a3b33a9

src/utility/graph.cpp

@@ -310,8 +310,46 @@ namespace storm {
             }
             
             template <typename T>
-            storm::storage::PartialScheduler computeSchedulerProbGreater0E(storm::storage::BitVector const& probGreater0EStates, storm::storage::SparseMatrix<T> const& transitionMatrix) {
-                return computeSchedulerWithOneSuccessorInStates(probGreater0EStates, transitionMatrix);
+            storm::storage::PartialScheduler computeSchedulerProbGreater0E(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional<storm::storage::BitVector> const& rowFilter) {
+                //Perform backwards DFS from psiStates and find a valid choice for each visited state.
+                
+                storm::storage::PartialScheduler result;
+                std::vector<uint_fast64_t> stack;
+                storm::storage::BitVector currentStates(psiStates); //the states that are either psiStates or for which we have found a valid choice.
+                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) {
+                        uint_fast64_t const& predecessor = predecessorEntryIt->getColumn();
+                        if (phiStates.get(predecessor) && !currentStates.get(predecessor)) {
+                            //The predecessor is a probGreater0E state that has not been considered yet. Let's find the right choice that leads to a state in currentStates.
+                            bool foundValidChoice = false;
+                            for (uint_fast64_t row = transitionMatrix.getRowGroupIndices()[predecessor]; row < transitionMatrix.getRowGroupIndices()[predecessor + 1]; ++row) {
+                                if(rowFilter && !rowFilter->get(row)){
+                                    continue;
+                                }
+                                for (typename storm::storage::SparseMatrix<T>::const_iterator successorEntryIt = transitionMatrix.begin(row), successorEntryIte = transitionMatrix.end(row); successorEntryIt != successorEntryIte; ++successorEntryIt) {
+                                    if(currentStates.get(successorEntryIt->getColumn())){
+                                        foundValidChoice = true;
+                                        break;
+                                    }
+                                }
+                                if(foundValidChoice){
+                                    result.setChoice(predecessor, row - transitionMatrix.getRowGroupIndices()[predecessor]);
+                                    currentStates.set(predecessor, true);
+                                    stack.push_back(predecessor);
+                                    break;
+                                }
+                            }
+                            STORM_LOG_INFO_COND(foundValidChoice, "Could not find a valid choice for ProbGreater0E state " << predecessor << ".");
+                        }
+                    }
+                }
+                return result;
             }
             
             template <typename T>
@@ -972,7 +1010,7 @@ namespace storm {
             
             
             
-            template storm::storage::PartialScheduler computeSchedulerProbGreater0E(storm::storage::BitVector const& probGreater0EStates, storm::storage::SparseMatrix<double> const& transitionMatrix);
+            template storm::storage::PartialScheduler computeSchedulerProbGreater0E(storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional<storm::storage::BitVector> const& rowFilter);
             
             template storm::storage::PartialScheduler computeSchedulerProb0E(storm::storage::BitVector const& prob0EStates, storm::storage::SparseMatrix<double> const& transitionMatrix);
             

src/utility/graph.h

@@ -234,13 +234,20 @@ namespace storm {
             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.
+             * Computes a scheduler for the ProbGreater0E-States such that in the induced system the given psiStates are reachable via phiStates
              *
-             * @param probGreater0EStates The states that have a scheduler achieving a probablity greater 0.
              * @param transitionMatrix The transition matrix of the system.
+             * @param backwardTransitions The reversed transition relation.
+             * @param phiStates The set of states satisfying phi.
+             * @param psiStates The set of states satisfying psi.
+             * @param rowFilter If given, the returned scheduler will only pick choices such that rowFilter is true for the corresponding matrixrow.
+             * @return A Scheduler for the ProbGreater0E-States
+             *
+             * @note No choice is defined for ProbGreater0E-States if all the probGreater0-choices violate the row filter.
+             *       This also holds for states that only reach psi via such states.
              */
             template <typename T>
-            storm::storage::PartialScheduler computeSchedulerProbGreater0E(storm::storage::BitVector const& probGreater0EStates, storm::storage::SparseMatrix<T> const& transitionMatrix);
+            storm::storage::PartialScheduler computeSchedulerProbGreater0E(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional<storm::storage::BitVector> const& rowFilter = boost::none);
 
             /*!
              * Computes a scheduler for the given states that have a scheduler that has a probability 0.
@@ -252,10 +259,14 @@ namespace storm {
             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.
+             * Computes a scheduler for the given prob1EStates such that in the induced system the given psiStates are reached with probability 1.
              *
              * @param prob1EStates The states that have a scheduler achieving probablity 1.
              * @param transitionMatrix The transition matrix of the system.
+             * @param backwardTransitions The reversed transition relation.
+             * @param phiStates The set of states satisfying phi.
+             * @param psiStates The set of states satisfying psi.
+             * @return A scheduler for the Prob1E-States
              */
             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);