diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 5859a8d58..689245e99 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -92,6 +92,15 @@ namespace storm { } } + template + void refineAfterQualitativeCheck(storm::abstraction::MenuGame const& game, detail::GameProb01Result const& prob01, storm::dd::Bdd const& transitionMatrixBdd) { + // First, we have to find the pivot states. + storm::dd::Bdd playerPStates = transitionMatrixBdd.existsAbstract(game.getColumnVariables()); + + +// playerPStates &= prob01.min.first. + } + template std::unique_ptr GameBasedMdpModelChecker::performGameBasedAbstractionRefinement(CheckTask const& checkTask, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) { STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidPropertyException, "The game-based abstraction refinement model checker can only compute the result for the initial states."); @@ -114,8 +123,11 @@ namespace storm { storm::abstraction::MenuGame game = abstractor.abstract(); STORM_LOG_DEBUG("Initial abstraction has " << game.getNumberOfStates() << " (player 1) states and " << game.getNumberOfTransitions() << " transitions."); + // 1.5 build a BDD from the transition matrix for various later uses. + storm::dd::Bdd transitionMatrixBdd = game.getTransitionMatrix().toBdd(); + // 2. compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max). - detail::GameProb01Result prob01 = computeProb01States(player1Direction, game, constraintExpression, targetStateExpression); + detail::GameProb01Result prob01 = computeProb01States(player1Direction, game, transitionMatrixBdd, constraintExpression, targetStateExpression); // 3. compute the states for which we know the result/for which we know there is more work to be done. storm::dd::Bdd maybeMin = !(prob01.min.first.states || prob01.min.second.states) && game.getReachableStates(); @@ -140,8 +152,7 @@ namespace storm { // If we get here, the initial states were all identified as prob0/1 states, but the value (0 or 1) // depends on whether player 2 is minimizing or maximizing. Therefore, we need to find a place to refine. - - + refineAfterQualitativeCheck(game, prob01, transitionMatrixBdd); } @@ -158,8 +169,7 @@ namespace storm { } template - detail::GameProb01Result GameBasedMdpModelChecker::computeProb01States(storm::OptimizationDirection player1Direction, storm::abstraction::MenuGame const& game, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) { - storm::dd::Bdd transitionMatrixBdd = game.getTransitionMatrix().toBdd(); + detail::GameProb01Result GameBasedMdpModelChecker::computeProb01States(storm::OptimizationDirection player1Direction, storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) { storm::dd::Bdd bottomStatesBdd = game.getBottomStates(); storm::dd::Bdd targetStates = game.getStates(targetStateExpression); @@ -168,12 +178,12 @@ namespace storm { } // Start by computing the states with probability 0/1 when player 2 minimizes. - storm::utility::graph::GameProb01Result prob0Min = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Minimize, true); - storm::utility::graph::GameProb01Result prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Minimize, false); + storm::utility::graph::GameProb01Result prob0Min = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true); + storm::utility::graph::GameProb01Result prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Minimize, false, false); // Now compute the states with probability 0/1 when player 2 maximizes. - storm::utility::graph::GameProb01Result prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Maximize, false); - storm::utility::graph::GameProb01Result prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Maximize, true); + storm::utility::graph::GameProb01Result prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Maximize, false, false); + storm::utility::graph::GameProb01Result prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true); 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."); diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.h b/src/modelchecker/abstraction/GameBasedMdpModelChecker.h index a7a9ae485..2e480e9fa 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.h +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.h @@ -50,7 +50,7 @@ namespace storm { private: std::unique_ptr performGameBasedAbstractionRefinement(CheckTask const& checkTask, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression); - detail::GameProb01Result computeProb01States(storm::OptimizationDirection player1Direction, storm::abstraction::MenuGame const& game, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression); + detail::GameProb01Result computeProb01States(storm::OptimizationDirection player1Direction, storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression); storm::expressions::Expression getExpression(storm::logic::Formula const& formula); diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp index 55cb72cda..da42fad1b 100644 --- a/src/utility/graph.cpp +++ b/src/utility/graph.cpp @@ -924,7 +924,7 @@ namespace storm { } template - GameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool produceStrategies) { + GameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy) { // The solution set. storm::dd::Bdd solution = psiStates; @@ -966,13 +966,13 @@ namespace storm { storm::dd::Bdd onlyProb0Successors = (transitionsBetweenProb0States || model.getIllegalSuccessorMask()).universalAbstract(model.getColumnVariables()); boost::optional> player2StrategyBdd; - if (produceStrategies && player2Strategy == OptimizationDirection::Minimize) { + if (producePlayer2Strategy) { // Pick a distribution that has only prob0 successors. player2StrategyBdd = onlyProb0Successors.existsAbstractRepresentative(model.getPlayer2Variables()); } boost::optional> player1StrategyBdd; - if (produceStrategies && player1Strategy == OptimizationDirection::Minimize) { + if (producePlayer1Strategy) { // Move from player 2 choices with only prob0 successors to player 1 choices with only prob 0 successors. onlyProb0Successors = onlyProb0Successors.existsAbstract(model.getPlayer2Variables()); @@ -984,7 +984,7 @@ namespace storm { } template - GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool produceStrategies) { + GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy) { // Create two sets of states. Those states for which we definitely know that their probability is 1 and // those states that potentially have a probability of 1. @@ -1079,7 +1079,7 @@ namespace storm { // If we were asked to produce strategies, we propagate that by triggering another iteration. // We only do this if at least one strategy will be produced. - produceStrategiesInIteration = !produceStrategiesInIteration && produceStrategies && (player1Strategy == OptimizationDirection::Maximize || player2Strategy == OptimizationDirection::Maximize); + produceStrategiesInIteration = !produceStrategiesInIteration && ((producePlayer1Strategy && player1Strategy == OptimizationDirection::Maximize) || (producePlayer2Strategy && player2Strategy == OptimizationDirection::Maximize)); } else { // Otherwise, we use the current hypothesis for the states with probability 1 as the new maybe // state set. @@ -1088,6 +1088,20 @@ namespace storm { ++maybeStateIterations; } + // If we were asked to produce strategies that do not need to pick a certain successor but are + // 'arbitrary', do so now. + bool strategiesToCompute = (producePlayer1Strategy && !player1StrategyBdd) || (producePlayer2Strategy && !player2StrategyBdd); + if (strategiesToCompute) { + storm::dd::Bdd relevantStates = (transitionMatrix && solution).existsAbstract(model.getColumnVariables()); + if (producePlayer2Strategy && !player2StrategyBdd) { + player2StrategyBdd = relevantStates.existsAbstractRepresentative(model.getPlayer2Variables()); + } + if (producePlayer1Strategy && !player1StrategyBdd) { + relevantStates = relevantStates.existsAbstract(model.getPlayer2Variables()); + player1StrategyBdd = relevantStates.existsAbstractRepresentative(model.getPlayer1Variables()); + } + } + return GameProb01Result(solution, player1StrategyBdd, player2StrategyBdd); } @@ -1488,9 +1502,9 @@ namespace storm { template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); - template GameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool produceStrategies); + template GameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy); - template GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool produceStrategies); + template GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy); // Instantiations for Sylvan. @@ -1520,9 +1534,9 @@ namespace storm { template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); - template GameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool produceStrategies); + template GameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy); - template GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool produceStrategies); + template GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy); } // namespace graph } // namespace utility diff --git a/src/utility/graph.h b/src/utility/graph.h index cd03b42dd..07b0aafa8 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -568,11 +568,11 @@ namespace storm { * @param transitionMatrix The transition matrix of the model as a BDD. * @param phiStates The BDD containing all phi states of the model. * @param psiStates The BDD containing all psi states of the model. - * @param produceStrategies A flag indicating whether strategies should be produced. Note that the strategies - * are only produced in case the choices of the player are not irrelevant. + * @param producePlayer1Strategy A flag indicating whether the strategy of player 1 shall be produced. + * @param producePlayer2Strategy A flag indicating whether the strategy of player 2 shall be produced. */ template - GameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool produceStrategies = false); + GameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false, bool producePlayer2Strategy = false); /*! * Computes the set of states that have probability 1 given the strategies of the two players. @@ -581,11 +581,11 @@ namespace storm { * @param transitionMatrix The transition matrix of the model as a BDD. * @param phiStates The BDD containing all phi states of the model. * @param psiStates The BDD containing all psi states of the model. - * @param produceStrategies A flag indicating whether strategies should be produced. Note that the strategies - * are only produced in case the choices of the player are not irrelevant. + * @param producePlayer1Strategy A flag indicating whether the strategy of player 1 shall be produced. + * @param producePlayer2Strategy A flag indicating whether the strategy of player 2 shall be produced. */ template - GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategybool, bool produceStrategies = false); + GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false, bool producePlayer2Strategy = false); /*! * Performs a topological sort of the states of the system according to the given transitions. diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp index 176129ed6..9fb9a0589 100644 --- a/test/functional/utility/GraphTest.cpp +++ b/test/functional/utility/GraphTest.cpp @@ -214,33 +214,33 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { // The target states are those states where !(s < 3). storm::dd::Bdd targetStates = game.getStates(initialPredicates[0], true); - storm::utility::graph::GameProb01Result result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true); + storm::utility::graph::GameProb01Result result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true); EXPECT_EQ(2, result.states.getNonZeroCount()); - EXPECT_TRUE(static_cast(result.player1Strategy)); - EXPECT_TRUE(static_cast(result.player2Strategy)); + EXPECT_TRUE(result.hasPlayer1Strategy()); + EXPECT_TRUE(result.hasPlayer2Strategy()); - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true); + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize); EXPECT_EQ(2, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); EXPECT_EQ(2, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); EXPECT_EQ(2, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true); + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); EXPECT_EQ(2, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true); + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); EXPECT_EQ(2, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize); EXPECT_EQ(1, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true); EXPECT_EQ(3, result.states.getNonZeroCount()); - EXPECT_TRUE(static_cast(result.player1Strategy)); - EXPECT_TRUE(static_cast(result.player2Strategy)); + EXPECT_TRUE(result.hasPlayer1Strategy()); + EXPECT_TRUE(result.hasPlayer2Strategy()); abstractProgram.refine({manager.getVariableExpression("s") < manager.integer(2)}); game = abstractProgram.getAbstractGame(); @@ -248,10 +248,10 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { // We need to create a new BDD for the target states since the reachable states might have changed. targetStates = game.getStates(initialPredicates[0], true); - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true); + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true); EXPECT_EQ(2, result.states.getNonZeroCount()); - EXPECT_TRUE(static_cast(result.player1Strategy)); - EXPECT_TRUE(static_cast(result.player2Strategy)); + ASSERT_TRUE(result.hasPlayer1Strategy()); + ASSERT_TRUE(result.hasPlayer2Strategy()); // Check the validity of the strategies. Start by checking whether only prob0 states have a strategy. storm::dd::Bdd nonProb0StatesWithStrategy = !result.states && result.player1Strategy.get(); @@ -265,28 +265,28 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { storm::dd::Add stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables()); EXPECT_EQ(1, stateDistributionCount.getMax()); - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true); + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize); EXPECT_EQ(3, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); EXPECT_EQ(1, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); EXPECT_EQ(4, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true); + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); EXPECT_EQ(2, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true); + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); EXPECT_EQ(3, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize); EXPECT_EQ(1, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true); EXPECT_EQ(4, result.states.getNonZeroCount()); - EXPECT_TRUE(static_cast(result.player1Strategy)); - EXPECT_TRUE(static_cast(result.player2Strategy)); + EXPECT_TRUE(result.hasPlayer1Strategy()); + EXPECT_TRUE(result.hasPlayer2Strategy()); // Check the validity of the strategies. Start by checking whether only prob1 states have a strategy. storm::dd::Bdd nonProb1StatesWithStrategy = !result.states && result.player1Strategy.get(); @@ -350,10 +350,10 @@ TEST(GraphTest, SymbolicProb01StochasticGameTwoDice) { // The target states are those states where s1 == 7 & s2 == 7 & d1 + d2 == 1. storm::dd::Bdd targetStates = game.getStates(initialPredicates[7], false) && game.getStates(initialPredicates[22], false) && game.getStates(initialPredicates[9], false) && game.getStates(initialPredicates[24], false); - storm::utility::graph::GameProb01Result result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true); + storm::utility::graph::GameProb01Result result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true); EXPECT_EQ(153, result.states.getNonZeroCount()); - EXPECT_TRUE(static_cast(result.player1Strategy)); - EXPECT_TRUE(static_cast(result.player2Strategy)); + ASSERT_TRUE(result.hasPlayer1Strategy()); + ASSERT_TRUE(result.hasPlayer2Strategy()); // Check the validity of the strategies. Start by checking whether only prob0 states have a strategy. storm::dd::Bdd nonProb0StatesWithStrategy = !result.states && result.player1Strategy.get(); @@ -366,28 +366,28 @@ TEST(GraphTest, SymbolicProb01StochasticGameTwoDice) { storm::dd::Add stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables()); EXPECT_EQ(1, stateDistributionCount.getMax()); - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true); + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize); EXPECT_EQ(1, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); EXPECT_EQ(153, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); EXPECT_EQ(1, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true); + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); EXPECT_EQ(153, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true); + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); EXPECT_EQ(1, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize); EXPECT_EQ(153, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true); EXPECT_EQ(1, result.states.getNonZeroCount()); - EXPECT_TRUE(static_cast(result.player1Strategy)); - EXPECT_TRUE(static_cast(result.player2Strategy)); + EXPECT_TRUE(result.hasPlayer1Strategy()); + EXPECT_TRUE(result.hasPlayer2Strategy()); // Check the validity of the strategies. Start by checking whether only prob1 states have a strategy. storm::dd::Bdd nonProb1StatesWithStrategy = !result.states && result.player1Strategy.get(); @@ -519,10 +519,10 @@ TEST(GraphTest, SymbolicProb01StochasticGameWlan) { // 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); + storm::utility::graph::GameProb01Result result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true); EXPECT_EQ(2831, result.states.getNonZeroCount()); - ASSERT_TRUE(static_cast(result.player1Strategy)); - ASSERT_TRUE(static_cast(result.player2Strategy)); + EXPECT_TRUE(result.hasPlayer1Strategy()); + EXPECT_TRUE(result.hasPlayer2Strategy()); // Check the validity of the strategies. Start by checking whether only prob0 states have a strategy. storm::dd::Bdd nonProb0StatesWithStrategy = !result.states && result.player1Strategy.get(); @@ -536,28 +536,28 @@ TEST(GraphTest, SymbolicProb01StochasticGameWlan) { storm::dd::Add stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables()); EXPECT_EQ(1, stateDistributionCount.getMax()); - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true); + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize); EXPECT_EQ(2692, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); EXPECT_EQ(2831, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); EXPECT_EQ(2692, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true); + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); EXPECT_EQ(2064, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true); + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); EXPECT_EQ(2884, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize); EXPECT_EQ(2064, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true); EXPECT_EQ(2884, result.states.getNonZeroCount()); - EXPECT_TRUE(static_cast(result.player1Strategy)); - EXPECT_TRUE(static_cast(result.player2Strategy)); + EXPECT_TRUE(result.hasPlayer1Strategy()); + EXPECT_TRUE(result.hasPlayer2Strategy()); // Check the validity of the strategies. Start by checking whether only prob1 states have a strategy. storm::dd::Bdd nonProb1StatesWithStrategy = !result.states && result.player1Strategy.get();