From cc550984b368cbe889cfa2aa54d638d0963201de Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 23 Aug 2016 09:59:01 +0200 Subject: [PATCH] enabling qualitative answers of game-based model checker Former-commit-id: b5eca1d6716a4bd4e605e72adc6c9d05f772f8ad --- .../abstraction/GameBasedMdpModelChecker.cpp | 97 ++++++++++++------- .../abstraction/GameBasedMdpModelChecker.h | 3 +- src/utility/graph.h | 1 + 3 files changed, 64 insertions(+), 37 deletions(-) diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 250742025..86c0072eb 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -85,8 +85,35 @@ namespace storm { } template - std::unique_ptr getResultAfterQualitativeCheck(CheckTask const& checkTask, storm::dd::DdManager const& ddManager, storm::dd::Bdd const& reachableStates, storm::dd::Bdd const& initialStates, bool prob0) { - return std::make_unique>(storm::storage::sparse::state_type(0), prob0 ? storm::utility::zero() : storm::utility::one()); + std::unique_ptr checkForResultAfterQualitativeCheck(CheckTask const& checkTask, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& statesMin, storm::dd::Bdd const& statesMax, bool prob0) { + std::unique_ptr result; + if ((initialStates && statesMin && statesMax) == initialStates) { + result = std::make_unique>(storm::storage::sparse::state_type(0), prob0 ? storm::utility::zero() : storm::utility::one()); + } + return result; + } + + template + std::unique_ptr checkForResultAfterQualitativeCheck(CheckTask const& checkTask, storm::OptimizationDirection player2Direction, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& prob0, storm::dd::Bdd const& prob1) { + std::unique_ptr result; + + if (checkTask.isBoundSet()) { + if (player2Direction == storm::OptimizationDirection::Minimize && storm::logic::isLowerBound(checkTask.getBoundComparisonType())) { + if ((prob1 && initialStates) == initialStates) { + result = std::make_unique>(storm::storage::sparse::state_type(0), storm::utility::one()); + } else if (checkTask.isQualitativeSet()) { + result = std::make_unique>(storm::storage::sparse::state_type(0), ValueType(0.5)); + } + } else if (player2Direction == storm::OptimizationDirection::Maximize && !storm::logic::isLowerBound(checkTask.getBoundComparisonType())) { + if ((prob0 && initialStates) == initialStates) { + result = std::make_unique>(storm::storage::sparse::state_type(0), storm::utility::zero()); + } else if (checkTask.isQualitativeSet()) { + result = std::make_unique>(storm::storage::sparse::state_type(0), ValueType(0.5)); + } + } + } + + return result; } template @@ -192,7 +219,21 @@ namespace storm { 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, transitionMatrixBdd, constraintExpression, targetStateExpression); + detail::GameProb01Result prob01; + storm::dd::Bdd targetStates = game.getStates(targetStateExpression); + if (player1Direction == storm::OptimizationDirection::Minimize) { + targetStates |= game.getBottomStates(); + } + prob01.min = computeProb01States(player1Direction, storm::OptimizationDirection::Minimize, game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates); + std::unique_ptr result = checkForResultAfterQualitativeCheck(checkTask, storm::OptimizationDirection::Minimize, game.getInitialStates(), prob01.min.first.states, prob01.min.second.states); + if (result) { + return result; + } + prob01.max = computeProb01States(player1Direction, storm::OptimizationDirection::Maximize, game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates); + result = checkForResultAfterQualitativeCheck(checkTask, storm::OptimizationDirection::Maximize, game.getInitialStates(), prob01.max.first.states, prob01.max.second.states); + if (result) { + return result; + } // 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(); @@ -204,16 +245,14 @@ namespace storm { // In this case, we know the result for the initial states for both player 2 minimizing and maximizing. STORM_LOG_TRACE("No initial state is a 'maybe' state. Refining abstraction based on qualitative check."); - // If the result is 0 independent of the player 2 strategy, then we know the final result and can return it. - storm::dd::Bdd tmp = game.getInitialStates() && prob01.min.first.states && prob01.max.first.states; - if (tmp == game.getInitialStates()) { - return getResultAfterQualitativeCheck(checkTask, game.getManager(), game.getReachableStates(), game.getInitialStates(), true); + // Check whether we can already give the answer based on the current information. + result = checkForResultAfterQualitativeCheck(checkTask, game.getInitialStates(), prob01.min.first.states, prob01.max.first.states, true); + if (result) { + return result; } - - // If the result is 1 independent of the player 2 strategy, then we know the final result and can return it. - tmp = game.getInitialStates() && prob01.min.second.states && prob01.max.second.states; - if (tmp == game.getInitialStates()) { - return getResultAfterQualitativeCheck(checkTask, game.getManager(), game.getReachableStates(), game.getInitialStates(), false); + result = checkForResultAfterQualitativeCheck(checkTask, game.getInitialStates(), prob01.min.second.states, prob01.max.second.states, false); + if (result) { + return result; } // If we get here, the initial states were all identified as prob0/1 states, but the value (0 or 1) @@ -233,32 +272,18 @@ namespace storm { } template - 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(); + std::pair, storm::utility::graph::GameProb01Result> GameBasedMdpModelChecker::computeProb01States(storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates) { + // Compute the states with probability 0/1. + storm::utility::graph::GameProb01Result prob0 = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, player2Direction, player2Direction == storm::OptimizationDirection::Minimize, player2Direction == storm::OptimizationDirection::Minimize); + storm::utility::graph::GameProb01Result prob1 = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, player2Direction, player2Direction == storm::OptimizationDirection::Maximize, player2Direction == storm::OptimizationDirection::Maximize); - storm::dd::Bdd targetStates = game.getStates(targetStateExpression); - if (player1Direction == storm::OptimizationDirection::Minimize) { - targetStates |= game.getBottomStates(); - } - - // 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, 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, false); - storm::utility::graph::GameProb01Result prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true); - prob1Max.getPlayer1Strategy().template toAdd().exportToDot("prob1maxstrat.dot"); - - 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."); + STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Minimize || prob0.hasPlayer1Strategy(), "Unable to proceed without strategy."); + STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Minimize || prob0.hasPlayer2Strategy(), "Unable to proceed without strategy."); + STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Maximize || prob0.hasPlayer1Strategy(), "Unable to proceed without strategy."); + STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Maximize || prob0.hasPlayer2Strategy(), "Unable to proceed without strategy."); - STORM_LOG_TRACE("Min: " << prob0Min.states.getNonZeroCount() << " no states, " << prob1Min.states.getNonZeroCount() << " yes states."); - STORM_LOG_TRACE("Max: " << prob0Max.states.getNonZeroCount() << " no states, " << prob1Max.states.getNonZeroCount() << " yes states."); - - return detail::GameProb01Result(prob0Min, prob1Min, prob0Max, prob1Max); + STORM_LOG_TRACE("Player 1: " << player1Direction << ", player 2: " << player2Direction << ": " << prob0.states.getNonZeroCount() << " 'no' states, " << prob1.states.getNonZeroCount() << " 'yes' states."); + return std::make_pair(prob0, prob1); } template diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.h b/src/modelchecker/abstraction/GameBasedMdpModelChecker.h index 2e480e9fa..139c3b306 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.h +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.h @@ -21,6 +21,7 @@ namespace storm { template struct GameProb01Result { public: + GameProb01Result() = default; GameProb01Result(storm::utility::graph::GameProb01Result const& prob0Min, storm::utility::graph::GameProb01Result const& prob1Min, storm::utility::graph::GameProb01Result const& prob0Max, storm::utility::graph::GameProb01Result const& prob1Max); std::pair, storm::utility::graph::GameProb01Result> min; @@ -50,7 +51,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::dd::Bdd const& transitionMatrixBdd, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression); + std::pair, storm::utility::graph::GameProb01Result> computeProb01States(storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates); storm::expressions::Expression getExpression(storm::logic::Formula const& formula); diff --git a/src/utility/graph.h b/src/utility/graph.h index 07b0aafa8..89ceafc3e 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -524,6 +524,7 @@ namespace storm { template struct GameProb01Result { + GameProb01Result() = default; GameProb01Result(storm::dd::Bdd const& states, boost::optional> const& player1Strategy = boost::none, boost::optional> const& player2Strategy = boost::none) : states(states), player1Strategy(player1Strategy), player2Strategy(player2Strategy) { // Intentionally left empty. }