From 88bcd7d74cd1d46e9e38321dfeeeab04c71a2ae5 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 17 Sep 2015 19:11:36 +0200 Subject: [PATCH] deadlock states now get fixed in abstract game Former-commit-id: efaa5d007e80d6ba0aa524feb4174cc8a2240d40 --- .../prism/menu_games/AbstractProgram.cpp | 25 ++++++++++++++++--- .../prism/menu_games/AbstractProgram.h | 6 +++++ .../menu_games/AbstractionDdInformation.cpp | 3 ++- .../menu_games/AbstractionDdInformation.h | 3 +++ 4 files changed, 33 insertions(+), 4 deletions(-) diff --git a/src/storage/prism/menu_games/AbstractProgram.cpp b/src/storage/prism/menu_games/AbstractProgram.cpp index a9c0f7aa5..47f617dd0 100644 --- a/src/storage/prism/menu_games/AbstractProgram.cpp +++ b/src/storage/prism/menu_games/AbstractProgram.cpp @@ -14,7 +14,7 @@ namespace storm { namespace menu_games { template - AbstractProgram::AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector const& initialPredicates, std::unique_ptr&& smtSolverFactory, bool addAllGuards) : smtSolverFactory(std::move(smtSolverFactory)), ddInformation(std::make_shared>()), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables(), program.getAllRangeExpressions()), modules(), program(program), initialStateAbstractor(expressionInformation, ddInformation, *this->smtSolverFactory) { + AbstractProgram::AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector const& initialPredicates, std::unique_ptr&& smtSolverFactory, bool addAllGuards) : smtSolverFactory(std::move(smtSolverFactory)), ddInformation(std::make_shared>()), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables(), program.getAllRangeExpressions()), modules(), program(program), initialStateAbstractor(expressionInformation, ddInformation, *this->smtSolverFactory), lastAbstractBdd(ddInformation.manager->getBddZero()), lastAbstractAdd(ddInformation.manager->getAddZero()) { // For now, we assume that there is a single module. If the program has more than one module, it needs // to be flattened before the procedure. @@ -91,6 +91,14 @@ namespace storm { storm::dd::Add AbstractProgram::getAbstractAdd() { // As long as there is only one module, we only build its game representation. std::pair, uint_fast64_t> gameBdd = modules.front().getAbstractBdd(); + + // If the abstraction did not change, we can return the most recenty obtained ADD. + if (gameBdd.first == lastAbstractBdd) { + return lastAbstractAdd; + } + + // Otherwise, we remember that the abstract BDD changed and perform a reachability analysis. + lastAbstractBdd = gameBdd.first; // Construct a set of all unnecessary variables, so we can abstract from it. std::set variablesToAbstract = {ddInformation.commandDdVariable, ddInformation.updateDdVariable}; @@ -99,11 +107,22 @@ namespace storm { } // Do a reachability analysis on the raw transition relation. - storm::dd::Bdd transitionRelation = gameBdd.first.existsAbstract(variablesToAbstract); + storm::dd::Bdd transitionRelation = lastAbstractBdd.existsAbstract(variablesToAbstract); storm::dd::Bdd reachableStates = this->getReachableStates(initialStateAbstractor.getAbstractStates(), transitionRelation); + // Find the deadlock states in the model. + storm::dd::Bdd deadlockStates = transitionRelation.existsAbstract(ddInformation.successorVariables); + deadlockStates = reachableStates && !deadlockStates; + + // If there are deadlock states, we fix them now. + storm::dd::Add deadlockTransitions = ddInformation.manager->getAddZero(); + if (!deadlockStates.isZero()) { + deadlockTransitions = (deadlockStates && ddInformation.allPredicateIdentities && ddInformation.manager->getEncoding(ddInformation.commandDdVariable, 0) && ddInformation.manager->getEncoding(ddInformation.updateDdVariable, 0) && ddInformation.getMissingOptionVariableCube(0, gameBdd.second)).toAdd(); + } + // Construct the final game by cutting away the transitions of unreachable states. - return (gameBdd.first && reachableStates).toAdd() * commandUpdateProbabilitiesAdd; + lastAbstractAdd = (lastAbstractBdd && reachableStates).toAdd() * commandUpdateProbabilitiesAdd + deadlockTransitions; + return lastAbstractAdd; } template diff --git a/src/storage/prism/menu_games/AbstractProgram.h b/src/storage/prism/menu_games/AbstractProgram.h index d9cf6b4ad..88094a632 100644 --- a/src/storage/prism/menu_games/AbstractProgram.h +++ b/src/storage/prism/menu_games/AbstractProgram.h @@ -82,6 +82,12 @@ namespace storm { // An ADD characterizing the probabilities of commands and their updates. storm::dd::Add commandUpdateProbabilitiesAdd; + + // A BDD that is the result of the last abstraction of the system. + storm::dd::Bdd lastAbstractBdd; + + // An ADD that is the result of the last abstraction of the system. + storm::dd::Add lastAbstractAdd; }; } } diff --git a/src/storage/prism/menu_games/AbstractionDdInformation.cpp b/src/storage/prism/menu_games/AbstractionDdInformation.cpp index 0848ceffb..6395fa951 100644 --- a/src/storage/prism/menu_games/AbstractionDdInformation.cpp +++ b/src/storage/prism/menu_games/AbstractionDdInformation.cpp @@ -14,7 +14,7 @@ namespace storm { namespace menu_games { template - AbstractionDdInformation::AbstractionDdInformation(std::shared_ptr> const& manager) : manager(manager) { + AbstractionDdInformation::AbstractionDdInformation(std::shared_ptr> const& manager) : manager(manager), allPredicateIdentities(manager->getBddOne()) { // Intentionally left empty. } @@ -40,6 +40,7 @@ namespace storm { predicateDdVariables.push_back(newMetaVariable); predicateBdds.emplace_back(manager->getEncoding(newMetaVariable.first, 1), manager->getEncoding(newMetaVariable.second, 1)); predicateIdentities.push_back(manager->getIdentity(newMetaVariable.first).equals(manager->getIdentity(newMetaVariable.second)).toBdd()); + allPredicateIdentities &= predicateIdentities.back(); sourceVariables.insert(newMetaVariable.first); successorVariables.insert(newMetaVariable.second); } diff --git a/src/storage/prism/menu_games/AbstractionDdInformation.h b/src/storage/prism/menu_games/AbstractionDdInformation.h index cc20253da..ac5fa4316 100644 --- a/src/storage/prism/menu_games/AbstractionDdInformation.h +++ b/src/storage/prism/menu_games/AbstractionDdInformation.h @@ -89,6 +89,9 @@ namespace storm { // The BDDs representing the predicate identities (i.e. source and successor variable have the same truth value). std::vector> predicateIdentities; + // A BDD that represents the identity of all predicate variables. + storm::dd::Bdd allPredicateIdentities; + // The DD variable encoding the command (i.e., the nondeterministic choices of player 1). storm::expressions::Variable commandDdVariable;