From 8df4a99770d2aeb83eab97c17718ac40ac0e0ea8 Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Mon, 8 Mar 2021 17:54:46 +0100 Subject: [PATCH] small changes, but did not fix the bug --- src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp | 4 ++-- .../rpatl/helper/internal/BoundedGloballyGameViHelper.cpp | 4 +--- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 094f36f18..7fb39bf1d 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -120,7 +120,7 @@ namespace storm { std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, relevantStates); // Reduce the matrix to relevant states - storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, true); + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); storm::storage::BitVector clippedStatesOfCoalition(relevantStates.getNumberOfSetBits()); clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition); @@ -133,7 +133,7 @@ namespace storm { viHelper.setProduceScheduler(true); } - // TODO: the lower bounds are not used at the moment + // TODO: the lower bounds are not used if(lowerBound != 0) { STORM_LOG_WARN("The use of lower bounds is not implemented for bounded globally formulas."); diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp index 5ad26ce62..177301730 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp @@ -36,9 +36,7 @@ namespace storm { this->_producedOptimalChoices->resize(this->_transitionMatrix.getRowGroupCount()); } - uint64_t iter = 0; - while (iter < upperBound) { - ++iter; + for (uint64_t iter = 0; iter < upperBound; iter++) { performIterationStep(env, dir);