From e8b7928831d7d559e88b9470525904940b0a6080 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 22 Sep 2015 17:53:27 +0200 Subject: [PATCH] fixed minor bug Former-commit-id: 6d208b877ab1c844fd34684693b9975772beb2cd --- src/utility/graph.cpp | 2 +- test/functional/utility/GraphTest.cpp | 19 ++++++++++--------- 2 files changed, 11 insertions(+), 10 deletions(-) diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp index 9ea5be105..34e10467d 100644 --- a/src/utility/graph.cpp +++ b/src/utility/graph.cpp @@ -844,7 +844,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 = produceStrategies && (player1Strategy == OptimizationDirection::Maximize || player2Strategy == OptimizationDirection::Maximize); + produceStrategiesInIteration = !produceStrategiesInIteration && produceStrategies && (player1Strategy == OptimizationDirection::Maximize || player2Strategy == OptimizationDirection::Maximize); } else { // Otherwise, we use the current hypothesis for the states with probability 1 as the new maybe // state set. diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp index 4f4814dbd..6ac99e129 100644 --- a/test/functional/utility/GraphTest.cpp +++ b/test/functional/utility/GraphTest.cpp @@ -107,8 +107,6 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); - - game.getQualitativeTransitionMatrix().toAdd().exportToDot("trans.dot"); // The target states are those states where !(s < 3). storm::dd::Bdd targetStates = game.getStates(initialPredicates[0], true); @@ -138,14 +136,9 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { 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_TRUE(static_cast(result.player1Strategy)); EXPECT_TRUE(static_cast(result.player2Strategy)); - - result.player1Strategy.get().toAdd().exportToDot("player1.dot"); - result.player2Strategy.get().toAdd().exportToDot("player2.dot"); - exit(-1); - + abstractProgram.refine({manager.getVariableExpression("s") < manager.integer(2)}); game = abstractProgram.getAbstractGame(); @@ -154,6 +147,8 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { 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_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(3, result.states.getNonZeroCount()); @@ -175,6 +170,8 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { 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_TRUE(static_cast(result.player1Strategy)); + EXPECT_TRUE(static_cast(result.player2Strategy)); } TEST(GraphTest, SymbolicProb01StochasticGameTwoDice) { @@ -226,8 +223,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); + storm::utility::graph::GameProb01Result result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true); EXPECT_EQ(153, 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()); @@ -249,6 +248,8 @@ TEST(GraphTest, SymbolicProb01StochasticGameTwoDice) { result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true); EXPECT_EQ(1, result.states.getNonZeroCount()); + EXPECT_TRUE(static_cast(result.player1Strategy)); + EXPECT_TRUE(static_cast(result.player2Strategy)); } #endif