sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

fixed expected results which have been too imprecise for the LP-based MinMaxLinearEquationSolver

tempestpy_adaptions
TimQu 7 years ago
parent
6a986d2490
commit
31b5d77560
1 changed files with 9 additions and 9 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 18
      src/test/storm/modelchecker/LpMdpPrctlModelCheckerTest.cpp

18
src/test/storm/modelchecker/LpMdpPrctlModelCheckerTest.cpp
View File

@ -76,14 +76,14 @@ TEST(LpMdpPrctlModelCheckerTest, Dice) {
result = checker.check(*formula); result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult7 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult7 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.333329499, quantitativeResult7[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(7.333333333, quantitativeResult7[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
result = checker.check(*formula); result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult8 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult8 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.333329499, quantitativeResult8[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(7.333333333, quantitativeResult8[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().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", ""); 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); result = stateRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult9 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult9 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.333329499, quantitativeResult9[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(7.333333333, quantitativeResult9[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
result = stateRewardModelChecker.check(*formula); result = stateRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult10 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult10 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.333329499, quantitativeResult10[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(7.333333333, quantitativeResult10[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().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"); 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); result = stateAndTransitionRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult11 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult11 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(14.666658998, quantitativeResult11[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(14.666666666, quantitativeResult11[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
result = stateAndTransitionRewardModelChecker.check(*formula); result = stateAndTransitionRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult12 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult12 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(14.666658998, quantitativeResult12[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(14.666666666, quantitativeResult12[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
} }
TEST(LpMdpPrctlModelCheckerTest, AsynchronousLeader) { TEST(LpMdpPrctlModelCheckerTest, AsynchronousLeader) {
@ -177,15 +177,15 @@ TEST(LpMdpPrctlModelCheckerTest, AsynchronousLeader) {
result = checker.check(*formula); result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(4.285689611, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(4.285714286, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
result = checker.check(*formula); result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(4.285689611, quantitativeResult6[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(4.285714286, quantitativeResult6[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
} }
TEST(LpMdpPrctlModelCheckerTest, SchedulerGeneration) { TEST(LpMdpPrctlModelCheckerTest, SchedulerGeneration) {

Write Preview
Loading…
Cancel
Save