From a86426211ce1d34697d9146fd6d84d8f0a09be10 Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Wed, 3 Mar 2021 17:52:33 +0100 Subject: [PATCH] changed statesOfCoalition --- .../modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 710362961..779392a3e 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -92,10 +92,7 @@ namespace storm { storm::storage::BitVector allStates = storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true); std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(allStates, psiStates); - // coalition handling for all states - storm::storage::BitVector clippedStatesOfCoalition(transitionMatrix.getRowGroupCount()); - clippedStatesOfCoalition.setClippedStatesOfCoalition(allStates, statesOfCoalition); - clippedStatesOfCoalition.complement(); + statesOfCoalition.complement(); if (produceScheduler) { STORM_LOG_WARN("Next formula does not expect that produceScheduler is set to true."); @@ -105,7 +102,7 @@ namespace storm { auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); multiplier->multiplyAndReduce(env, goal.direction(), x, &b, x, nullptr, &statesOfCoalition); - //STORM_LOG_DEBUG("x = " << storm::utility::vector::toString(x)); + STORM_LOG_DEBUG("x = " << storm::utility::vector::toString(x)); return MDPSparseModelCheckingHelperReturnType(std::move(x)); }