From 50087994f7129f41b3a62be79317c4a4d9fe311e Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Mon, 1 Mar 2021 18:12:07 +0100 Subject: [PATCH] fixed typo --- src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index f6b756352..f1be13d61 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -72,7 +72,7 @@ namespace storm { } template - 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) { + 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) { // the idea is to implement the definition of globally as in the formula: // 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