added no-cuts option. prob1 tests for game now passing.

Former-commit-id: 3806747948

src/builder/DdPrismModelBuilder.cpp

@@ -254,6 +254,11 @@ namespace storm {
         
         template <storm::dd::DdType Type>
         void DdPrismModelBuilder<Type>::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()) {

src/builder/ExplicitPrismModelBuilder.cpp

@@ -113,6 +113,7 @@ namespace storm {
         template <typename ValueType, typename IndexType>
         ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()), terminalStates(), negatedTerminalStates() {
             this->preserveFormula(formula);
+            this->setTerminalStatesFromFormula(formula);
         }
         
         template <typename ValueType, typename IndexType>
@@ -132,6 +133,11 @@ namespace storm {
         
         template <typename ValueType, typename IndexType>
         void ExplicitPrismModelBuilder<ValueType, IndexType>::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()) {

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.

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<std::string> 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<storm::settings::SettingMemento> GeneralSettings::overrideDontFixDeadlocksSet(bool stateToSet) {
                 return this->overrideOption(dontFixDeadlockOptionName, stateToSet);
             }

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;

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

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<storm::utility::solver::MathsatSmtSolverFactory>());
     
@@ -295,12 +295,12 @@ TEST(PrismMenuGame, WlanAbstractionTest) {
     
     storm::prism::menu_games::MenuGame<storm::dd::DdType::CUDD> 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<storm::utility::solver::MathsatSmtSolverFactory>());
     
@@ -317,12 +317,12 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest) {
 
     storm::prism::menu_games::MenuGame<storm::dd::DdType::CUDD> 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<storm::utility::solver::MathsatSmtSolverFactory>());
     
@@ -435,8 +435,8 @@ TEST(PrismMenuGame, WlanFullAbstractionTest) {
     
     storm::prism::menu_games::MenuGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
     
-    EXPECT_EQ(59, game.getNumberOfTransitions());
-    EXPECT_EQ(37, game.getNumberOfStates());
+    EXPECT_EQ(9503, game.getNumberOfTransitions());
+    EXPECT_EQ(5523, game.getNumberOfStates());
 }
 
 #endif

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);

test/functional/utility/GraphTest.cpp

@@ -252,6 +252,152 @@ TEST(GraphTest, SymbolicProb01StochasticGameTwoDice) {
     EXPECT_TRUE(static_cast<bool>(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<storm::utility::solver::MathsatSmtSolverFactory>());
+    
+    std::vector<storm::expressions::Expression> 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<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+    
+    storm::prism::menu_games::MenuGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
+    
+    // The target states are those states where col == 2.
+    storm::dd::Bdd<storm::dd::DdType::CUDD> targetStates = game.getStates(initialPredicates[2], false);
+    
+    storm::utility::graph::GameProb01Result<storm::dd::DdType::CUDD> 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<bool>(result.player1Strategy));
+    EXPECT_TRUE(static_cast<bool>(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<bool>(result.player1Strategy));
+    EXPECT_TRUE(static_cast<bool>(result.player2Strategy));
+}
+
 #endif
 
 TEST(GraphTest, ExplicitProb01) {