From 31b5d77560911ee9fe3c8f61d61a5e2b23ac0d82 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 2 Aug 2017 13:43:03 +0200 Subject: [PATCH] fixed expected results which have been too imprecise for the LP-based MinMaxLinearEquationSolver --- .../LpMdpPrctlModelCheckerTest.cpp | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/src/test/storm/modelchecker/LpMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/LpMdpPrctlModelCheckerTest.cpp index b1b0a884a..494516b0d 100644 --- a/src/test/storm/modelchecker/LpMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/LpMdpPrctlModelCheckerTest.cpp @@ -76,14 +76,14 @@ TEST(LpMdpPrctlModelCheckerTest, Dice) { result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult7 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(7.333329499, quantitativeResult7[0], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.333333333, quantitativeResult7[0], storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult8 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(7.333329499, quantitativeResult8[0], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.333333333, quantitativeResult8[0], storm::settings::getModule().getPrecision()); abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", ""); @@ -98,14 +98,14 @@ TEST(LpMdpPrctlModelCheckerTest, Dice) { result = stateRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult9 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(7.333329499, quantitativeResult9[0], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.333333333, quantitativeResult9[0], storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); result = stateRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult10 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(7.333329499, quantitativeResult10[0], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.333333333, quantitativeResult10[0], storm::settings::getModule().getPrecision()); abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew"); @@ -120,14 +120,14 @@ TEST(LpMdpPrctlModelCheckerTest, Dice) { result = stateAndTransitionRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult11 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(14.666658998, quantitativeResult11[0], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(14.666666666, quantitativeResult11[0], storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); result = stateAndTransitionRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult12 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(14.666658998, quantitativeResult12[0], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(14.666666666, quantitativeResult12[0], storm::settings::getModule().getPrecision()); } TEST(LpMdpPrctlModelCheckerTest, AsynchronousLeader) { @@ -177,15 +177,15 @@ TEST(LpMdpPrctlModelCheckerTest, AsynchronousLeader) { result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(4.285689611, quantitativeResult5[0], storm::settings::getModule().getPrecision()); + + EXPECT_NEAR(4.285714286, quantitativeResult5[0], storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(4.285689611, quantitativeResult6[0], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.285714286, quantitativeResult6[0], storm::settings::getModule().getPrecision()); } TEST(LpMdpPrctlModelCheckerTest, SchedulerGeneration) {