diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 683099542..f17f0cd27 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -176,8 +176,11 @@ namespace storm { storm::utility::vector::setVectorValues(result, statesWithProbability1, storm::utility::one()); } + // Check if the values of the maybe states are relevant for the SolveGoal + bool maybeStatesNotRelevant = goal.hasRelevantValues() && goal.relevantValues().isDisjointFrom(maybeStates); + // Check whether we need to compute exact probabilities for some states. - if (qualitative) { + if (qualitative || maybeStatesNotRelevant) { // Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1. storm::utility::vector::setVectorValues(result, maybeStates, storm::utility::convertNumber(0.5)); } else { @@ -434,8 +437,11 @@ namespace storm { storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::infinity()); } + // Check if the values of the maybe states are relevant for the SolveGoal + bool maybeStatesNotRelevant = goal.hasRelevantValues() && goal.relevantValues().isDisjointFrom(maybeStates); + // Check whether we need to compute exact rewards for some states. - if (qualitative) { + if (qualitative || maybeStatesNotRelevant) { // Set the values for all maybe-states to 1 to indicate that their reward values // are neither 0 nor infinity. storm::utility::vector::setVectorValues(result, maybeStates, storm::utility::one()); diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 38a84bd48..eb63176c6 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -606,8 +606,11 @@ namespace storm { scheduler = std::make_unique>(transitionMatrix.getRowGroupCount()); } + // Check if the values of the maybe states are relevant for the SolveGoal + bool maybeStatesNotRelevant = goal.hasRelevantValues() && goal.relevantValues().isDisjointFrom(qualitativeStateSets.maybeStates); + // Check whether we need to compute exact probabilities for some states. - if (qualitative) { + if (qualitative || maybeStatesNotRelevant) { // Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1. storm::utility::vector::setVectorValues(result, qualitativeStateSets.maybeStates, storm::utility::convertNumber(0.5)); } else { @@ -1091,8 +1094,11 @@ namespace storm { scheduler = std::make_unique>(transitionMatrix.getRowGroupCount()); } + // Check if the values of the maybe states are relevant for the SolveGoal + bool maybeStatesNotRelevant = goal.hasRelevantValues() && goal.relevantValues().isDisjointFrom(qualitativeStateSets.maybeStates); + // Check whether we need to compute exact rewards for some states. - if (qualitative) { + if (qualitative || maybeStatesNotRelevant) { STORM_LOG_INFO("The rewards for the initial states were determined in a preprocessing step. No exact rewards were computed."); // Set the values for all maybe-states to 1 to indicate that their reward values // are neither 0 nor infinity.