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;