diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 6c408f386..16d63f245 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -101,14 +101,28 @@ namespace storm { targetStates |= game.getBottomStates(); } + transitionMatrixBdd.template toAdd().exportToDot("transbdd.dot"); + // 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, true); + storm::utility::graph::GameProb01Result 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 prob0Max = storm::utility::graph::performProb0(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); storm::utility::graph::GameProb01Result 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().exportToDot("prob0_min_pl1_strat.dot"); + prob0Min.getPlayer2Strategy().template toAdd().exportToDot("prob0_min_pl2_strat.dot"); + + prob1Max.getPlayer1Strategy().template toAdd().exportToDot("prob1_max_pl1_strat.dot"); + prob1Max.getPlayer2Strategy().template toAdd().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."); diff --git a/src/utility/graph.h b/src/utility/graph.h index ce5f1cd2f..d57c8a731 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -528,6 +528,26 @@ namespace storm { // Intentionally left empty. } + bool hasPlayer1Strategy() const { + return static_cast(player1Strategy); + } + + storm::dd::Bdd const& getPlayer1Strategy() { + return player1Strategy.get(); + } + + bool hasPlayer2Strategy() const { + return static_cast(player2Strategy); + } + + storm::dd::Bdd const& getPlayer2Strategy() { + return player2Strategy.get(); + } + + storm::dd::Bdd const& getStates() const { + return states; + } + storm::dd::Bdd states; boost::optional> player1Strategy; boost::optional> player2Strategy; diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp index 33c31ac5b..79e52c8d8 100644 --- a/test/functional/utility/GraphTest.cpp +++ b/test/functional/utility/GraphTest.cpp @@ -215,30 +215,30 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { 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); - EXPECT_EQ(1, result.states.getNonZeroCount()); + EXPECT_EQ(2, result.states.getNonZeroCount()); EXPECT_TRUE(static_cast(result.player1Strategy)); EXPECT_TRUE(static_cast(result.player2Strategy)); result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true); - EXPECT_EQ(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(result.player1Strategy)); EXPECT_TRUE(static_cast(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(result.player1Strategy)); EXPECT_TRUE(static_cast(result.player2Strategy)); @@ -259,32 +259,32 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { // Proceed by checking whether they select exactly one action in each state. storm::dd::Add stateDistributionsUnderStrategies = (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd() * result.player2Strategy.get().template toAdd()).sumAbstract(game.getColumnVariables());; - EXPECT_EQ(0, stateDistributionsUnderStrategies.getNonZeroCount()); + 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 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(result.player1Strategy)); EXPECT_TRUE(static_cast(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() * result.player2Strategy.get().template toAdd()).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());