From 3125ad4c89af70816dfb70352381fe987e8d3520 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 16 Dec 2016 22:01:20 +0100 Subject: [PATCH] more work on boolean transient variables in JANI menu game abstraction (labels) --- .../abstraction/AbstractionInformation.cpp | 21 ++++++++++++------- .../abstraction/AbstractionInformation.h | 12 ++++++++++- .../abstraction/ExpressionTranslator.cpp | 6 +++--- src/storm/abstraction/MenuGameAbstractor.h | 2 +- src/storm/abstraction/MenuGameRefiner.cpp | 2 +- src/storm/abstraction/MenuGameRefiner.h | 2 +- .../jani/JaniMenuGameAbstractor.cpp | 9 ++++---- .../abstraction/jani/JaniMenuGameAbstractor.h | 9 +------- .../prism/PrismMenuGameAbstractor.cpp | 7 ++++--- .../prism/PrismMenuGameAbstractor.h | 9 +------- .../abstraction/GameBasedMdpModelChecker.cpp | 10 ++++++--- 11 files changed, 49 insertions(+), 40 deletions(-) diff --git a/src/storm/abstraction/AbstractionInformation.cpp b/src/storm/abstraction/AbstractionInformation.cpp index ff28089b2..804a8ee33 100644 --- a/src/storm/abstraction/AbstractionInformation.cpp +++ b/src/storm/abstraction/AbstractionInformation.cpp @@ -14,7 +14,7 @@ namespace storm { namespace abstraction { template - AbstractionInformation::AbstractionInformation(storm::expressions::ExpressionManager& expressionManager, std::set const& abstractedVariables, std::unique_ptr&& smtSolver, std::shared_ptr> ddManager) : expressionManager(expressionManager), equivalenceChecker(std::move(smtSolver)), abstractedVariables(abstractedVariables), ddManager(ddManager), allPredicateIdentities(ddManager->getBddOne()), expressionToBddMap() { + AbstractionInformation::AbstractionInformation(storm::expressions::ExpressionManager& expressionManager, std::set const& abstractedVariables, std::unique_ptr&& smtSolver, std::shared_ptr> ddManager) : expressionManager(expressionManager), equivalenceChecker(std::move(smtSolver)), abstractedVariables(abstractedVariables), ddManager(ddManager), allPredicateIdentities(ddManager->getBddOne()), allLocationIdentities(ddManager->getBddOne()), expressionToBddMap() { // Intentionally left empty. } @@ -292,6 +292,10 @@ namespace storm { storm::dd::Bdd const& AbstractionInformation::getAllPredicateIdentities() const { return allPredicateIdentities; } + template + storm::dd::Bdd const& AbstractionInformation::getAllLocationIdentities() const { + return allLocationIdentities; + } template std::size_t AbstractionInformation::getPlayer1VariableCount() const { @@ -483,12 +487,15 @@ namespace storm { template std::pair, uint64_t> AbstractionInformation::addLocationVariables(uint64_t highestLocationIndex) { - locationVariablePairs.emplace_back(ddManager->addMetaVariable("loc_" + std::to_string(locationVariablePairs.size()), 0, highestLocationIndex)); - allSourceLocationVariables.insert(locationVariablePairs.back().first); - sourceVariables.insert(locationVariablePairs.back().first); - allSuccessorLocationVariables.insert(locationVariablePairs.back().second); - successorVariables.insert(locationVariablePairs.back().second); - extendedPredicateDdVariables.emplace_back(locationVariablePairs.back()); + auto newMetaVariable = ddManager->addMetaVariable("loc_" + std::to_string(locationVariablePairs.size()), 0, highestLocationIndex); + + locationVariablePairs.emplace_back(newMetaVariable); + allSourceLocationVariables.insert(newMetaVariable.first); + sourceVariables.insert(newMetaVariable.first); + allSuccessorLocationVariables.insert(newMetaVariable.second); + successorVariables.insert(newMetaVariable.second); + extendedPredicateDdVariables.emplace_back(newMetaVariable); + allLocationIdentities &= ddManager->template getIdentity(newMetaVariable.first).equals(ddManager->template getIdentity(newMetaVariable.second)) && ddManager->getRange(newMetaVariable.first) && ddManager->getRange(newMetaVariable.second); return std::make_pair(locationVariablePairs.back(), locationVariablePairs.size() - 1); } diff --git a/src/storm/abstraction/AbstractionInformation.h b/src/storm/abstraction/AbstractionInformation.h index 4a2276e6b..46b6804ee 100644 --- a/src/storm/abstraction/AbstractionInformation.h +++ b/src/storm/abstraction/AbstractionInformation.h @@ -348,6 +348,13 @@ namespace storm { */ storm::dd::Bdd const& getAllPredicateIdentities() const; + /*! + * Retrieves a BDD representing the identities of all location variables. + * + * @return All location identities. + */ + storm::dd::Bdd const& getAllLocationIdentities() const; + /*! * Retrieves a mapping of the known predicates to the BDDs that represent the corresponding states. * @@ -558,7 +565,10 @@ namespace storm { /// A BDD that represents the identity of all predicate variables. storm::dd::Bdd allPredicateIdentities; - + + /// A BDD that represents the identity of all location variables. + storm::dd::Bdd allLocationIdentities; + /// A meta variable pair that marks bottom states. std::pair bottomStateVariables; diff --git a/src/storm/abstraction/ExpressionTranslator.cpp b/src/storm/abstraction/ExpressionTranslator.cpp index adc6525c1..a60ab3c12 100644 --- a/src/storm/abstraction/ExpressionTranslator.cpp +++ b/src/storm/abstraction/ExpressionTranslator.cpp @@ -58,7 +58,7 @@ namespace storm { } storm::dd::Bdd left = boost::any_cast>(expression.getFirstOperand()->accept(*this, boost::none)); - storm::dd::Bdd right = boost::any_cast>(expression.getFirstOperand()->accept(*this, boost::none)); + storm::dd::Bdd right = boost::any_cast>(expression.getSecondOperand()->accept(*this, boost::none)); switch (expression.getOperatorType()) { case BinaryBooleanFunctionExpression::OperatorType::And: return left && right; case BinaryBooleanFunctionExpression::OperatorType::Or: return left || right; @@ -93,7 +93,7 @@ namespace storm { if (hasLocationVariables) { storm::dd::Add left = boost::any_cast>(expression.getFirstOperand()->accept(*this, boost::none)); - storm::dd::Add right = boost::any_cast>(expression.getFirstOperand()->accept(*this, boost::none)); + storm::dd::Add right = boost::any_cast>(expression.getSecondOperand()->accept(*this, boost::none)); switch (expression.getRelationType()) { case BinaryRelationExpression::RelationType::Equal: return left.equals(right); @@ -180,7 +180,7 @@ namespace storm { template boost::any ExpressionTranslator::visit(IntegerLiteralExpression const& expression, boost::any const& data) { - return abstractionInformation.get().getDdManager().template getConstant(expression.getValue()); + return abstractionInformation.get().getDdManager().template getConstant(expression.getValue()); } template diff --git a/src/storm/abstraction/MenuGameAbstractor.h b/src/storm/abstraction/MenuGameAbstractor.h index cec5818b0..099d27440 100644 --- a/src/storm/abstraction/MenuGameAbstractor.h +++ b/src/storm/abstraction/MenuGameAbstractor.h @@ -38,7 +38,7 @@ namespace storm { * Retrieves a BDD that characterizes the states corresponding to the given expression. For this to work, * appropriate predicates must have been used to refine the abstraction, otherwise this will fail. */ - virtual storm::dd::Bdd getStates(storm::expressions::Expression const& expression) const = 0; + virtual storm::dd::Bdd getStates(storm::expressions::Expression const& expression) = 0; /// Methods to refine the abstraction. virtual void refine(RefinementCommand const& command) = 0; diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index 8523dc913..9531d2e04 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -74,7 +74,7 @@ namespace storm { template void MenuGameRefiner::refine(std::vector const& predicates) const { - performRefinement(createGlobalRefinement(predicates)); + performRefinement(createGlobalRefinement(preprocessPredicates(predicates, RefinementPredicates::Source::Manual))); } template diff --git a/src/storm/abstraction/MenuGameRefiner.h b/src/storm/abstraction/MenuGameRefiner.h index 9334690ec..3250b97ab 100644 --- a/src/storm/abstraction/MenuGameRefiner.h +++ b/src/storm/abstraction/MenuGameRefiner.h @@ -32,7 +32,7 @@ namespace storm { class RefinementPredicates { public: enum class Source { - WeakestPrecondition, InitialGuard, Guard, Interpolation + WeakestPrecondition, InitialGuard, Guard, Interpolation, Manual }; RefinementPredicates() = default; diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp index e4a39ff8d..83a7181c8 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp @@ -2,6 +2,7 @@ #include "storm/abstraction/BottomStateResult.h" #include "storm/abstraction/GameBddResult.h" +#include "storm/abstraction/ExpressionTranslator.h" #include "storm/storage/BitVector.h" @@ -128,9 +129,9 @@ namespace storm { } template - storm::dd::Bdd JaniMenuGameAbstractor::getStates(storm::expressions::Expression const& predicate) const { - STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created."); - return abstractionInformation.getPredicateSourceVariable(predicate); + storm::dd::Bdd JaniMenuGameAbstractor::getStates(storm::expressions::Expression const& expression) { + storm::abstraction::ExpressionTranslator translator(abstractionInformation, smtSolverFactory->create(abstractionInformation.getExpressionManager())); + return translator.translate(expression); } template @@ -161,7 +162,7 @@ namespace storm { // If there are deadlock states, we fix them now. storm::dd::Add deadlockTransitions = abstractionInformation.getDdManager().template getAddZero(); if (!deadlockStates.isZero()) { - deadlockTransitions = (deadlockStates && abstractionInformation.getAllPredicateIdentities() && abstractionInformation.encodePlayer1Choice(0, abstractionInformation.getPlayer1VariableCount()) && abstractionInformation.encodePlayer2Choice(0, 0, game.numberOfPlayer2Variables) && abstractionInformation.encodeAux(0, 0, abstractionInformation.getAuxVariableCount())).template toAdd(); + deadlockTransitions = (deadlockStates && abstractionInformation.getAllPredicateIdentities() && abstractionInformation.getAllLocationIdentities() && abstractionInformation.encodePlayer1Choice(0, abstractionInformation.getPlayer1VariableCount()) && abstractionInformation.encodePlayer2Choice(0, 0, game.numberOfPlayer2Variables) && abstractionInformation.encodeAux(0, 0, abstractionInformation.getAuxVariableCount())).template toAdd(); } // Compute bottom states and the appropriate transitions if necessary. diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.h b/src/storm/abstraction/jani/JaniMenuGameAbstractor.h index 335e61f60..445616c4a 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.h +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.h @@ -91,14 +91,7 @@ namespace storm { */ storm::expressions::Expression getInitialExpression() const override; - /*! - * Retrieves the set of states (represented by a BDD) satisfying the given predicate, assuming that it - * was either given as an initial predicate or used as a refining predicate later. - * - * @param predicate The predicate for which to retrieve the states. - * @return The BDD representing the set of states. - */ - storm::dd::Bdd getStates(storm::expressions::Expression const& predicate) const override; + storm::dd::Bdd getStates(storm::expressions::Expression const& expression) override; /*! * Performs the given refinement command. diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index 992f6fec8..c08b306f1 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -2,6 +2,7 @@ #include "storm/abstraction/BottomStateResult.h" #include "storm/abstraction/GameBddResult.h" +#include "storm/abstraction/ExpressionTranslator.h" #include "storm/storage/BitVector.h" @@ -129,9 +130,9 @@ namespace storm { } template - storm::dd::Bdd PrismMenuGameAbstractor::getStates(storm::expressions::Expression const& expression) const { - STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created."); - return abstractionInformation.getPredicateSourceVariable(expression); + storm::dd::Bdd PrismMenuGameAbstractor::getStates(storm::expressions::Expression const& expression) { + storm::abstraction::ExpressionTranslator translator(abstractionInformation, smtSolverFactory->create(abstractionInformation.getExpressionManager())); + return translator.translate(expression); } template diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h index cc4ad4e69..df5e740ca 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h @@ -91,14 +91,7 @@ namespace storm { */ storm::expressions::Expression getInitialExpression() const override; - /*! - * Retrieves the set of states (represented by a BDD) satisfying the given predicate, assuming that it - * was either given as an initial predicate or used as a refining predicate later. - * - * @param predicate The predicate for which to retrieve the states. - * @return The BDD representing the set of states. - */ - storm::dd::Bdd getStates(storm::expressions::Expression const& expression) const; + storm::dd::Bdd getStates(storm::expressions::Expression const& expression) override; /*! * Performs the given refinement command. diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index ee18dc9e0..a14030c2d 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -209,7 +209,7 @@ namespace storm { // Cut away all columns targeting non-maybe states. submatrix *= maybeStatesAdd.swapVariables(game.getRowColumnMetaVariablePairs()); - + // Cut the starting vector to the maybe states of this query. storm::dd::Add startVector; if (startInfo) { @@ -311,6 +311,10 @@ namespace storm { storm::abstraction::MenuGameRefiner refiner(*abstractor, smtSolverFactory->create(preprocessedModel.getManager())); refiner.refine(initialPredicates); + storm::dd::Bdd globalConstraintStates = abstractor->getStates(constraintExpression); + storm::dd::Bdd globalTargetStates = abstractor->getStates(targetStateExpression); + globalTargetStates.template toAdd().exportToDot("target.dot"); + // Enter the main-loop of abstraction refinement. boost::optional> previousQualitativeResult = boost::none; boost::optional> previousMinQuantitativeResult = boost::none; @@ -328,8 +332,8 @@ namespace storm { // (2) Prepare transition matrix BDD and target state BDD for later use. storm::dd::Bdd transitionMatrixBdd = game.getTransitionMatrix().toBdd(); storm::dd::Bdd initialStates = game.getInitialStates(); - storm::dd::Bdd constraintStates = game.getStates(constraintExpression); - storm::dd::Bdd targetStates = game.getStates(targetStateExpression); + storm::dd::Bdd constraintStates = globalConstraintStates && game.getReachableStates(); + storm::dd::Bdd targetStates = globalTargetStates && game.getReachableStates(); if (player1Direction == storm::OptimizationDirection::Minimize) { targetStates |= game.getBottomStates(); }