From fde78ad7597057ba2c82ea59f2aa7c43a9efb3a5 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 2 Dec 2013 17:25:48 +0100 Subject: [PATCH] Bugfix for matrix creation in LRA computation. Former-commit-id: cb4c9cb7286048847fb3d7ebd1cae24c9cd61228 --- .../csl/SparseMarkovAutomatonCslModelChecker.h | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index c040b92ed..8077086bb 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -312,7 +312,7 @@ namespace storm { for (auto element : row) { if (statesNotContainedInAnyMec.get(element.column())) { // If the target state is not contained in an MEC, we can copy over the entry. - sspMatrix.insertNextValue(currentChoice, statesNotInMecsBeforeIndex[element.column()], element.value()); + sspMatrix.insertNextValue(currentChoice, statesNotInMecsBeforeIndex[element.column()], element.value(), true); } else { // If the target state is contained in MEC i, we need to add the probability to the corresponding field in the vector // so that we are able to write the cumulative probability to the MEC into the matrix. @@ -323,7 +323,7 @@ namespace storm { // Now insert all (cumulative) probability values that target an MEC. for (uint_fast64_t mecIndex = 0; mecIndex < auxiliaryStateToProbabilityMap.size(); ++mecIndex) { if (auxiliaryStateToProbabilityMap[mecIndex] != 0) { - sspMatrix.insertNextValue(currentChoice, firstAuxiliaryStateIndex + mecIndex, auxiliaryStateToProbabilityMap[mecIndex]); + sspMatrix.insertNextValue(currentChoice, firstAuxiliaryStateIndex + mecIndex, auxiliaryStateToProbabilityMap[mecIndex], true); } } } @@ -349,7 +349,7 @@ namespace storm { for (auto element : row) { if (statesNotContainedInAnyMec.get(element.column())) { // If the target state is not contained in an MEC, we can copy over the entry. - sspMatrix.insertNextValue(currentChoice, statesNotInMecsBeforeIndex[element.column()], element.value()); + sspMatrix.insertNextValue(currentChoice, statesNotInMecsBeforeIndex[element.column()], element.value(), true); } else { // If the target state is contained in MEC i, we need to add the probability to the corresponding field in the vector // so that we are able to write the cumulative probability to the MEC into the matrix. @@ -366,7 +366,7 @@ namespace storm { b.back() += auxiliaryStateToProbabilityMap[mecIndex] * lraValuesForEndComponents[mecIndex]; } else { // Otherwise, we add a transition to the auxiliary state that is associated with the target MEC. - sspMatrix.insertNextValue(currentChoice, firstAuxiliaryStateIndex + targetMecIndex, auxiliaryStateToProbabilityMap[targetMecIndex]); + sspMatrix.insertNextValue(currentChoice, firstAuxiliaryStateIndex + targetMecIndex, auxiliaryStateToProbabilityMap[targetMecIndex], true); } } }