From b6ffa9a6497ce300d279d5424d73f91281b27f76 Mon Sep 17 00:00:00 2001 From: lukpo Date: Wed, 4 Aug 2021 14:33:17 +0200 Subject: [PATCH] small change in the comments of computeGloballyProbabilities --- src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 84b756dee..b3b89688e 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -81,9 +81,8 @@ namespace storm { template SMGSparseModelCheckingHelperReturnType 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) { - // the idea is to implement the definition of globally as in the formula: // G psi = 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 + // The psiStates are flipped, then the true U part is calculated, at the end the result is flipped again. storm::storage::BitVector notPsiStates = ~psiStates; statesOfCoalition.complement(); auto result = computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), notPsiStates, qualitative, statesOfCoalition, produceScheduler, hint);