From 734599c11495cb9c4a94deb28d5f97051906ec73 Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Mon, 22 Feb 2021 12:11:21 +0100 Subject: [PATCH] correction of globally functionality --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index be91ecd02..286a5ed60 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -73,14 +73,15 @@ 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) { - // TODO: the inputs are copied from until, check which of them are used - // - there is no leftsubformula, so there is no phiStates (as Input) - // - what about this "hint"? - - // TODO: SparseMdpPrctlHelper uses "useMecBasedTechnique" - should I pay attention to that? - - goal.oneMinus(); - auto result = computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), psiStates, qualitative, statesOfCoalition, produceScheduler, 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 + 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; }