added notPhiStates to expandScheduler

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++;

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);
 
             };
         }