diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 286a5ed60..f6b756352 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -72,15 +72,12 @@ namespace storm { } template - MDPSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) { + MDPSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::v(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) { // the idea is to implement the definition of globally as in the formula: - // G phi = not(F(not phi)) = not(true U (not phi)) - // so the phiStates are flipped, then the true U part is calculated, at the end the result is flipped again + // G phi = not(F(not psi)) = not(true U (not psi)) + // so the psiStates are flipped, then the true U part is calculated, at the end the result is flipped again storm::storage::BitVector notPsiStates = ~psiStates; - //goal.oneMinus(); statesOfCoalition.complement(); - //STORM_LOG_DEBUG(storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true)); - //STORM_LOG_DEBUG(psiStates); auto result = computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), notPsiStates, qualitative, statesOfCoalition, produceScheduler, hint); for (auto& element : result.values) { element = storm::utility::one() - element;