From e48f3d070583cf159dcdc28b617c26d482f7a792 Mon Sep 17 00:00:00 2001
From: Lukas Posch <lukas.posch@student.tugraz.at>
Date: Tue, 16 Feb 2021 16:09:46 +0100
Subject: [PATCH] added notPhiStates to expandScheduler

---
 .../modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp      | 6 ++++--
 src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h  | 2 +-
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
index ed535f8d4..5a303017c 100644
--- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
+++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
@@ -46,13 +46,13 @@ namespace storm {
                 viHelper.fillResultVector(x, relevantStates, psiStates);
 
                 if (produceScheduler) {
-                    scheduler = std::make_unique<storm::storage::Scheduler<ValueType>>(expandScheduler(viHelper.extractScheduler(), psiStates));
+                    scheduler = std::make_unique<storm::storage::Scheduler<ValueType>>(expandScheduler(viHelper.extractScheduler(), psiStates, ~phiStates));
                 }
                 return MDPSparseModelCheckingHelperReturnType<ValueType>(std::move(x), std::move(scheduler));
             }
 
             template<typename ValueType>
-            storm::storage::Scheduler<ValueType> SparseSmgRpatlHelper<ValueType>::expandScheduler(storm::storage::Scheduler<ValueType> scheduler, storm::storage::BitVector psiStates) {
+            storm::storage::Scheduler<ValueType> SparseSmgRpatlHelper<ValueType>::expandScheduler(storm::storage::Scheduler<ValueType> scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates) {
                 for(uint i = 0; i < 2; i++) {
                 }
                 storm::storage::Scheduler<ValueType> completeScheduler(psiStates.size());
@@ -60,6 +60,8 @@ namespace storm {
                 for(uint stateCounter = 0; stateCounter < psiStates.size(); stateCounter++) {
                     if(psiStates.get(stateCounter)) {
                         completeScheduler.setChoice(0, stateCounter);
+                    } else if(notPhiStates.get(stateCounter)) {
+                        completeScheduler.setChoice(0, stateCounter);
                     } else {
                         completeScheduler.setChoice(scheduler.getChoice(maybeStatesCounter), stateCounter);
                         maybeStatesCounter++;
diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h
index 9505bd51f..7152ab3db 100644
--- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h
+++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h
@@ -39,7 +39,7 @@ namespace storm {
                 static MDPSparseModelCheckingHelperReturnType<ValueType> computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint());
 
             private:
-                static storm::storage::Scheduler<ValueType> expandScheduler(storm::storage::Scheduler<ValueType> scheduler, storm::storage::BitVector psiStates);
+                static storm::storage::Scheduler<ValueType> expandScheduler(storm::storage::Scheduler<ValueType> scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates);
 
             };
         }