From 03bf55f4abf3514d11da379c73aed064e09547ff Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 3 Mar 2020 22:24:23 +0100 Subject: [PATCH] Bugfix in new unif+ implementation --- .../csl/helper/SparseMarkovAutomatonCslHelper.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 131c3cf44..39bfb81a4 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -54,6 +54,8 @@ namespace storm { storm::storage::BitVector maybeStates = ~(getProb0States(dir, phiStates, psiStates) | psiStates); storm::storage::BitVector markovianMaybeStates = markovianStates & maybeStates; storm::storage::BitVector probabilisticMaybeStates = ~markovianStates & maybeStates; + storm::storage::BitVector markovianStatesModMaybeStates = markovianMaybeStates % maybeStates; + storm::storage::BitVector probabilisticStatesModMaybeStates = probabilisticMaybeStates % maybeStates; // Catch the case where this is query can be solved by solving the untimed variant instead. // This is the case if there is no Markovian maybe state (e.g. if the initial state is already a psi state) of if the time bound is infinity. @@ -161,8 +163,8 @@ namespace storm { // Create the new values for the maybestates // Fuse the results together - storm::utility::vector::setVectorValues(maybeStatesValues, markovianMaybeStates, nextMarkovianStateValues); - storm::utility::vector::setVectorValues(maybeStatesValues, probabilisticMaybeStates, nextProbabilisticStateValues); + storm::utility::vector::setVectorValues(maybeStatesValues, markovianStatesModMaybeStates, nextMarkovianStateValues); + storm::utility::vector::setVectorValues(maybeStatesValues, probabilisticStatesModMaybeStates, nextProbabilisticStateValues); if (!computeLowerBound) { // Add the scaled values to the actual result vector uint64_t i = N-1-k;