From c672f7aea22f7b541c51becff3dc432b534210a2 Mon Sep 17 00:00:00 2001 From: TimQu Date: Sat, 9 Jul 2016 21:01:41 +0200 Subject: [PATCH] fix in bounded reachability computation with Markov automata Former-commit-id: fe2b39977886f2a3c4962341f3d4968bc61b1928 --- src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 7817dc644..90f858756 100644 --- a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -72,7 +72,7 @@ namespace storm { std::vector bMarkovian(markovianNonGoalStates.getNumberOfSetBits()); // Compute the two fixed right-hand side vectors, one for Markovian states and one for the probabilistic ones. - std::vector bProbabilisticFixed = transitionMatrix.getConstrainedRowSumVector(probabilisticNonGoalStates, goalStates); + std::vector bProbabilisticFixed = transitionMatrix.getConstrainedRowGroupSumVector(probabilisticNonGoalStates, goalStates); std::vector bMarkovianFixed; bMarkovianFixed.reserve(markovianNonGoalStates.getNumberOfSetBits()); for (auto state : markovianNonGoalStates) {