diff --git a/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index e771b3e0a..f0858e2ca 100644 --- a/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -242,9 +242,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) { EXPECT_EQ(0ull, scheduler2.getChoice(3).getDeterministicChoice()); } -// Test is currently disabled as the computation of this property requires eliminating the zero-reward MECs, which is -// currently not implemented and also not supported by PRISM. -TEST(DISABLED_GmmxxMdpPrctlModelCheckerTest, TinyRewards) { +TEST(GmmxxMdpPrctlModelCheckerTest, TinyRewards) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/tiny_rewards.nm"); // A parser that we use for conveniently constructing the formulas. diff --git a/src/test/storm/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp index d5906064e..ebeb02282 100644 --- a/src/test/storm/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp @@ -103,8 +103,8 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Cudd) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult7 = result->asSymbolicQuantitativeCheckResult(); - EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMax(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.3333317041397095, quantitativeResult7.getMin(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.3333317041397095, quantitativeResult7.getMax(), storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); @@ -201,8 +201,8 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Sylvan) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult7 = result->asSymbolicQuantitativeCheckResult(); - EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMax(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.3333317041397095, quantitativeResult7.getMin(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.3333317041397095, quantitativeResult7.getMax(), storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); @@ -281,8 +281,8 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult(); - EXPECT_NEAR(4.2856890848060498, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.2856890848060498, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.2856904569131631, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.2856904569131631, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");