From c624b194271545906f3e1d4a90c0e6429dc05b96 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 22 Sep 2015 19:02:05 +0200 Subject: [PATCH] added no-cuts option. prob1 tests for game now passing. Former-commit-id: 3806747948377378e393f2a78a05b3692b93e7dc --- src/builder/DdPrismModelBuilder.cpp | 5 + src/builder/ExplicitPrismModelBuilder.cpp | 6 + src/settings/Option.cpp | 4 +- src/settings/modules/GeneralSettings.cpp | 10 +- src/settings/modules/GeneralSettings.h | 8 + src/utility/graph.cpp | 3 +- .../abstraction/PrismMenuGameTest.cpp | 14 +- test/functional/builder/wlan0-2-4.nm | 114 ++++++++++++++ test/functional/utility/GraphTest.cpp | 146 ++++++++++++++++++ 9 files changed, 298 insertions(+), 12 deletions(-) create mode 100644 test/functional/builder/wlan0-2-4.nm diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index 4f6ab3871..721a92480 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -254,6 +254,11 @@ namespace storm { template void DdPrismModelBuilder::Options::setTerminalStatesFromFormula(storm::logic::Formula const& formula) { + // If cutting the model was disabled, we do not set anything. + if (storm::settings::generalSettings().isNoCutsSet()) { + return; + } + if (formula.isAtomicExpressionFormula()) { terminalStates = formula.asAtomicExpressionFormula().getExpression(); } else if (formula.isAtomicLabelFormula()) { diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index cfc7d8577..aa873f618 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -113,6 +113,7 @@ namespace storm { template ExplicitPrismModelBuilder::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set()), expressionLabels(std::vector()), terminalStates(), negatedTerminalStates() { this->preserveFormula(formula); + this->setTerminalStatesFromFormula(formula); } template @@ -132,6 +133,11 @@ namespace storm { template void ExplicitPrismModelBuilder::Options::setTerminalStatesFromFormula(storm::logic::Formula const& formula) { + // If cutting the model was disabled, we do not set anything. + if (storm::settings::generalSettings().isNoCutsSet()) { + return; + } + if (formula.isAtomicExpressionFormula()) { terminalStates = formula.asAtomicExpressionFormula().getExpression(); } else if (formula.isAtomicLabelFormula()) { diff --git a/src/settings/Option.cpp b/src/settings/Option.cpp index b5cba7759..d011de507 100644 --- a/src/settings/Option.cpp +++ b/src/settings/Option.cpp @@ -115,10 +115,10 @@ namespace storm { STORM_LOG_THROW(!longName.empty(), storm::exceptions::IllegalArgumentException, "Unable to construct option with empty name."); STORM_LOG_THROW(!moduleName.empty(), storm::exceptions::IllegalArgumentException, "Unable to construct option with empty module name."); - bool longNameContainsNonAlpha = std::find_if(longName.begin(), longName.end(), [](char c) { return !(std::isalpha(c) || std::isdigit(c)); }) != longName.end(); + bool longNameContainsNonAlpha = std::find_if(longName.begin(), longName.end(), [](char c) { return !(std::isalpha(c) || std::isdigit(c) || c == '-'); }) != longName.end(); STORM_LOG_THROW(!longNameContainsNonAlpha, storm::exceptions::IllegalArgumentException, "Unable to construct option with illegal long name '" << longName << "'."); - bool shortNameContainsNonAlpha = std::find_if(shortName.begin(), shortName.end(), [](char c) { return !(std::isalpha(c) || std::isdigit(c)); }) != shortName.end(); + bool shortNameContainsNonAlpha = std::find_if(shortName.begin(), shortName.end(), [](char c) { return !(std::isalpha(c) || std::isdigit(c) || c == '-'); }) != shortName.end(); STORM_LOG_THROW(!shortNameContainsNonAlpha, storm::exceptions::IllegalArgumentException, "Unable to construct option with illegal short name '" << shortName << "'."); // Then index all arguments. diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp index 893dd4717..5faea4ed2 100644 --- a/src/settings/modules/GeneralSettings.cpp +++ b/src/settings/modules/GeneralSettings.cpp @@ -36,7 +36,8 @@ namespace storm { const std::string GeneralSettings::choiceLabelingOptionName = "choicelab"; const std::string GeneralSettings::counterexampleOptionName = "counterexample"; const std::string GeneralSettings::counterexampleOptionShortName = "cex"; - const std::string GeneralSettings::dontFixDeadlockOptionName = "nofixdl"; + const std::string GeneralSettings::noCutsOptionName = "no-cuts"; + const std::string GeneralSettings::dontFixDeadlockOptionName = "no-fixdl"; const std::string GeneralSettings::dontFixDeadlockOptionShortName = "ndl"; const std::string GeneralSettings::timeoutOptionName = "timeout"; const std::string GeneralSettings::timeoutOptionShortName = "t"; @@ -88,7 +89,8 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the state rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, choiceLabelingOptionName, false, "If given, the choice labels are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the choice labels.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, dontFixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(dontFixDeadlockOptionShortName).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, noCutsOptionName, false, "Do not perform cuts when buildings the state space.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, dontFixDeadlockOptionName, false, "If the model contains deadlock states, this flag disables automatically fixing them.").setShortName(dontFixDeadlockOptionShortName).build()); std::vector engines = {"sparse", "hybrid", "dd"}; this->addOption(storm::settings::OptionBuilder(moduleName, engineOptionName, false, "Sets which engine is used for model building and model checking.").setShortName(engineOptionShortName) @@ -220,6 +222,10 @@ namespace storm { return this->getOption(dontFixDeadlockOptionName).getHasOptionBeenSet(); } + bool GeneralSettings::isNoCutsSet() const { + return this->getOption(noCutsOptionName).getHasOptionBeenSet(); + } + std::unique_ptr GeneralSettings::overrideDontFixDeadlocksSet(bool stateToSet) { return this->overrideOption(dontFixDeadlockOptionName, stateToSet); } diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h index 1c7abdc98..39ba1e4f6 100644 --- a/src/settings/modules/GeneralSettings.h +++ b/src/settings/modules/GeneralSettings.h @@ -215,6 +215,13 @@ namespace storm { * @return True if the dont-fix-deadlocks option was set. */ bool isDontFixDeadlocksSet() const; + + /*! + * Retrieves whether the no-cuts option was set. + * + * @return True if the no-cuts option was set. + */ + bool isNoCutsSet() const; /*! * Overrides the option to not fix deadlocks by setting it to the specified value. As soon as the @@ -384,6 +391,7 @@ namespace storm { static const std::string choiceLabelingOptionName; static const std::string counterexampleOptionName; static const std::string counterexampleOptionShortName; + static const std::string noCutsOptionName; static const std::string dontFixDeadlockOptionName; static const std::string dontFixDeadlockOptionShortName; static const std::string timeoutOptionName; diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp index 34e10467d..1d0e850da 100644 --- a/src/utility/graph.cpp +++ b/src/utility/graph.cpp @@ -824,7 +824,8 @@ namespace storm { } } - // Add psi states to result. + // Explicitly add psi states to result since they may have transitions going to some state that + // does not have a reachability probability of 1. valid |= psiStates; // If no new states were added, we have found the current hypothesis for the states with diff --git a/test/functional/abstraction/PrismMenuGameTest.cpp b/test/functional/abstraction/PrismMenuGameTest.cpp index 30b55e863..6425c05b7 100644 --- a/test/functional/abstraction/PrismMenuGameTest.cpp +++ b/test/functional/abstraction/PrismMenuGameTest.cpp @@ -280,7 +280,7 @@ TEST(PrismMenuGame, TwoDiceFullAbstractionTest) { } TEST(PrismMenuGame, WlanAbstractionTest) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-4.nm"); program = program.substituteConstants(); program = program.flattenModules(std::make_unique()); @@ -295,12 +295,12 @@ TEST(PrismMenuGame, WlanAbstractionTest) { storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(277, game.getNumberOfTransitions()); + EXPECT_EQ(279, game.getNumberOfTransitions()); EXPECT_EQ(4, game.getNumberOfStates()); } TEST(PrismMenuGame, WlanAbstractionAndRefinementTest) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-4.nm"); program = program.substituteConstants(); program = program.flattenModules(std::make_unique()); @@ -317,12 +317,12 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest) { storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(556, game.getNumberOfTransitions()); + EXPECT_EQ(560, game.getNumberOfTransitions()); EXPECT_EQ(8, game.getNumberOfStates()); } TEST(PrismMenuGame, WlanFullAbstractionTest) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-4.nm"); program = program.substituteConstants(); program = program.flattenModules(std::make_unique()); @@ -435,8 +435,8 @@ TEST(PrismMenuGame, WlanFullAbstractionTest) { storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(59, game.getNumberOfTransitions()); - EXPECT_EQ(37, game.getNumberOfStates()); + EXPECT_EQ(9503, game.getNumberOfTransitions()); + EXPECT_EQ(5523, game.getNumberOfStates()); } #endif \ No newline at end of file diff --git a/test/functional/builder/wlan0-2-4.nm b/test/functional/builder/wlan0-2-4.nm new file mode 100644 index 000000000..136be18c5 --- /dev/null +++ b/test/functional/builder/wlan0-2-4.nm @@ -0,0 +1,114 @@ +mdp +const int COL = 2; +const int ASLOTTIME = 1; +const int DIFS = 3; +const int VULN = 1; +const int TRANS_TIME_MAX = 4; +const int TRANS_TIME_MIN = 4; +const int ACK_TO = 6; +const int ACK = 4; +const int SIFS = 1; +const int TIME_MAX = ((max(6, 4)) + 1); +const int MAX_BACKOFF = 0; + + +formula busy = ((c1 > 0) | (c2 > 0)); +formula free = ((c1 = 0) & (c2 = 0)); + +module medium + col: [0..2] init 0; + c1: [0..2] init 0; + c2: [0..2] init 0; + [send1] ((c1 = 0) & (c2 = 0)) -> 1 : (c1' = 1); + [send2] ((c2 = 0) & (c1 = 0)) -> 1 : (c2' = 1); + [send1] ((c1 = 0) & (c2 > 0)) -> 1 : (col' = (min((col + 1), 2))) & (c1' = 2) & (c2' = 2); + [send2] ((c2 = 0) & (c1 > 0)) -> 1 : (col' = (min((col + 1), 2))) & (c1' = 2) & (c2' = 2); + [finish1] (c1 > 0) -> 1 : (c1' = 0); + [finish2] (c2 > 0) -> 1 : (c2' = 0); +endmodule + +module station1 + x1: [0..((max(6, 4)) + 1)] init 0; + s1: [1..12] init 1; + slot1: [0..1] init 0; + backoff1: [0..15] init 0; + bc1: [0..1] init 0; + [time] (((s1 = 1) & (x1 < 3)) & ((c1 = 0) & (c2 = 0))) -> 1 : (x1' = (min((x1 + 1), 7))); + [] ((s1 = 1) & ((x1 = 3) | (x1 = 2))) -> 1 : (x1' = 0) & (s1' = 8); + [] ((s1 = 1) & ((c1 > 0) | (c2 > 0))) -> 1 : (x1' = 0) & (s1' = 2); + [time] ((s1 = 2) & ((c1 > 0) | (c2 > 0))) -> 1 : (s1' = 2); + [] ((s1 = 2) & ((c1 = 0) & (c2 = 0))) -> 1 : (s1' = 3); + [time] (((s1 = 3) & (x1 < 3)) & ((c1 = 0) & (c2 = 0))) -> 1 : (x1' = (min((x1 + 1), 7))); + [] ((s1 = 3) & ((c1 > 0) | (c2 > 0))) -> 1 : (x1' = 0) & (s1' = 2); + [] (((s1 = 3) & ((x1 = 3) | (x1 = 2))) & (bc1 = 0)) -> 1 : (x1' = 0) & (s1' = 4) & (slot1' = 0) & (bc1' = (min((bc1 + 1), 0))); + [] (s1 = 4) -> (1 / 16) : (s1' = 5) & (backoff1' = 0) + (1 / 16) : (s1' = 5) & (backoff1' = 1) + (1 / 16) : (s1' = 5) & (backoff1' = 2) + (1 / 16) : (s1' = 5) & (backoff1' = 3) + (1 / 16) : (s1' = 5) & (backoff1' = 4) + (1 / 16) : (s1' = 5) & (backoff1' = 5) + (1 / 16) : (s1' = 5) & (backoff1' = 6) + (1 / 16) : (s1' = 5) & (backoff1' = 7) + (1 / 16) : (s1' = 5) & (backoff1' = 8) + (1 / 16) : (s1' = 5) & (backoff1' = 9) + (1 / 16) : (s1' = 5) & (backoff1' = 10) + (1 / 16) : (s1' = 5) & (backoff1' = 11) + (1 / 16) : (s1' = 5) & (backoff1' = 12) + (1 / 16) : (s1' = 5) & (backoff1' = 13) + (1 / 16) : (s1' = 5) & (backoff1' = 14) + (1 / 16) : (s1' = 5) & (backoff1' = 15); + [time] (((s1 = 5) & (x1 < 1)) & ((c1 = 0) & (c2 = 0))) -> 1 : (x1' = (min((x1 + 1), 7))); + [] (((s1 = 5) & (x1 = 1)) & (backoff1 > 0)) -> 1 : (x1' = 0) & (s1' = 5) & (backoff1' = (backoff1 - 1)); + [] ((((s1 = 5) & (x1 = 1)) & (backoff1 = 0)) & (slot1 > 0)) -> 1 : (x1' = 0) & (s1' = 5) & (slot1' = (slot1 - 1)) & (backoff1' = 15); + [] ((((s1 = 5) & (x1 = 1)) & (backoff1 = 0)) & (slot1 = 0)) -> 1 : (x1' = 0) & (s1' = 8); + [] ((s1 = 5) & ((c1 > 0) | (c2 > 0))) -> 1 : (x1' = 0) & (s1' = 6); + [time] ((s1 = 6) & ((c1 > 0) | (c2 > 0))) -> 1 : (s1' = 6); + [] ((s1 = 6) & ((c1 = 0) & (c2 = 0))) -> 1 : (s1' = 7); + [time] (((s1 = 7) & (x1 < 3)) & ((c1 = 0) & (c2 = 0))) -> 1 : (x1' = (min((x1 + 1), 7))); + [] ((s1 = 7) & ((x1 = 3) | (x1 = 2))) -> 1 : (x1' = 0) & (s1' = 5); + [] ((s1 = 7) & ((c1 > 0) | (c2 > 0))) -> 1 : (x1' = 0) & (s1' = 6); + [time] ((s1 = 8) & (x1 < 1)) -> 1 : (x1' = (min((x1 + 1), 7))); + [send1] ((s1 = 8) & ((x1 = 1) | (x1 = 0))) -> 1 : (x1' = 0) & (s1' = 9); + [time] ((s1 = 9) & (x1 < 4)) -> 1 : (x1' = (min((x1 + 1), 7))); + [finish1] (((s1 = 9) & (x1 >= 4)) & (c1 = 1)) -> 1 : (x1' = 0) & (s1' = 10); + [finish1] (((s1 = 9) & (x1 >= 4)) & (c1 = 2)) -> 1 : (x1' = 0) & (s1' = 11); + [] ((((s1 = 10) & (c1 = 0)) & (x1 = 0)) & ((c1 > 0) | (c2 > 0))) -> 1 : (s1' = 2); + [time] ((((s1 = 10) & (c1 = 0)) & (x1 = 0)) & ((c1 = 0) & (c2 = 0))) -> 1 : (x1' = (min((x1 + 1), 7))); + [send1] (((s1 = 10) & (c1 = 0)) & ((x1 = 1) | ((x1 = 0) & ((c1 = 0) & (c2 = 0))))) -> 1 : (x1' = 0) & (s1' = 10); + [time] (((s1 = 10) & (c1 = 1)) & (x1 < 4)) -> 1 : (x1' = (min((x1 + 1), 7))); + [finish1] (((s1 = 10) & (c1 = 1)) & ((x1 = 4) | (x1 = 3))) -> 1 : (x1' = 0) & (s1' = 12) & (bc1' = 0); + [] (((s1 = 11) & (x1 = 0)) & ((c1 > 0) | (c2 > 0))) -> 1 : (s1' = 2); + [time] (((s1 = 11) & (x1 = 0)) & ((c1 = 0) & (c2 = 0))) -> 1 : (x1' = (min((x1 + 1), 7))); + [time] (((s1 = 11) & (x1 > 0)) & (x1 < 6)) -> 1 : (x1' = (min((x1 + 1), 7))); + [] ((s1 = 11) & (x1 = 6)) -> 1 : (x1' = 0) & (s1' = 3); + [time] (s1 = 12) -> 1 : (s1' = 12); +endmodule + +module station2 + x2: [0..((max(6, 4)) + 1)] init 0; + s2: [1..12] init 1; + slot2: [0..1] init 0; + backoff2: [0..15] init 0; + bc2: [0..1] init 0; + [time] (((s2 = 1) & (x2 < 3)) & ((c2 = 0) & (c1 = 0))) -> 1 : (x2' = (min((x2 + 1), 7))); + [] ((s2 = 1) & ((x2 = 3) | (x2 = 2))) -> 1 : (x2' = 0) & (s2' = 8); + [] ((s2 = 1) & ((c2 > 0) | (c1 > 0))) -> 1 : (x2' = 0) & (s2' = 2); + [time] ((s2 = 2) & ((c2 > 0) | (c1 > 0))) -> 1 : (s2' = 2); + [] ((s2 = 2) & ((c2 = 0) & (c1 = 0))) -> 1 : (s2' = 3); + [time] (((s2 = 3) & (x2 < 3)) & ((c2 = 0) & (c1 = 0))) -> 1 : (x2' = (min((x2 + 1), 7))); + [] ((s2 = 3) & ((c2 > 0) | (c1 > 0))) -> 1 : (x2' = 0) & (s2' = 2); + [] (((s2 = 3) & ((x2 = 3) | (x2 = 2))) & (bc2 = 0)) -> 1 : (x2' = 0) & (s2' = 4) & (slot2' = 0) & (bc2' = (min((bc2 + 1), 0))); + [] (s2 = 4) -> (1 / 16) : (s2' = 5) & (backoff2' = 0) + (1 / 16) : (s2' = 5) & (backoff2' = 1) + (1 / 16) : (s2' = 5) & (backoff2' = 2) + (1 / 16) : (s2' = 5) & (backoff2' = 3) + (1 / 16) : (s2' = 5) & (backoff2' = 4) + (1 / 16) : (s2' = 5) & (backoff2' = 5) + (1 / 16) : (s2' = 5) & (backoff2' = 6) + (1 / 16) : (s2' = 5) & (backoff2' = 7) + (1 / 16) : (s2' = 5) & (backoff2' = 8) + (1 / 16) : (s2' = 5) & (backoff2' = 9) + (1 / 16) : (s2' = 5) & (backoff2' = 10) + (1 / 16) : (s2' = 5) & (backoff2' = 11) + (1 / 16) : (s2' = 5) & (backoff2' = 12) + (1 / 16) : (s2' = 5) & (backoff2' = 13) + (1 / 16) : (s2' = 5) & (backoff2' = 14) + (1 / 16) : (s2' = 5) & (backoff2' = 15); + [time] (((s2 = 5) & (x2 < 1)) & ((c2 = 0) & (c1 = 0))) -> 1 : (x2' = (min((x2 + 1), 7))); + [] (((s2 = 5) & (x2 = 1)) & (backoff2 > 0)) -> 1 : (x2' = 0) & (s2' = 5) & (backoff2' = (backoff2 - 1)); + [] ((((s2 = 5) & (x2 = 1)) & (backoff2 = 0)) & (slot2 > 0)) -> 1 : (x2' = 0) & (s2' = 5) & (slot2' = (slot2 - 1)) & (backoff2' = 15); + [] ((((s2 = 5) & (x2 = 1)) & (backoff2 = 0)) & (slot2 = 0)) -> 1 : (x2' = 0) & (s2' = 8); + [] ((s2 = 5) & ((c2 > 0) | (c1 > 0))) -> 1 : (x2' = 0) & (s2' = 6); + [time] ((s2 = 6) & ((c2 > 0) | (c1 > 0))) -> 1 : (s2' = 6); + [] ((s2 = 6) & ((c2 = 0) & (c1 = 0))) -> 1 : (s2' = 7); + [time] (((s2 = 7) & (x2 < 3)) & ((c2 = 0) & (c1 = 0))) -> 1 : (x2' = (min((x2 + 1), 7))); + [] ((s2 = 7) & ((x2 = 3) | (x2 = 2))) -> 1 : (x2' = 0) & (s2' = 5); + [] ((s2 = 7) & ((c2 > 0) | (c1 > 0))) -> 1 : (x2' = 0) & (s2' = 6); + [time] ((s2 = 8) & (x2 < 1)) -> 1 : (x2' = (min((x2 + 1), 7))); + [send2] ((s2 = 8) & ((x2 = 1) | (x2 = 0))) -> 1 : (x2' = 0) & (s2' = 9); + [time] ((s2 = 9) & (x2 < 4)) -> 1 : (x2' = (min((x2 + 1), 7))); + [finish2] (((s2 = 9) & (x2 >= 4)) & (c2 = 1)) -> 1 : (x2' = 0) & (s2' = 10); + [finish2] (((s2 = 9) & (x2 >= 4)) & (c2 = 2)) -> 1 : (x2' = 0) & (s2' = 11); + [] ((((s2 = 10) & (c2 = 0)) & (x2 = 0)) & ((c2 > 0) | (c1 > 0))) -> 1 : (s2' = 2); + [time] ((((s2 = 10) & (c2 = 0)) & (x2 = 0)) & ((c2 = 0) & (c1 = 0))) -> 1 : (x2' = (min((x2 + 1), 7))); + [send2] (((s2 = 10) & (c2 = 0)) & ((x2 = 1) | ((x2 = 0) & ((c2 = 0) & (c1 = 0))))) -> 1 : (x2' = 0) & (s2' = 10); + [time] (((s2 = 10) & (c2 = 1)) & (x2 < 4)) -> 1 : (x2' = (min((x2 + 1), 7))); + [finish2] (((s2 = 10) & (c2 = 1)) & ((x2 = 4) | (x2 = 3))) -> 1 : (x2' = 0) & (s2' = 12) & (bc2' = 0); + [] (((s2 = 11) & (x2 = 0)) & ((c2 > 0) | (c1 > 0))) -> 1 : (s2' = 2); + [time] (((s2 = 11) & (x2 = 0)) & ((c2 = 0) & (c1 = 0))) -> 1 : (x2' = (min((x2 + 1), 7))); + [time] (((s2 = 11) & (x2 > 0)) & (x2 < 6)) -> 1 : (x2' = (min((x2 + 1), 7))); + [] ((s2 = 11) & (x2 = 6)) -> 1 : (x2' = 0) & (s2' = 3); + [time] (s2 = 12) -> 1 : (s2' = 12); +endmodule + +label "twoCollisions" = (col = 2); \ No newline at end of file diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp index 6ac99e129..c402b06f5 100644 --- a/test/functional/utility/GraphTest.cpp +++ b/test/functional/utility/GraphTest.cpp @@ -252,6 +252,152 @@ TEST(GraphTest, SymbolicProb01StochasticGameTwoDice) { EXPECT_TRUE(static_cast(result.player2Strategy)); } +TEST(GraphTest, SymbolicProb01StochasticGameWlan) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-4.nm"); + program = program.substituteConstants(); + program = program.flattenModules(std::make_unique()); + + std::vector initialPredicates; + storm::expressions::ExpressionManager& manager = program.getManager(); + + initialPredicates.push_back(manager.getVariableExpression("col") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("col") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("col") == manager.integer(2)); + + initialPredicates.push_back(manager.getVariableExpression("c1") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("c1") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("c1") == manager.integer(2)); + + initialPredicates.push_back(manager.getVariableExpression("c2") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("c2") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("c2") == manager.integer(2)); + + initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(2)); + initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(3)); + initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(4)); + initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(5)); + initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(6)); + initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(7)); + + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(2)); + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(3)); + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(4)); + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(5)); + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(6)); + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(7)); + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(8)); + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(9)); + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(10)); + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(11)); + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(12)); + + initialPredicates.push_back(manager.getVariableExpression("slot1") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("slot1") == manager.integer(1)); + + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(2)); + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(3)); + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(4)); + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(5)); + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(6)); + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(7)); + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(8)); + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(9)); + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(10)); + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(11)); + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(12)); + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(13)); + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(14)); + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(15)); + + initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(1)); + + initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(2)); + initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(3)); + initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(4)); + initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(5)); + initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(6)); + initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(7)); + + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(2)); + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(3)); + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(4)); + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(5)); + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(6)); + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(7)); + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(8)); + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(9)); + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(10)); + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(11)); + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(12)); + + initialPredicates.push_back(manager.getVariableExpression("slot2") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("slot2") == manager.integer(1)); + + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(2)); + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(3)); + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(4)); + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(5)); + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(6)); + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(7)); + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(8)); + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(9)); + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(10)); + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(11)); + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(12)); + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(13)); + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(14)); + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(15)); + + initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(1)); + + storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + + storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); + + // The target states are those states where col == 2. + storm::dd::Bdd targetStates = game.getStates(initialPredicates[2], false); + + storm::utility::graph::GameProb01Result result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true); + EXPECT_EQ(2831, result.states.getNonZeroCount()); + EXPECT_TRUE(static_cast(result.player1Strategy)); + EXPECT_TRUE(static_cast(result.player2Strategy)); + + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true); + EXPECT_EQ(2692, result.states.getNonZeroCount()); + + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true); + EXPECT_EQ(2831, result.states.getNonZeroCount()); + + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true); + EXPECT_EQ(2692, result.states.getNonZeroCount()); + + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true); + EXPECT_EQ(2064, result.states.getNonZeroCount()); + + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true); + EXPECT_EQ(2884, result.states.getNonZeroCount()); + + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true); + EXPECT_EQ(2064, result.states.getNonZeroCount()); + + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true); + EXPECT_EQ(2884, result.states.getNonZeroCount()); + EXPECT_TRUE(static_cast(result.player1Strategy)); + EXPECT_TRUE(static_cast(result.player2Strategy)); +} + #endif TEST(GraphTest, ExplicitProb01) {