From 8574d474a436eb8a1efe0efd09939220b0c4bf17 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 23 Sep 2015 17:11:43 +0200 Subject: [PATCH] added support for computation of bottom states. not yet done Former-commit-id: 49c2a28b2862f574d549d6623ec03c4964967920 --- .../prism/menu_games/AbstractProgram.cpp | 25 ++++++++++++++++--- .../prism/menu_games/AbstractProgram.h | 6 +++++ src/storage/prism/menu_games/MenuGame.cpp | 8 +++++- src/storage/prism/menu_games/MenuGame.h | 16 ++++++++++-- .../prism/menu_games/StateSetAbstractor.cpp | 19 +++++++++----- .../prism/menu_games/StateSetAbstractor.h | 5 +++- 6 files changed, 65 insertions(+), 14 deletions(-) diff --git a/src/storage/prism/menu_games/AbstractProgram.cpp b/src/storage/prism/menu_games/AbstractProgram.cpp index 53cafc69e..3105e82a5 100644 --- a/src/storage/prism/menu_games/AbstractProgram.cpp +++ b/src/storage/prism/menu_games/AbstractProgram.cpp @@ -17,7 +17,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), currentGame(nullptr) { + 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), addedAllGuards(addAllGuards), bottomStateAbstractor(expressionInformation, ddInformation, *this->smtSolverFactory), currentGame(nullptr) { // 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. @@ -30,6 +30,10 @@ namespace storm { for (auto const& command : module.getCommands()) { if (addAllGuards) { expressionInformation.predicates.push_back(command.getGuardExpression()); + } else { + // If not all guards were added, we also need to populate the bottom state abstractor. + std::cout << "adding " << !command.getGuardExpression() << std::endl; + bottomStateAbstractor.addPredicate(!command.getGuardExpression()); } maximalUpdateCount = std::max(maximalUpdateCount, static_cast(command.getNumberOfUpdates())); } @@ -100,7 +104,10 @@ namespace storm { // Refine initial state abstractor. initialStateAbstractor.refine(newPredicateIndices); - // Finally, we rebuild the game. + // Refine bottom state abstractor. + bottomStateAbstractor.refine(newPredicateIndices); + + // Finally, we rebuild the game.. currentGame = buildGame(); } @@ -122,7 +129,7 @@ namespace storm { } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given predicate is illegal, since it was neither used as an initial predicate nor used to refine the abstraction."); } - + template std::unique_ptr> AbstractProgram::buildGame() { // As long as there is only one module, we only build its game representation. @@ -138,6 +145,16 @@ namespace storm { storm::dd::Bdd transitionRelation = gameBdd.first.existsAbstract(variablesToAbstract); storm::dd::Bdd initialStates = initialStateAbstractor.getAbstractStates(); storm::dd::Bdd reachableStates = this->getReachableStates(initialStates, transitionRelation); + + // Determine the bottom states. + storm::dd::Bdd bottomStates; + if (addedAllGuards) { + bottomStates = ddInformation.manager->getBddZero(); + } else { + bottomStates = bottomStateAbstractor.getAbstractStates(); + } + + std::cout << "found " << (reachableStates && bottomStates).getNonZeroCount() << " reachable bottom states" << std::endl; // Find the deadlock states in the model. storm::dd::Bdd deadlockStates = transitionRelation.existsAbstract(ddInformation.successorVariables); @@ -160,7 +177,7 @@ namespace storm { std::set allNondeterminismVariables = usedPlayer2Variables; allNondeterminismVariables.insert(ddInformation.commandDdVariable); - return std::unique_ptr>(new MenuGame(ddInformation.manager, reachableStates, initialStates, transitionMatrix, ddInformation.sourceVariables, ddInformation.successorVariables, ddInformation.predicateDdVariables, {ddInformation.commandDdVariable}, usedPlayer2Variables, allNondeterminismVariables, ddInformation.updateDdVariable, ddInformation.expressionToBddMap)); + return std::unique_ptr>(new MenuGame(ddInformation.manager, reachableStates, initialStates, transitionMatrix, bottomStates, ddInformation.sourceVariables, ddInformation.successorVariables, ddInformation.predicateDdVariables, {ddInformation.commandDdVariable}, usedPlayer2Variables, allNondeterminismVariables, ddInformation.updateDdVariable, ddInformation.expressionToBddMap)); } template diff --git a/src/storage/prism/menu_games/AbstractProgram.h b/src/storage/prism/menu_games/AbstractProgram.h index 807d5f17e..996963ee0 100644 --- a/src/storage/prism/menu_games/AbstractProgram.h +++ b/src/storage/prism/menu_games/AbstractProgram.h @@ -104,6 +104,12 @@ namespace storm { // A state-set abstractor used to determine the initial states of the abstraction. StateSetAbstractor initialStateAbstractor; + // A flag that stores whether all guards were added (which is relevant for determining the bottom states). + bool addedAllGuards; + + // A state-set abstractor used to determine the bottom states if not all guards were added. + StateSetAbstractor bottomStateAbstractor; + // An ADD characterizing the probabilities of commands and their updates. storm::dd::Add commandUpdateProbabilitiesAdd; diff --git a/src/storage/prism/menu_games/MenuGame.cpp b/src/storage/prism/menu_games/MenuGame.cpp index 22f25e251..fb9269c5a 100644 --- a/src/storage/prism/menu_games/MenuGame.cpp +++ b/src/storage/prism/menu_games/MenuGame.cpp @@ -17,6 +17,7 @@ namespace storm { storm::dd::Bdd reachableStates, storm::dd::Bdd initialStates, storm::dd::Add transitionMatrix, + storm::dd::Bdd bottomStates, std::set const& rowVariables, std::set const& columnVariables, std::vector> const& rowColumnMetaVariablePairs, @@ -24,7 +25,7 @@ namespace storm { std::set const& player2Variables, std::set const& allNondeterminismVariables, storm::expressions::Variable const& updateVariable, - std::map> const& expressionToBddMap) : storm::models::symbolic::StochasticTwoPlayerGame(manager, reachableStates, initialStates, transitionMatrix.sumAbstract({updateVariable}), rowVariables, nullptr, columnVariables, nullptr, rowColumnMetaVariablePairs, player1Variables, player2Variables, allNondeterminismVariables), updateVariable(updateVariable), expressionToBddMap(expressionToBddMap) { + std::map> const& expressionToBddMap) : storm::models::symbolic::StochasticTwoPlayerGame(manager, reachableStates, initialStates, transitionMatrix.sumAbstract({updateVariable}), rowVariables, nullptr, columnVariables, nullptr, rowColumnMetaVariablePairs, player1Variables, player2Variables, allNondeterminismVariables), updateVariable(updateVariable), expressionToBddMap(expressionToBddMap), bottomStates(bottomStates) { // Intentionally left empty. } @@ -49,6 +50,11 @@ namespace storm { } } + template + storm::dd::Bdd MenuGame::getBottomStates() const { + return bottomStates; + } + template bool MenuGame::hasLabel(std::string const& label) const { return false; diff --git a/src/storage/prism/menu_games/MenuGame.h b/src/storage/prism/menu_games/MenuGame.h index 854dbe5f6..44d3c6e25 100644 --- a/src/storage/prism/menu_games/MenuGame.h +++ b/src/storage/prism/menu_games/MenuGame.h @@ -31,9 +31,10 @@ namespace storm { * Constructs a model from the given data. * * @param manager The manager responsible for the decision diagrams. - * @param reachableStates A DD representing the reachable states. - * @param initialStates A DD representing the initial states of the model. + * @param reachableStates The reachable states of the model. + * @param initialStates The initial states of the model. * @param transitionMatrix The matrix representing the transitions in the model. + * @param bottomStates The bottom states of the model. * @param rowVariables The set of row meta variables used in the DDs. * @param columVariables The set of column meta variables used in the DDs. * @param rowColumnMetaVariablePairs All pairs of row/column meta variables. @@ -48,6 +49,7 @@ namespace storm { storm::dd::Bdd reachableStates, storm::dd::Bdd initialStates, storm::dd::Add transitionMatrix, + storm::dd::Bdd bottomStates, std::set const& rowVariables, std::set const& columnVariables, std::vector> const& rowColumnMetaVariablePairs, @@ -78,6 +80,13 @@ namespace storm { */ storm::dd::Bdd getStates(storm::expressions::Expression const& expression, bool negated) const; + /*! + * Retrieves the bottom states of the model. + * + * @return The bottom states of the model. + */ + storm::dd::Bdd getBottomStates() const; + virtual bool hasLabel(std::string const& label) const override; private: @@ -86,6 +95,9 @@ namespace storm { // A mapping from expressions that were used in the abstraction process to the the BDDs representing them. std::map> expressionToBddMap; + + // The bottom states of the model. + storm::dd::Bdd bottomStates; }; } // namespace menu_games diff --git a/src/storage/prism/menu_games/StateSetAbstractor.cpp b/src/storage/prism/menu_games/StateSetAbstractor.cpp index da5219043..a1f7d8175 100644 --- a/src/storage/prism/menu_games/StateSetAbstractor.cpp +++ b/src/storage/prism/menu_games/StateSetAbstractor.cpp @@ -13,7 +13,7 @@ namespace storm { namespace menu_games { template - StateSetAbstractor::StateSetAbstractor(AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(expressionInformation.manager)), expressionInformation(expressionInformation), ddInformation(ddInformation), variablePartition(expressionInformation.variables), relevantPredicatesAndVariables(), concretePredicateVariables(), cachedBdd(ddInformation.manager->getBddZero()) { + StateSetAbstractor::StateSetAbstractor(AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(expressionInformation.manager)), expressionInformation(expressionInformation), ddInformation(ddInformation), variablePartition(expressionInformation.variables), relevantPredicatesAndVariables(), concretePredicateVariables(), needsRecomputation(false), cachedBdd(ddInformation.manager->getBddZero()) { // Assert all range expressions to enforce legal variable values. for (auto const& rangeExpression : expressionInformation.rangeExpressions) { @@ -36,9 +36,9 @@ namespace storm { std::set usedVariables = predicate.getVariables(); concretePredicateVariables.insert(usedVariables.begin(), usedVariables.end()); variablePartition.relate(usedVariables); - - // Since the new predicate might have changed the abstractions, we need to recompute it. - this->refine(); + + // Remember that we have to recompute the BDD. + this->needsRecomputation = true; } template @@ -82,11 +82,14 @@ namespace storm { template storm::dd::Bdd StateSetAbstractor::getStateBdd(storm::solver::SmtSolver::ModelReference const& model) const { STORM_LOG_TRACE("Building source state BDD."); + std::cout << "new model: " << std::endl; storm::dd::Bdd result = ddInformation.manager->getBddOne(); for (auto const& variableIndexPair : relevantPredicatesAndVariables) { if (model.getBooleanValue(variableIndexPair.first)) { + std::cout << expressionInformation.predicates[variableIndexPair.second] << " is true" << std::endl; result &= ddInformation.predicateBdds[variableIndexPair.second].first; } else { + std::cout << expressionInformation.predicates[variableIndexPair.second] << " is false" << std::endl; result &= !ddInformation.predicateBdds[variableIndexPair.second].first; } } @@ -98,13 +101,17 @@ namespace storm { STORM_LOG_TRACE("Recomputing BDD for state set abstraction."); storm::dd::Bdd result = ddInformation.manager->getBddZero(); - smtSolver->allSat(decisionVariables, [&result,this] (storm::solver::SmtSolver::ModelReference const& model) { result |= getStateBdd(model); return true; } ); + uint_fast64_t modelCounter = 0; + smtSolver->allSat(decisionVariables, [&result,this,&modelCounter] (storm::solver::SmtSolver::ModelReference const& model) { result |= getStateBdd(model); ++modelCounter; std::cout << "found " << modelCounter << " models" << std::endl; return modelCounter < 10000 ? true : false; } ); cachedBdd = result; } template - storm::dd::Bdd StateSetAbstractor::getAbstractStates() const { + storm::dd::Bdd StateSetAbstractor::getAbstractStates() { + if (needsRecomputation) { + this->refine(); + } return cachedBdd; } diff --git a/src/storage/prism/menu_games/StateSetAbstractor.h b/src/storage/prism/menu_games/StateSetAbstractor.h index 7e5b17178..b6703022d 100644 --- a/src/storage/prism/menu_games/StateSetAbstractor.h +++ b/src/storage/prism/menu_games/StateSetAbstractor.h @@ -62,7 +62,7 @@ namespace storm { * * @return The set of matching abstract states in the form of a BDD */ - storm::dd::Bdd getAbstractStates() const; + storm::dd::Bdd getAbstractStates(); private: /*! @@ -106,6 +106,9 @@ namespace storm { // The set of all decision variables over which to perform the all-sat enumeration. std::vector decisionVariables; + // A flag indicating whether the cached BDD needs recomputation. + bool needsRecomputation; + // The cached BDD representing the abstraction. This variable is written to in refinement steps (if work // needed to be done). storm::dd::Bdd cachedBdd;