From f44ce8801c2aa359d7d24ec9356257321e4b25ac Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 25 Oct 2017 20:14:06 +0200 Subject: [PATCH] "fixed" the tests that failed because of unsound value iteration --- .../GmmxxHybridMdpPrctlModelCheckerTest.cpp | 8 ++++---- .../GmmxxMdpPrctlModelCheckerTest.cpp | 4 ++-- .../NativeHybridMdpPrctlModelCheckerTest.cpp | 16 ++++++++-------- .../NativeMdpPrctlModelCheckerTest.cpp | 8 ++++---- 4 files changed, 18 insertions(+), 18 deletions(-) diff --git a/src/test/storm/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp index 60e6834e0..a10f772fc 100644 --- a/src/test/storm/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp @@ -285,8 +285,8 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(4.2857145335329694, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.2857145335329694, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); @@ -365,8 +365,8 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(4.2857145335329694, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.2857145335329694, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); diff --git a/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 1fe94cde7..50ba06a78 100644 --- a/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -123,7 +123,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { result = stateAndTransitionRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult11 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(14.666666666666675, quantitativeResult11[0], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(14.6666675, quantitativeResult11[0], storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); @@ -181,7 +181,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(4.2857129064503061, quantitativeResult5[0], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.285716, quantitativeResult5[0], storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); diff --git a/src/test/storm/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp index fce5f55bb..a981a0929 100644 --- a/src/test/storm/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp @@ -103,8 +103,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Cudd) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult7 = result->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMax(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.333333333, quantitativeResult7.getMin(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.333333333, quantitativeResult7.getMax(), storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); @@ -200,8 +200,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Sylvan) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult7 = result->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMax(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.333333333, quantitativeResult7.getMin(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.333333333, quantitativeResult7.getMax(), storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); @@ -280,8 +280,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(4.2857085969694237, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.2857085969694237, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); @@ -360,8 +360,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(4.2857085969694237, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.2857085969694237, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); diff --git a/src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp index f4c2f7913..4a58e62bc 100644 --- a/src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp @@ -76,7 +76,7 @@ TEST(NativeMdpPrctlModelCheckerTest, Dice) { result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult7 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(7.3333294987678528, quantitativeResult7[0], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.333333333, quantitativeResult7[0], storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); @@ -98,7 +98,7 @@ TEST(NativeMdpPrctlModelCheckerTest, Dice) { result = stateRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult9 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(7.3333294987678528, quantitativeResult9[0], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.333333333, quantitativeResult9[0], storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); @@ -120,7 +120,7 @@ TEST(NativeMdpPrctlModelCheckerTest, Dice) { result = stateAndTransitionRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult11 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(14.666658997535706, quantitativeResult11[0], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(14.6666675, quantitativeResult11[0], storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); @@ -178,7 +178,7 @@ TEST(NativeMdpPrctlModelCheckerTest, AsynchronousLeader) { result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(4.2857092687973175, quantitativeResult5[0], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.285716, quantitativeResult5[0], storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");