From 5706831ad6070c28053ea4d657c1e56af098bee7 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 30 Aug 2018 14:28:31 +0200 Subject: [PATCH] fixing settings/tests --- .../settings/modules/AbstractionSettings.cpp | 4 + .../settings/modules/AbstractionSettings.h | 7 + .../storm/abstraction/PrismMenuGameTest.cpp | 148 ++++++++++++------ 3 files changed, 109 insertions(+), 50 deletions(-) diff --git a/src/storm/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp index ace89c635..682418169 100644 --- a/src/storm/settings/modules/AbstractionSettings.cpp +++ b/src/storm/settings/modules/AbstractionSettings.cpp @@ -180,6 +180,10 @@ namespace storm { this->getOption(addAllGuardsOptionName).getArgumentByName("value").setFromStringValue(value ? "on" : "off"); } + void AbstractionSettings::setAddAllInitialExpressions(bool value) { + this->getOption(addInitialExpressionsOptionName).getArgumentByName("value").setFromStringValue(value ? "on" : "off"); + } + bool AbstractionSettings::isUseInterpolationSet() const { return this->getOption(useInterpolationOptionName).getArgumentByName("value").getValueAsString() == "on"; } diff --git a/src/storm/settings/modules/AbstractionSettings.h b/src/storm/settings/modules/AbstractionSettings.h index 5e2e8fdbc..dbcaffd9d 100644 --- a/src/storm/settings/modules/AbstractionSettings.h +++ b/src/storm/settings/modules/AbstractionSettings.h @@ -76,6 +76,13 @@ namespace storm { */ void setAddAllGuards(bool value); + /*! + * Sets the option to add all initial expressions to the specified value. + * + * @param value The new value. + */ + void setAddAllInitialExpressions(bool value); + /*! * Retrieves whether the option to use interpolation was set. * diff --git a/src/test/storm/abstraction/PrismMenuGameTest.cpp b/src/test/storm/abstraction/PrismMenuGameTest.cpp index a200c1d68..5f9f86ddd 100644 --- a/src/test/storm/abstraction/PrismMenuGameTest.cpp +++ b/src/test/storm/abstraction/PrismMenuGameTest.cpp @@ -23,7 +23,9 @@ #include "storm/settings/modules/AbstractionSettings.h" TEST(PrismMenuGame, DieAbstractionTest_Cudd) { - storm::settings::mutableAbstractionSettings().setAddAllGuards(false); + auto& settings = storm::settings::mutableAbstractionSettings(); + settings.setAddAllGuards(false); + settings.setAddAllInitialExpressions(false); storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); @@ -47,8 +49,10 @@ TEST(PrismMenuGame, DieAbstractionTest_Cudd) { } TEST(PrismMenuGame, DieAbstractionTest_Sylvan) { - storm::settings::mutableAbstractionSettings().setAddAllGuards(false); - + auto& settings = storm::settings::mutableAbstractionSettings(); + settings.setAddAllGuards(false); + settings.setAddAllInitialExpressions(false); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); std::vector initialPredicates; @@ -97,8 +101,10 @@ TEST(PrismMenuGame, DieAbstractionTest_Sylvan) { #endif TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Cudd) { - storm::settings::mutableAbstractionSettings().setAddAllGuards(false); - + auto& settings = storm::settings::mutableAbstractionSettings(); + settings.setAddAllGuards(false); + settings.setAddAllInitialExpressions(false); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); std::vector initialPredicates; @@ -124,8 +130,10 @@ TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Cudd) { } TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Sylvan) { - storm::settings::mutableAbstractionSettings().setAddAllGuards(false); - + auto& settings = storm::settings::mutableAbstractionSettings(); + settings.setAddAllGuards(false); + settings.setAddAllInitialExpressions(false); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); std::vector initialPredicates; @@ -151,8 +159,10 @@ TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Sylvan) { } TEST(PrismMenuGame, DieFullAbstractionTest_Cudd) { - storm::settings::mutableAbstractionSettings().setAddAllGuards(false); - + auto& settings = storm::settings::mutableAbstractionSettings(); + settings.setAddAllGuards(false); + settings.setAddAllInitialExpressions(false); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); std::vector initialPredicates; @@ -191,8 +201,10 @@ TEST(PrismMenuGame, DieFullAbstractionTest_Cudd) { } TEST(PrismMenuGame, DieFullAbstractionTest_Sylvan) { - storm::settings::mutableAbstractionSettings().setAddAllGuards(false); - + auto& settings = storm::settings::mutableAbstractionSettings(); + settings.setAddAllGuards(false); + settings.setAddAllInitialExpressions(false); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); std::vector initialPredicates; @@ -231,8 +243,10 @@ TEST(PrismMenuGame, DieFullAbstractionTest_Sylvan) { } TEST(PrismMenuGame, CrowdsAbstractionTest_Cudd) { - storm::settings::mutableAbstractionSettings().setAddAllGuards(false); - + auto& settings = storm::settings::mutableAbstractionSettings(); + settings.setAddAllGuards(false); + settings.setAddAllInitialExpressions(false); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); program = program.substituteConstants(); @@ -257,8 +271,10 @@ TEST(PrismMenuGame, CrowdsAbstractionTest_Cudd) { } TEST(PrismMenuGame, CrowdsAbstractionTest_Sylvan) { - storm::settings::mutableAbstractionSettings().setAddAllGuards(false); - + auto& settings = storm::settings::mutableAbstractionSettings(); + settings.setAddAllGuards(false); + settings.setAddAllInitialExpressions(false); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); program = program.substituteConstants(); @@ -283,8 +299,10 @@ TEST(PrismMenuGame, CrowdsAbstractionTest_Sylvan) { } TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Cudd) { - storm::settings::mutableAbstractionSettings().setAddAllGuards(false); - + auto& settings = storm::settings::mutableAbstractionSettings(); + settings.setAddAllGuards(false); + settings.setAddAllInitialExpressions(false); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); program = program.substituteConstants(); @@ -311,8 +329,10 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Cudd) { } TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Sylvan) { - storm::settings::mutableAbstractionSettings().setAddAllGuards(false); - + auto& settings = storm::settings::mutableAbstractionSettings(); + settings.setAddAllGuards(false); + settings.setAddAllInitialExpressions(false); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); program = program.substituteConstants(); @@ -339,8 +359,10 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Sylvan) { } TEST(PrismMenuGame, CrowdsFullAbstractionTest_Cudd) { - storm::settings::mutableAbstractionSettings().setAddAllGuards(false); - + auto& settings = storm::settings::mutableAbstractionSettings(); + settings.setAddAllGuards(false); + settings.setAddAllInitialExpressions(false); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); program = program.substituteConstants(); @@ -419,8 +441,10 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest_Cudd) { } TEST(PrismMenuGame, CrowdsFullAbstractionTest_Sylvan) { - storm::settings::mutableAbstractionSettings().setAddAllGuards(false); - + auto& settings = storm::settings::mutableAbstractionSettings(); + settings.setAddAllGuards(false); + settings.setAddAllInitialExpressions(false); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); program = program.substituteConstants(); @@ -499,8 +523,10 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest_Sylvan) { } TEST(PrismMenuGame, TwoDiceAbstractionTest_Cudd) { - storm::settings::mutableAbstractionSettings().setAddAllGuards(false); - + auto& settings = storm::settings::mutableAbstractionSettings(); + settings.setAddAllGuards(false); + settings.setAddAllInitialExpressions(false); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); program = program.substituteConstants(); program = program.flattenModules(std::make_shared()); @@ -527,8 +553,10 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest_Cudd) { } TEST(PrismMenuGame, TwoDiceAbstractionTest_Sylvan) { - storm::settings::mutableAbstractionSettings().setAddAllGuards(false); - + auto& settings = storm::settings::mutableAbstractionSettings(); + settings.setAddAllGuards(false); + settings.setAddAllInitialExpressions(false); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); program = program.substituteConstants(); program = program.flattenModules(std::make_shared()); @@ -555,8 +583,10 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest_Sylvan) { } TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Cudd) { - storm::settings::mutableAbstractionSettings().setAddAllGuards(false); - + auto& settings = storm::settings::mutableAbstractionSettings(); + settings.setAddAllGuards(false); + settings.setAddAllInitialExpressions(false); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); program = program.substituteConstants(); program = program.flattenModules(std::make_shared()); @@ -585,8 +615,10 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Cudd) { } TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Sylvan) { - storm::settings::mutableAbstractionSettings().setAddAllGuards(false); - + auto& settings = storm::settings::mutableAbstractionSettings(); + settings.setAddAllGuards(false); + settings.setAddAllInitialExpressions(false); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); program = program.substituteConstants(); program = program.flattenModules(std::make_shared()); @@ -615,8 +647,10 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Sylvan) { } TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Cudd) { - storm::settings::mutableAbstractionSettings().setAddAllGuards(false); - + auto& settings = storm::settings::mutableAbstractionSettings(); + settings.setAddAllGuards(false); + settings.setAddAllInitialExpressions(false); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); program = program.substituteConstants(); program = program.flattenModules(std::make_shared()); @@ -674,8 +708,10 @@ TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Cudd) { } TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Sylvan) { - storm::settings::mutableAbstractionSettings().setAddAllGuards(false); - + auto& settings = storm::settings::mutableAbstractionSettings(); + settings.setAddAllGuards(false); + settings.setAddAllInitialExpressions(false); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); program = program.substituteConstants(); program = program.flattenModules(std::make_shared()); @@ -733,8 +769,10 @@ TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Sylvan) { } TEST(PrismMenuGame, WlanAbstractionTest_Cudd) { - storm::settings::mutableAbstractionSettings().setAddAllGuards(false); - + auto& settings = storm::settings::mutableAbstractionSettings(); + settings.setAddAllGuards(false); + settings.setAddAllInitialExpressions(false); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm"); program = program.substituteConstants(); program = program.flattenModules(std::make_shared()); @@ -754,7 +792,7 @@ TEST(PrismMenuGame, WlanAbstractionTest_Cudd) { storm::abstraction::MenuGame game = abstractor.abstract(); - EXPECT_EQ(915ull, game.getNumberOfTransitions()); + EXPECT_EQ(903ull, game.getNumberOfTransitions()); EXPECT_EQ(8ull, game.getNumberOfStates()); EXPECT_EQ(4ull, game.getBottomStates().getNonZeroCount()); @@ -762,8 +800,10 @@ TEST(PrismMenuGame, WlanAbstractionTest_Cudd) { } TEST(PrismMenuGame, WlanAbstractionTest_Sylvan) { - storm::settings::mutableAbstractionSettings().setAddAllGuards(false); - + auto& settings = storm::settings::mutableAbstractionSettings(); + settings.setAddAllGuards(false); + settings.setAddAllInitialExpressions(false); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm"); program = program.substituteConstants(); program = program.flattenModules(std::make_shared()); @@ -783,7 +823,7 @@ TEST(PrismMenuGame, WlanAbstractionTest_Sylvan) { storm::abstraction::MenuGame game = abstractor.abstract(); - EXPECT_EQ(915ull, game.getNumberOfTransitions()); + EXPECT_EQ(903ull, game.getNumberOfTransitions()); EXPECT_EQ(8ull, game.getNumberOfStates()); EXPECT_EQ(4ull, game.getBottomStates().getNonZeroCount()); @@ -791,7 +831,9 @@ TEST(PrismMenuGame, WlanAbstractionTest_Sylvan) { } TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Cudd) { - storm::settings::mutableAbstractionSettings().setAddAllGuards(false); + auto& settings = storm::settings::mutableAbstractionSettings(); + settings.setAddAllGuards(false); + settings.setAddAllInitialExpressions(false); storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm"); program = program.substituteConstants(); @@ -814,7 +856,7 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Cudd) { storm::abstraction::MenuGame game = abstractor.abstract(); - EXPECT_EQ(1824ull, game.getNumberOfTransitions()); + EXPECT_EQ(1800ull, game.getNumberOfTransitions()); EXPECT_EQ(16ull, game.getNumberOfStates()); EXPECT_EQ(8ull, game.getBottomStates().getNonZeroCount()); @@ -822,8 +864,10 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Cudd) { } TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Sylvan) { - storm::settings::mutableAbstractionSettings().setAddAllGuards(false); - + auto& settings = storm::settings::mutableAbstractionSettings(); + settings.setAddAllGuards(false); + settings.setAddAllInitialExpressions(false); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm"); program = program.substituteConstants(); program = program.flattenModules(std::make_shared()); @@ -845,7 +889,7 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Sylvan) { storm::abstraction::MenuGame game = abstractor.abstract(); - EXPECT_EQ(1824ull, game.getNumberOfTransitions()); + EXPECT_EQ(1800ull, game.getNumberOfTransitions()); EXPECT_EQ(16ull, game.getNumberOfStates()); EXPECT_EQ(8ull, game.getBottomStates().getNonZeroCount()); @@ -853,8 +897,10 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Sylvan) { } TEST(PrismMenuGame, WlanFullAbstractionTest_Cudd) { - storm::settings::mutableAbstractionSettings().setAddAllGuards(false); - + auto& settings = storm::settings::mutableAbstractionSettings(); + settings.setAddAllGuards(false); + settings.setAddAllInitialExpressions(false); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm"); program = program.substituteConstants(); program = program.flattenModules(std::make_shared()); @@ -980,8 +1026,10 @@ TEST(PrismMenuGame, WlanFullAbstractionTest_Cudd) { } TEST(PrismMenuGame, WlanFullAbstractionTest_Sylvan) { - storm::settings::mutableAbstractionSettings().setAddAllGuards(false); - + auto& settings = storm::settings::mutableAbstractionSettings(); + settings.setAddAllGuards(false); + settings.setAddAllInitialExpressions(false); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm"); program = program.substituteConstants(); program = program.flattenModules(std::make_shared());