From fb84fc6af0ccd50344438c75bed484cb56ddaa39 Mon Sep 17 00:00:00 2001 From: lukpo Date: Tue, 10 Aug 2021 10:14:12 +0200 Subject: [PATCH] Added a comment why this computeBoundedGlobally check happens. --- src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index e28d591e0..527bb07e0 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -218,6 +218,7 @@ namespace storm { storm::utility::vector::setVectorValues(result, relevantStates, x); } + // In bounded-globally formulas we not only to reach a psiState on the path but also want to stay in a set of psiStates in the given step bounds. if(!computeBoundedGlobally){ storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); }