Merge remote-tracking branch 'remotes/origin/menu_games' into sylvanRationalFunctions

Former-commit-id: 24e32e5b30

resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c

@@ -611,11 +611,12 @@ cuddBddExistAbstractRepresentativeRecur(
         if (res1 == NULL) {
             return(NULL);
         }
+        // FIXME
         if (res1 == one) {
             if (F->ref != 1) {
                 cuddCacheInsert2(manager, Cudd_bddExistAbstractRepresentative, f, cube, one);
             }
-            return(one);
+            return(cube);
         }
         cuddRef(res1);
         

src/abstraction/AbstractionInformation.cpp

@@ -51,6 +51,7 @@ namespace storm {
             std::pair<storm::expressions::Variable, storm::expressions::Variable> newMetaVariable = ddManager->addMetaVariable(stream.str());
             
             predicateDdVariables.push_back(newMetaVariable);
+            extendedPredicateDdVariables.push_back(newMetaVariable);
             predicateBdds.emplace_back(ddManager->getEncoding(newMetaVariable.first, 1), ddManager->getEncoding(newMetaVariable.second, 1));
             predicateIdentities.push_back(ddManager->getEncoding(newMetaVariable.first, 1).iff(ddManager->getEncoding(newMetaVariable.second, 1)));
             allPredicateIdentities &= predicateIdentities.back();

src/abstraction/prism/AbstractProgram.cpp

@@ -205,6 +205,96 @@ namespace storm {
                 return reachableStates;
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            void AbstractProgram<DdType, ValueType>::exportToDot(std::string const& filename) const {
+                std::ofstream out(filename);
+                out << "digraph game {" << std::endl;
+                
+                // Create the player 1 nodes.
+                storm::dd::Add<DdType, ValueType> statesAsAdd = currentGame->getReachableStates().template toAdd<ValueType>();
+                for (auto stateValue : statesAsAdd) {
+                    out << "\tpl1_";
+                    std::stringstream stateName;
+                    for (auto const& var : currentGame->getRowVariables()) {
+                        if (stateValue.first.getBooleanValue(var)) {
+                            stateName << "1";
+                        } else {
+                            stateName << "0";
+                        }
+                    }
+                    out << stateName.str();
+                    out << " [ label=\"";
+                    if (stateValue.first.getBooleanValue(abstractionInformation.getBottomStateVariable(true))) {
+                        out << "*\", margin=0, width=0, height=0, shape=\"none";
+                    } else {
+                        out << stateName.str() << "\", margin=0, width=0, height=0, shape=\"oval";
+                    }
+                    out << "\" ];" << std::endl;
+                }
+                
+                // Create the nodes of the second player.
+                storm::dd::Add<DdType, ValueType> player2States = currentGame->getTransitionMatrix().toBdd().existsAbstract(currentGame->getColumnVariables()).existsAbstract(currentGame->getPlayer2Variables()).template toAdd<ValueType>();
+                for (auto stateValue : player2States) {
+                    out << "\tpl2_";
+                    std::stringstream stateName;
+                    for (auto const& var : currentGame->getRowVariables()) {
+                        if (stateValue.first.getBooleanValue(var)) {
+                            stateName << "1";
+                        } else {
+                            stateName << "0";
+                        }
+                    }
+                    uint_fast64_t index = 0;
+                    for (uint_fast64_t player1VariableIndex = 0; player1VariableIndex < abstractionInformation.getPlayer1VariableCount(); ++player1VariableIndex) {
+                        index <<= 1;
+                        if (stateValue.first.getBooleanValue(abstractionInformation.getPlayer1Variables()[player1VariableIndex])) {
+                            index |= 1;
+                        }
+                    }
+                    out << stateName.str() << "_" << index;
+                    out << " [ shape=\"square\", width=0, height=0, margin=0, label=\"" << index << "\" ];" << std::endl;
+                    out << "\tpl1_" << stateName.str() << " -> " << "pl2_" << stateName.str() << "_" << index << " [ label=\"" << index << "\" ];" << std::endl;
+                }
+                
+                // Create the nodes of the probabilistic player.
+                storm::dd::Add<DdType, ValueType> playerPStates = currentGame->getTransitionMatrix().toBdd().existsAbstract(currentGame->getColumnVariables()).template toAdd<ValueType>();
+                for (auto stateValue : playerPStates) {
+                    out << "\tplp_";
+                    std::stringstream stateName;
+                    for (auto const& var : currentGame->getRowVariables()) {
+                        if (stateValue.first.getBooleanValue(var)) {
+                            stateName << "1";
+                        } else {
+                            stateName << "0";
+                        }
+                    }
+                    uint_fast64_t index = 0;
+                    for (uint_fast64_t player1VariableIndex = 0; player1VariableIndex < abstractionInformation.getPlayer1VariableCount(); ++player1VariableIndex) {
+                        index <<= 1;
+                        if (stateValue.first.getBooleanValue(abstractionInformation.getPlayer1Variables()[player1VariableIndex])) {
+                            index |= 1;
+                        }
+                    }
+                    stateName << "_" << index;
+                    index = 0;
+                    for (uint_fast64_t player2VariableIndex = 0; player2VariableIndex < currentGame->getPlayer2Variables().size(); ++player2VariableIndex) {
+                        index <<= 1;
+                        if (stateValue.first.getBooleanValue(abstractionInformation.getPlayer2Variables()[player2VariableIndex])) {
+                            index |= 1;
+                        }                    }
+                    out << stateName.str() << "_" << index;
+                    out << " [ shape=\"point\", label=\"\" ];" << std::endl;
+                    out << "\tpl2_" << stateName.str() << " -> " << "plp_" << stateName.str() << "_" << index << " [ label=\"" << index << "\" ];" << std::endl;
+                }
+                
+//                for (auto stateValue : currentGame->getTransitionMatrix()) {
+//                    std::stringstream stateName;
+//
+//                }
+                
+                out << "}" << std::endl;
+            }
+            
             // Explicitly instantiate the class.
             template class AbstractProgram<storm::dd::DdType::CUDD, double>;
             template class AbstractProgram<storm::dd::DdType::Sylvan, double>;

src/abstraction/prism/AbstractProgram.h

@@ -74,6 +74,13 @@ namespace storm {
                  */
                 void refine(std::vector<storm::expressions::Expression> const& predicates);
                 
+                /*!
+                 * Exports the current state of the abstraction in the dot format to the given file.
+                 *
+                 * @param filename The name of the file to which to write the dot output.
+                 */
+                void exportToDot(std::string const& filename) const;
+                
             private:
                 /*!
                  * Computes the reachable states of the transition relation.

src/abstraction/prism/PrismMenuGameAbstractor.cpp

@@ -23,6 +23,11 @@ namespace storm {
             void PrismMenuGameAbstractor<DdType, ValueType>::refine(std::vector<storm::expressions::Expression> const& predicates) {
                 abstractProgram.refine(predicates);
             }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            void PrismMenuGameAbstractor<DdType, ValueType>::exportToDot(std::string const& filename) const {
+                abstractProgram.exportToDot(filename);
+            }
          
             template class PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double>;
             template class PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double>;

src/abstraction/prism/PrismMenuGameAbstractor.h

@@ -16,6 +16,8 @@ namespace storm {
                 virtual storm::abstraction::MenuGame<DdType, ValueType> abstract() override;
                 virtual void refine(std::vector<storm::expressions::Expression> const& predicates) override;
 
+                void exportToDot(std::string const& filename) const;
+                
             private:
                 /// The abstract program that performs the actual abstraction.
                 AbstractProgram<DdType, ValueType> abstractProgram;

src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -70,9 +70,9 @@ namespace storm {
             
             storm::abstraction::prism::PrismMenuGameAbstractor<Type, ValueType> abstractor(preprocessedProgram, initialPredicates, smtSolverFactory);
             
-            
             // 1. build initial abstraction based on the the constraint expression (if not 'true') and the target state expression.
             storm::abstraction::MenuGame<Type, ValueType> game = abstractor.abstract();
+            abstractor.exportToDot("game.dot");
             STORM_LOG_DEBUG("Initial abstraction has " << game.getNumberOfStates() << " (player 1) states and " << game.getNumberOfTransitions() << " transitions.");
             
             // 2. solve the game wrt. to min/max as given by checkTask and min/max for the abstraction player to obtain two bounds.
@@ -95,22 +95,34 @@ namespace storm {
         void GameBasedMdpModelChecker<Type, ValueType>::computeProb01States(storm::OptimizationDirection player1Direction, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) {
             storm::dd::Bdd<Type> transitionMatrixBdd = game.getTransitionMatrix().toBdd();
             storm::dd::Bdd<Type> bottomStatesBdd = game.getBottomStates();
-            game.getTransitionMatrix().exportToDot("trans.dot");
-            bottomStatesBdd.template toAdd<ValueType>().exportToDot("bottom.dot");
             
             storm::dd::Bdd<Type> targetStates = game.getStates(targetStateExpression);
             if (player1Direction == storm::OptimizationDirection::Minimize) {
                 targetStates |= game.getBottomStates();
             }
+                        
+            transitionMatrixBdd.template toAdd<ValueType>().exportToDot("transbdd.dot");
             
             // Start by computing the states with probability 0/1 when player 2 minimizes.
             storm::utility::graph::GameProb01Result<Type> prob0Min = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Minimize, true);
-            storm::utility::graph::GameProb01Result<Type> prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Minimize, true);
+            storm::utility::graph::GameProb01Result<Type> prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Minimize, false);
             
             // Now compute the states with probability 0/1 when player 2 maximizes.
-            storm::utility::graph::GameProb01Result<Type> prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Maximize, true);
+            storm::utility::graph::GameProb01Result<Type> prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Maximize, false);
             storm::utility::graph::GameProb01Result<Type> prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Maximize, true);
             
+//            STORM_LOG_ASSERT(prob0Min.hasPlayer1Strategy(), "Unable to proceed without strategy.");
+            STORM_LOG_ASSERT(prob0Min.hasPlayer2Strategy(), "Unable to proceed without strategy.");
+
+            STORM_LOG_ASSERT(prob1Max.hasPlayer1Strategy(), "Unable to proceed without strategy.");
+            STORM_LOG_ASSERT(prob1Max.hasPlayer2Strategy(), "Unable to proceed without strategy.");
+
+//            prob0Min.getPlayer1Strategy().template toAdd<ValueType>().exportToDot("prob0_min_pl1_strat.dot");
+            prob0Min.getPlayer2Strategy().template toAdd<ValueType>().exportToDot("prob0_min_pl2_strat.dot");
+
+            prob1Max.getPlayer1Strategy().template toAdd<ValueType>().exportToDot("prob1_max_pl1_strat.dot");
+            prob1Max.getPlayer2Strategy().template toAdd<ValueType>().exportToDot("prob1_max_pl2_strat.dot");
+
             STORM_LOG_DEBUG("Min: " << prob0Min.states.getNonZeroCount() << " no states, " << prob1Min.states.getNonZeroCount() << " yes states.");
             STORM_LOG_DEBUG("Max: " << prob0Max.states.getNonZeroCount() << " no states, " << prob1Max.states.getNonZeroCount() << " yes states.");
             

src/storage/dd/cudd/CuddAddIterator.cpp

@@ -117,7 +117,7 @@ namespace storm {
             // valuations later.
             for (auto const& metaVariable : *this->metaVariables) {
                 bool metaVariableAppearsInCube = false;
-                std::vector<std::tuple<storm::expressions::Variable, uint_fast64_t>> localRelenvantDontCareDdVariables;
+                std::vector<std::tuple<storm::expressions::Variable, uint_fast64_t>> localRelevantDontCareDdVariables;
                 auto const& ddMetaVariable = this->ddManager->getMetaVariable(metaVariable);
                 if (ddMetaVariable.getType() == MetaVariableType::Bool) {
                     if (this->cube[ddMetaVariable.getDdVariables().front().getIndex()] == 0) {
@@ -127,7 +127,8 @@ namespace storm {
                         metaVariableAppearsInCube = true;
                         currentValuation.setBooleanValue(metaVariable, true);
                     } else {
-                        localRelenvantDontCareDdVariables.push_back(std::make_tuple(metaVariable, 0));
+                        currentValuation.setBooleanValue(metaVariable, false);
+                        localRelevantDontCareDdVariables.push_back(std::make_tuple(metaVariable, 0));
                     }
                 } else {
                     int_fast64_t intValue = 0;
@@ -141,7 +142,7 @@ namespace storm {
                         } else {
                             // Temporarily leave bit unset so we can iterate trough the other option later.
                             // Add the bit to the relevant don't care bits.
-                            localRelenvantDontCareDdVariables.push_back(std::make_tuple(metaVariable, ddMetaVariable.getNumberOfDdVariables() - bitIndex - 1));
+                            localRelevantDontCareDdVariables.push_back(std::make_tuple(metaVariable, ddMetaVariable.getNumberOfDdVariables() - bitIndex - 1));
                         }
                     }
                     if (this->enumerateDontCareMetaVariables || metaVariableAppearsInCube) {
@@ -152,7 +153,7 @@ namespace storm {
                 // If all meta variables are to be enumerated or the meta variable appeared in the cube, we register the
                 // missing bits to later enumerate all possible valuations.
                 if (this->enumerateDontCareMetaVariables || metaVariableAppearsInCube) {
-                    relevantDontCareDdVariables.insert(relevantDontCareDdVariables.end(), localRelenvantDontCareDdVariables.begin(), localRelenvantDontCareDdVariables.end());
+                    relevantDontCareDdVariables.insert(relevantDontCareDdVariables.end(), localRelevantDontCareDdVariables.begin(), localRelevantDontCareDdVariables.end());
                 }
             }
             

src/utility/graph.cpp

@@ -955,7 +955,7 @@ namespace storm {
                     solution = tmp;
                     ++iterations;
                 }
-                
+
                 // Since we have determined the inverse of the desired set, we need to complement it now.
                 solution = !solution && model.getReachableStates();
 

src/utility/graph.h

@@ -528,6 +528,26 @@ namespace storm {
                     // Intentionally left empty.
                 }
                 
+                bool hasPlayer1Strategy() const {
+                    return static_cast<bool>(player1Strategy);
+                }
+                
+                storm::dd::Bdd<Type> const& getPlayer1Strategy() {
+                    return player1Strategy.get();
+                }
+
+                bool hasPlayer2Strategy() const {
+                    return static_cast<bool>(player2Strategy);
+                }
+
+                storm::dd::Bdd<Type> const& getPlayer2Strategy() {
+                    return player2Strategy.get();
+                }
+
+                storm::dd::Bdd<Type> const& getStates() const {
+                    return states;
+                }
+
                 storm::dd::Bdd<Type> states;
                 boost::optional<storm::dd::Bdd<Type>> player1Strategy;
                 boost::optional<storm::dd::Bdd<Type>> player2Strategy;

test/functional/utility/GraphTest.cpp

@@ -215,30 +215,30 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) {
     storm::dd::Bdd<storm::dd::DdType::CUDD> targetStates = game.getStates(initialPredicates[0], true);
     
     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(1, result.states.getNonZeroCount());
+    EXPECT_EQ(2, 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(1, result.states.getNonZeroCount());
+    EXPECT_EQ(2, result.states.getNonZeroCount());
     
     result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true);
-    EXPECT_EQ(1, result.states.getNonZeroCount());
+    EXPECT_EQ(2, result.states.getNonZeroCount());
     
     result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true);
-    EXPECT_EQ(1, result.states.getNonZeroCount());
+    EXPECT_EQ(2, result.states.getNonZeroCount());
     
     result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true);
-    EXPECT_EQ(0, result.states.getNonZeroCount());
+    EXPECT_EQ(2, result.states.getNonZeroCount());
     
     result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true);
     EXPECT_EQ(2, result.states.getNonZeroCount());
     
     result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true);
-    EXPECT_EQ(0, result.states.getNonZeroCount());
+    EXPECT_EQ(1, result.states.getNonZeroCount());
     
     result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true);
-    EXPECT_EQ(2, result.states.getNonZeroCount());
+    EXPECT_EQ(3, result.states.getNonZeroCount());
     EXPECT_TRUE(static_cast<bool>(result.player1Strategy));
     EXPECT_TRUE(static_cast<bool>(result.player2Strategy));
     
@@ -249,7 +249,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) {
     targetStates = game.getStates(initialPredicates[0], true);
     
     result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true);
-    EXPECT_EQ(0, result.states.getNonZeroCount());
+    EXPECT_EQ(2, result.states.getNonZeroCount());
     EXPECT_TRUE(static_cast<bool>(result.player1Strategy));
     EXPECT_TRUE(static_cast<bool>(result.player2Strategy));
     
@@ -258,33 +258,33 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) {
     EXPECT_TRUE(nonProb0StatesWithStrategy.isZero());
     
     // Proceed by checking whether they select exactly one action in each state.
-    storm::dd::Add<storm::dd::DdType::CUDD, double> stateDistributionsUnderStrategies = (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd<double>() * result.player2Strategy.get().template toAdd<double>()).sumAbstract(game.getColumnVariables());;
-    EXPECT_EQ(0, stateDistributionsUnderStrategies.getNonZeroCount());
+    storm::dd::Add<storm::dd::DdType::CUDD, double> stateDistributionsUnderStrategies = (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd<double>() * result.player2Strategy.get().template toAdd<double>()).sumAbstract(game.getColumnVariables());
+    EXPECT_EQ(2, stateDistributionsUnderStrategies.getNonZeroCount());
     
     // Check that the number of distributions per state is one (or zero in the case where there are no prob0 states).
     storm::dd::Add<storm::dd::DdType::CUDD> stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables());
-    EXPECT_EQ(0, stateDistributionCount.getMax());
+    EXPECT_EQ(1, stateDistributionCount.getMax());
     
     result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true);
     EXPECT_EQ(3, result.states.getNonZeroCount());
     
     result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true);
-    EXPECT_EQ(0, result.states.getNonZeroCount());
+    EXPECT_EQ(1, result.states.getNonZeroCount());
     
     result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true);
-    EXPECT_EQ(3, result.states.getNonZeroCount());
+    EXPECT_EQ(4, result.states.getNonZeroCount());
     
     result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true);
-    EXPECT_EQ(0, result.states.getNonZeroCount());
+    EXPECT_EQ(2, result.states.getNonZeroCount());
     
     result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true);
     EXPECT_EQ(3, result.states.getNonZeroCount());
     
     result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true);
-    EXPECT_EQ(0, result.states.getNonZeroCount());
+    EXPECT_EQ(1, result.states.getNonZeroCount());
     
     result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true);
-    EXPECT_EQ(3, result.states.getNonZeroCount());
+    EXPECT_EQ(4, result.states.getNonZeroCount());
     EXPECT_TRUE(static_cast<bool>(result.player1Strategy));
     EXPECT_TRUE(static_cast<bool>(result.player2Strategy));
     
@@ -294,7 +294,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) {
     
     // Proceed by checking whether they select exactly one action in each state.
     stateDistributionsUnderStrategies = (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd<double>() * result.player2Strategy.get().template toAdd<double>()).sumAbstract(game.getColumnVariables());
-    EXPECT_EQ(3, stateDistributionsUnderStrategies.getNonZeroCount());
+    EXPECT_EQ(4, stateDistributionsUnderStrategies.getNonZeroCount());
     
     // Check that the number of distributions per state is one (or zero in the case where there are no prob1 states).
     stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables());