Bugfix and test-fix: Only the "never leave MEC"-states have cost > 0 and transition costs are all 0 in the ssp.

Former-commit-id: f6688a8956

src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp

@@ -354,14 +354,7 @@ namespace storm {
                             // Now insert all (cumulative) probability values that target an MEC.
                             for (uint_fast64_t targetMecIndex = 0; targetMecIndex < auxiliaryStateToProbabilityMap.size(); ++targetMecIndex) {
                                 if (auxiliaryStateToProbabilityMap[targetMecIndex] != 0) {
-                                    // If the target MEC is the same as the current one, instead of adding a transition, we need to add the weighted reward
-                                    // to the right-hand side vector of the SSP.
-                                    if (mecIndex == targetMecIndex) {
-                                        b.back() += auxiliaryStateToProbabilityMap[mecIndex] * lraValuesForEndComponents[mecIndex];
-                                    } else {
-                                        // Otherwise, we add a transition to the auxiliary state that is associated with the target MEC.
-                                        sspMatrixBuilder.addNextValue(currentChoice, firstAuxiliaryStateIndex + targetMecIndex, auxiliaryStateToProbabilityMap[targetMecIndex]);
-                                    }
+                                    sspMatrixBuilder.addNextValue(currentChoice, firstAuxiliaryStateIndex + targetMecIndex, auxiliaryStateToProbabilityMap[targetMecIndex]);
                                 }
                             }
                             

src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@@ -440,14 +440,7 @@ namespace storm {
 							// Now insert all (cumulative) probability values that target an MEC.
 							for (uint_fast64_t targetMecIndex = 0; targetMecIndex < auxiliaryStateToProbabilityMap.size(); ++targetMecIndex) {
 								if (auxiliaryStateToProbabilityMap[targetMecIndex] != 0) {
-									// If the target MEC is the same as the current one, instead of adding a transition, we need to add the weighted reward
-									// to the right-hand side vector of the SSP.
-									if (mecIndex == targetMecIndex) {
-										b.back() += auxiliaryStateToProbabilityMap[mecIndex] * lraValuesForEndComponents[mecIndex];
-									} else {
-										// Otherwise, we add a transition to the auxiliary state that is associated with the target MEC.
-										sspMatrixBuilder.addNextValue(currentChoice, firstAuxiliaryStateIndex + targetMecIndex, auxiliaryStateToProbabilityMap[targetMecIndex]);
-									}
+									sspMatrixBuilder.addNextValue(currentChoice, firstAuxiliaryStateIndex + targetMecIndex, auxiliaryStateToProbabilityMap[targetMecIndex]);
 								}
 							}
 

test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp

@@ -518,12 +518,12 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
 		result = std::move(checker.check(*lraFormula));
 		storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
 
-		EXPECT_NEAR(1./3., quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
-		EXPECT_NEAR(0.4, quantitativeResult2[3], storm::settings::nativeEquationSolverSettings().getPrecision());
+		EXPECT_NEAR(0.3 / 3., quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
+		EXPECT_NEAR(0.0, quantitativeResult2[3], storm::settings::nativeEquationSolverSettings().getPrecision());
 		EXPECT_NEAR(1./3., quantitativeResult2[6], storm::settings::nativeEquationSolverSettings().getPrecision());
 		EXPECT_NEAR(0.0, quantitativeResult2[9], storm::settings::nativeEquationSolverSettings().getPrecision());
-		EXPECT_NEAR(.26, quantitativeResult2[12], storm::settings::nativeEquationSolverSettings().getPrecision());
-		EXPECT_NEAR(467./1500., quantitativeResult2[13], storm::settings::nativeEquationSolverSettings().getPrecision());
-		EXPECT_NEAR(.26, quantitativeResult2[14], storm::settings::nativeEquationSolverSettings().getPrecision());
+		EXPECT_NEAR(0.3 / 3., quantitativeResult2[12], storm::settings::nativeEquationSolverSettings().getPrecision());
+		EXPECT_NEAR(.79 / 3., quantitativeResult2[13], storm::settings::nativeEquationSolverSettings().getPrecision());
+		EXPECT_NEAR(0.3 / 3., quantitativeResult2[14], storm::settings::nativeEquationSolverSettings().getPrecision());
 	}
 }