From 43688d09ea3afd643c2ac74e2f16f9ecbedff295 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Mon, 29 Oct 2018 11:32:48 +0100
Subject: [PATCH] reward infinity scheduler extraction is now correct

---
 .../prctl/helper/SparseMdpPrctlHelper.cpp       |  2 +-
 src/storm/utility/graph.cpp                     | 17 +++++++++++++++--
 src/storm/utility/graph.h                       | 10 ++++++++++
 3 files changed, 26 insertions(+), 3 deletions(-)

diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
index e455e2308..7e1d6e45c 100644
--- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
+++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
@@ -1053,7 +1053,7 @@ namespace storm {
                         scheduler.setChoice(0, state);
                     }
                 } else {
-                    storm::utility::graph::computeSchedulerProb0E(qualitativeStateSets.infinityStates, transitionMatrix, scheduler);
+                    storm::utility::graph::computeSchedulerRewInf(qualitativeStateSets.infinityStates, transitionMatrix, scheduler);
                     for (auto const& state : qualitativeStateSets.rewardZeroStates) {
                         scheduler.setChoice(0, state);
                     }
diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp
index 6cd7ca91f..d17d95edc 100644
--- a/src/storm/utility/graph.cpp
+++ b/src/storm/utility/graph.cpp
@@ -429,6 +429,7 @@ namespace storm {
                 std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices();
                 
                 for (auto const& state : states) {
+                    bool setValue = false;
                     for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) {
                         bool oneSuccessorInStates = false;
                         for (auto const& element : transitionMatrix.getRow(choice)) {
@@ -441,9 +442,11 @@ namespace storm {
                             for (uint_fast64_t memState = 0; memState < scheduler.getNumberOfMemoryStates(); ++memState) {
                                 scheduler.setChoice(choice - nondeterministicChoiceIndices[state], state, memState);
                             }
+                            setValue = true;
                             break;
                         }
                     }
+                    STORM_LOG_ASSERT(setValue, "Expected that at least one action for state " <<  state << " leads with positive probability to the selected state");
                 }
             }
             
@@ -494,6 +497,11 @@ namespace storm {
             void computeSchedulerProb0E(storm::storage::BitVector const& prob0EStates, storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::Scheduler<T>& scheduler) {
                 computeSchedulerStayingInStates(prob0EStates, transitionMatrix, scheduler);
             }
+
+            template <typename T>
+            void computeSchedulerRewInf(storm::storage::BitVector const& rewInfStates, storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::Scheduler<T>& scheduler) {
+                computeSchedulerWithOneSuccessorInStates(rewInfStates, transitionMatrix, scheduler);
+            }
             
             template <typename T>
             void 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::Scheduler<T>& scheduler, boost::optional<storm::storage::BitVector> const& rowFilter) {
@@ -1665,7 +1673,10 @@ namespace storm {
             template void computeSchedulerProbGreater0E(storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler<double>& scheduler, boost::optional<storm::storage::BitVector> const& rowFilter);
             
             template void computeSchedulerProb0E(storm::storage::BitVector const& prob0EStates, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::Scheduler<double>& scheduler);
-            
+
+            template void computeSchedulerRewInf(storm::storage::BitVector const& rewInfStates, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::Scheduler<double>& scheduler);
+
+
             template void 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, storm::storage::Scheduler<double>& scheduler, boost::optional<storm::storage::BitVector> const& rowFilter = boost::none);
             
             template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ;
@@ -1734,7 +1745,9 @@ namespace storm {
             template void computeSchedulerProbGreater0E(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler<storm::RationalNumber>& scheduler, boost::optional<storm::storage::BitVector> const& rowFilter);
             
             template void computeSchedulerProb0E(storm::storage::BitVector const& prob0EStates, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::Scheduler<storm::RationalNumber>& scheduler);
-            
+
+            template void computeSchedulerRewInf(storm::storage::BitVector const& rewInfStates, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::Scheduler<storm::RationalNumber>& scheduler);
+
             template void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler<storm::RationalNumber>& scheduler, boost::optional<storm::storage::BitVector> const& rowFilter = boost::none);
             
             template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ;
diff --git a/src/storm/utility/graph.h b/src/storm/utility/graph.h
index d42a6be2f..152cf10b9 100644
--- a/src/storm/utility/graph.h
+++ b/src/storm/utility/graph.h
@@ -284,6 +284,16 @@ namespace storm {
             template <typename T>
             void computeSchedulerProbGreater0E(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler<T>& scheduler, boost::optional<storm::storage::BitVector> const& rowFilter = boost::none);
 
+            /*!
+             * Computes a scheduler for the given states that have a scheduler that has a reward infinity.
+             *
+             * @param rewInfStates The states that have a scheduler achieving reward infinity.
+             * @param transitionMatrix The transition matrix of the system.
+             * @param scheduler The resulting scheduler for the rewInf States. The scheduler is not set at other states.
+             */
+            template <typename T>
+            void computeSchedulerRewInf(storm::storage::BitVector const& rewInfStates, storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::Scheduler<T>& scheduler);
+
             /*!
              * Computes a scheduler for the given states that have a scheduler that has a probability 0.
              *