From 1bb116dd1ce51a3a14fb5d91fc8b0f034c897536 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 17 Aug 2016 20:14:58 +0200 Subject: [PATCH 1/3] some more work on game-based model checker Former-commit-id: 50399c3d7ca4273bae8f612e3bfa6a600e82caa0 --- src/abstraction/prism/AbstractProgram.cpp | 40 +++++++- .../abstraction/GameBasedMdpModelChecker.cpp | 94 ++++++++++++++----- .../abstraction/GameBasedMdpModelChecker.h | 18 +++- .../SymbolicQualitativeCheckResult.cpp | 20 +++- .../results/SymbolicQualitativeCheckResult.h | 4 + .../SymbolicQuantitativeCheckResult.cpp | 5 + .../results/SymbolicQuantitativeCheckResult.h | 1 + src/utility/graph.h | 12 ++- 8 files changed, 158 insertions(+), 36 deletions(-) diff --git a/src/abstraction/prism/AbstractProgram.cpp b/src/abstraction/prism/AbstractProgram.cpp index 7a1b2255f..f5a1d0763 100644 --- a/src/abstraction/prism/AbstractProgram.cpp +++ b/src/abstraction/prism/AbstractProgram.cpp @@ -278,16 +278,46 @@ namespace storm { 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; -// -// } + for (auto stateValue : currentGame->getTransitionMatrix()) { + std::stringstream sourceStateName; + std::stringstream successorStateName; + for (auto const& var : currentGame->getRowVariables()) { + if (stateValue.first.getBooleanValue(var)) { + sourceStateName << "1"; + } else { + sourceStateName << "0"; + } + } + for (auto const& var : currentGame->getColumnVariables()) { + if (stateValue.first.getBooleanValue(var)) { + successorStateName << "1"; + } else { + successorStateName << "0"; + } + } + uint_fast64_t pl1Index = 0; + for (uint_fast64_t player1VariableIndex = 0; player1VariableIndex < abstractionInformation.getPlayer1VariableCount(); ++player1VariableIndex) { + pl1Index <<= 1; + if (stateValue.first.getBooleanValue(abstractionInformation.getPlayer1Variables()[player1VariableIndex])) { + pl1Index |= 1; + } + } + uint_fast64_t pl2Index = 0; + for (uint_fast64_t player2VariableIndex = 0; player2VariableIndex < currentGame->getPlayer2Variables().size(); ++player2VariableIndex) { + pl2Index <<= 1; + if (stateValue.first.getBooleanValue(abstractionInformation.getPlayer2Variables()[player2VariableIndex])) { + pl2Index |= 1; + } + } + out << "\tplp_" << sourceStateName.str() << "_" << pl1Index << "_" << pl2Index << " -> pl1_" << successorStateName.str() << " [ label=\"" << stateValue.second << "\"];" << std::endl; + } out << "}" << std::endl; } diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index f48c6fe9e..81cf6ca20 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -1,14 +1,17 @@ #include "src/modelchecker/abstraction/GameBasedMdpModelChecker.h" +#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" + #include "src/models/symbolic/StandardRewardModel.h" #include "src/storage/expressions/ExpressionManager.h" +#include "src/storage/dd/DdManager.h" + #include "src/abstraction/prism/PrismMenuGameAbstractor.h" #include "src/logic/FragmentSpecification.h" -#include "src/utility/graph.h" #include "src/utility/macros.h" #include "src/exceptions/NotSupportedException.h" @@ -18,6 +21,13 @@ namespace storm { namespace modelchecker { + namespace detail { + template + GameProb01Result::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) : min(std::make_pair(prob0Min, prob1Min)), max(std::make_pair(prob0Max, prob1Max)) { + // Intentionally left empty. + } + } + template GameBasedMdpModelChecker::GameBasedMdpModelChecker(storm::prism::Program const& program, std::shared_ptr const& smtSolverFactory) : originalProgram(program), smtSolverFactory(smtSolverFactory) { STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently only DTMCs/MDPs are supported by the game-based model checker."); @@ -54,10 +64,39 @@ namespace storm { return performGameBasedAbstractionRefinement(checkTask.substituteFormula(pathFormula), originalProgram.getManager().boolean(true), getExpression(pathFormula.getSubformula())); } + template + bool getResultConsideringBound(ValueType const& value, storm::logic::Bound const& bound) { + if (storm::logic::isLowerBound(bound.comparisonType)) { + if (storm::logic::isStrict(bound.comparisonType)) { + return value > bound.threshold; + } else { + return value >= bound.threshold; + } + } else { + if (storm::logic::isStrict(bound.comparisonType)) { + return value < bound.threshold; + } else { + return value <= bound.threshold; + } + } + } + + 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) { + if (checkTask.isBoundSet()) { + bool result = getResultConsideringBound(prob0 ? storm::utility::zero() : storm::utility::one(), checkTask.getBound()); + return std::make_unique>(reachableStates, initialStates, result ? initialStates : ddManager.getBddZero()); + } else { + return std::make_unique>(reachableStates, initialStates, prob0 ? ddManager.template getAddZero() : initialStates.template toAdd()); + } + } + 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."); + // Optimization: do not compute both bounds if not necessary (e.g. if bound given and exceeded, etc.) + // Set up initial predicates. std::vector initialPredicates; initialPredicates.push_back(targetStateExpression); @@ -72,13 +111,39 @@ namespace storm { // 1. build initial abstraction based on the the constraint expression (if not 'true') and the target state expression. storm::abstraction::MenuGame game = abstractor.abstract(); - abstractor.exportToDot("game.dot"); STORM_LOG_DEBUG("Initial abstraction has " << game.getNumberOfStates() << " (player 1) states and " << game.getNumberOfTransitions() << " transitions."); + + // 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); + + // 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(); + storm::dd::Bdd maybeMax = !(prob01.max.first.states || prob01.max.second.states) && game.getReachableStates(); + + // 4. if the initial states are not maybe states, then we can refine at this point. + storm::dd::Bdd initialMaybeStates = game.getInitialStates() && (maybeMin || maybeMax); + if (initialMaybeStates.isZero()) { + // In this case, we know the result for the initial states for both player 2 minimizing and maximizing. + + // 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()) { + getResultAfterQualitativeCheck(checkTask, game.getManager(), game.getReachableStates(), game.getInitialStates(), true); + } + + // 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()) { + getResultAfterQualitativeCheck(checkTask, game.getManager(), game.getReachableStates(), game.getInitialStates(), false); + } + + // 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. + + + } + - // 2. solve the game wrt. to min/max as given by checkTask and min/max for the abstraction player to obtain two bounds. - // Note that we have to deal with bottom states if not all guards were added in the beginning. - // Also note that it might be the case that not both bounds need to be computed if there is a bound given in checkTask. - computeProb01States(player1Direction, game, constraintExpression, targetStateExpression); // std::unique_ptr> gameSolverFactory = std::make_unique>(); // gameSolverFactory->create(game.getTransitionMatrix(), game.getReachableStates()); @@ -92,7 +157,7 @@ namespace storm { } template - void GameBasedMdpModelChecker::computeProb01States(storm::OptimizationDirection player1Direction, storm::abstraction::MenuGame const& game, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) { + 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(); storm::dd::Bdd bottomStatesBdd = game.getBottomStates(); @@ -100,8 +165,6 @@ namespace storm { if (player1Direction == storm::OptimizationDirection::Minimize) { 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); @@ -111,21 +174,10 @@ namespace storm { 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."); + return detail::GameProb01Result(prob0Min, prob1Min, prob0Max, prob1Max); } template diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.h b/src/modelchecker/abstraction/GameBasedMdpModelChecker.h index a23f68021..a7a9ae485 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.h +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.h @@ -3,12 +3,13 @@ #include "src/modelchecker/AbstractModelChecker.h" -#include "src/utility/solver.h" - #include "src/storage/prism/Program.h" #include "src/storage/dd/DdType.h" +#include "src/utility/solver.h" +#include "src/utility/graph.h" + namespace storm { namespace abstraction { template @@ -16,6 +17,17 @@ namespace storm { } namespace modelchecker { + namespace detail { + template + struct GameProb01Result { + public: + 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; + std::pair, storm::utility::graph::GameProb01Result> max; + }; + } + template class GameBasedMdpModelChecker : public AbstractModelChecker { public: @@ -38,7 +50,7 @@ namespace storm { private: std::unique_ptr performGameBasedAbstractionRefinement(CheckTask const& checkTask, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression); - void 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::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression); storm::expressions::Expression getExpression(storm::logic::Formula const& formula); diff --git a/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp b/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp index 2275b942f..6d4ae0e44 100644 --- a/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp +++ b/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp @@ -6,7 +6,12 @@ namespace storm { namespace modelchecker { template - SymbolicQualitativeCheckResult::SymbolicQualitativeCheckResult(storm::dd::Bdd const& reachableStates, storm::dd::Bdd const& truthValues) : reachableStates(reachableStates), truthValues(truthValues) { + SymbolicQualitativeCheckResult::SymbolicQualitativeCheckResult(storm::dd::Bdd const& reachableStates, storm::dd::Bdd const& truthValues) : reachableStates(reachableStates), states(reachableStates), truthValues(truthValues) { + // Intentionally left empty. + } + + template + SymbolicQualitativeCheckResult::SymbolicQualitativeCheckResult(storm::dd::Bdd const& reachableStates, storm::dd::Bdd const& states, storm::dd::Bdd const& truthValues) : reachableStates(reachableStates), states(states), truthValues(truthValues) { // Intentionally left empty. } @@ -17,7 +22,7 @@ namespace storm { template bool SymbolicQualitativeCheckResult::isResultForAllStates() const { - return true; + return reachableStates == states; } template @@ -51,10 +56,14 @@ namespace storm { template std::ostream& SymbolicQualitativeCheckResult::writeToStream(std::ostream& out) const { - if (this->truthValues.isZero()) { - out << "[false]" << std::endl; - } else { + if (states == truthValues) { out << "[true]" << std::endl; + } else { + if (truthValues.isZero()) { + out << "[false]" << std::endl; + } else { + out << "[true false]" << std::endl; + } } return out; } @@ -62,6 +71,7 @@ namespace storm { template void SymbolicQualitativeCheckResult::filter(QualitativeCheckResult const& filter) { STORM_LOG_THROW(filter.isSymbolicQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot filter symbolic check result with non-symbolic filter."); + this->states &= filter.asSymbolicQualitativeCheckResult().getTruthValuesVector();; this->truthValues &= filter.asSymbolicQualitativeCheckResult().getTruthValuesVector(); } diff --git a/src/modelchecker/results/SymbolicQualitativeCheckResult.h b/src/modelchecker/results/SymbolicQualitativeCheckResult.h index 3e94f5ee8..70f279f9b 100644 --- a/src/modelchecker/results/SymbolicQualitativeCheckResult.h +++ b/src/modelchecker/results/SymbolicQualitativeCheckResult.h @@ -13,6 +13,7 @@ namespace storm { public: SymbolicQualitativeCheckResult() = default; SymbolicQualitativeCheckResult(storm::dd::Bdd const& reachableStates, storm::dd::Bdd const& truthValues); + SymbolicQualitativeCheckResult(storm::dd::Bdd const& reachableStates, storm::dd::Bdd const& states, storm::dd::Bdd const& truthValues); SymbolicQualitativeCheckResult(SymbolicQualitativeCheckResult const& other) = default; SymbolicQualitativeCheckResult& operator=(SymbolicQualitativeCheckResult const& other) = default; @@ -40,6 +41,9 @@ namespace storm { // The set of all reachable states. storm::dd::Bdd reachableStates; + // The states for which this check result contains a truth value. + storm::dd::Bdd states; + // The values of the qualitative check result. storm::dd::Bdd truthValues; }; diff --git a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp index 0acd3ada3..5f3bc88f0 100644 --- a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp @@ -15,6 +15,11 @@ namespace storm { // Intentionally left empty. } + template + SymbolicQuantitativeCheckResult::SymbolicQuantitativeCheckResult(storm::dd::Bdd const& reachableStates, storm::dd::Bdd const& states, storm::dd::Add const& values) : reachableStates(reachableStates), states(states), values(values) { + // Intentionally left empty. + } + template std::unique_ptr SymbolicQuantitativeCheckResult::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const { storm::dd::Bdd states; diff --git a/src/modelchecker/results/SymbolicQuantitativeCheckResult.h b/src/modelchecker/results/SymbolicQuantitativeCheckResult.h index 9cbb272a3..2fad3d1ac 100644 --- a/src/modelchecker/results/SymbolicQuantitativeCheckResult.h +++ b/src/modelchecker/results/SymbolicQuantitativeCheckResult.h @@ -13,6 +13,7 @@ namespace storm { public: SymbolicQuantitativeCheckResult() = default; SymbolicQuantitativeCheckResult(storm::dd::Bdd const& reachableStates, storm::dd::Add const& values); + SymbolicQuantitativeCheckResult(storm::dd::Bdd const& reachableStates, storm::dd::Bdd const& states, storm::dd::Add const& values); SymbolicQuantitativeCheckResult(SymbolicQuantitativeCheckResult const& other) = default; SymbolicQuantitativeCheckResult& operator=(SymbolicQuantitativeCheckResult const& other) = default; diff --git a/src/utility/graph.h b/src/utility/graph.h index d57c8a731..cd03b42dd 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -532,18 +532,26 @@ namespace storm { return static_cast(player1Strategy); } - storm::dd::Bdd const& getPlayer1Strategy() { + storm::dd::Bdd const& getPlayer1Strategy() const { return player1Strategy.get(); } + + boost::optional> const& getOptionalPlayer1Strategy() { + return player1Strategy; + } bool hasPlayer2Strategy() const { return static_cast(player2Strategy); } - storm::dd::Bdd const& getPlayer2Strategy() { + storm::dd::Bdd const& getPlayer2Strategy() const { return player2Strategy.get(); } + boost::optional> const& getOptionalPlayer2Strategy() { + return player2Strategy; + } + storm::dd::Bdd const& getStates() const { return states; } From 4c9f22c7c2363b322ebae92a6db996e4cc8b8150 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 17 Aug 2016 20:23:53 +0200 Subject: [PATCH 2/3] included missing header Former-commit-id: a1e81897dddc2c011371ae7cfd5ab4c5530326ae --- src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 81cf6ca20..5859a8d58 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -1,6 +1,7 @@ #include "src/modelchecker/abstraction/GameBasedMdpModelChecker.h" #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" +#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "src/models/symbolic/StandardRewardModel.h" From 469d856267bf80e5ccb41183f32ddfafed9a1552 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 17 Aug 2016 22:03:57 +0200 Subject: [PATCH 3/3] fixed bug in CUDD implementation of existsAbstractRepresentative Former-commit-id: 0e0d5ca0f094b6ad7a945154d5386c40b89a0b68 --- resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c b/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c index 2c01c6404..b9f6a7db9 100644 --- a/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c +++ b/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c @@ -614,7 +614,7 @@ cuddBddExistAbstractRepresentativeRecur( // FIXME if (res1 == one) { if (F->ref != 1) { - cuddCacheInsert2(manager, Cudd_bddExistAbstractRepresentative, f, cube, one); + cuddCacheInsert2(manager, Cudd_bddExistAbstractRepresentative, f, cube, Cudd_Not(cube)); } return(Cudd_Not(cube)); }