diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 5a303017c..89b93aa1d 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -58,8 +58,10 @@ namespace storm { storm::storage::Scheduler completeScheduler(psiStates.size()); uint_fast64_t maybeStatesCounter = 0; for(uint stateCounter = 0; stateCounter < psiStates.size(); stateCounter++) { + // psiStates already fulfill formulae so we can set an arbitrary action if(psiStates.get(stateCounter)) { completeScheduler.setChoice(0, stateCounter); + // ~phiStates do not fulfill formulae so we can set an arbitrary action } else if(notPhiStates.get(stateCounter)) { completeScheduler.setChoice(0, stateCounter); } else {