From 44de3793c93e468a2f5dcc5ef0514d307998d514 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 25 Nov 2016 17:00:19 +0100 Subject: [PATCH] started to pull the rest of the refinement logic into refiner class, not working (or compiling) yet --- .../abstraction/AbstractionInformation.cpp | 39 ++++ .../abstraction/AbstractionInformation.h | 5 + src/storm/abstraction/MenuGameAbstractor.h | 7 +- src/storm/abstraction/MenuGameRefiner.cpp | 153 ++++++++++++- src/storm/abstraction/MenuGameRefiner.h | 22 +- .../abstraction/prism/AbstractProgram.cpp | 201 ++---------------- src/storm/abstraction/prism/AbstractProgram.h | 36 +--- .../prism/PrismMenuGameAbstractor.cpp | 4 + .../prism/PrismMenuGameAbstractor.h | 2 + .../abstraction/GameBasedMdpModelChecker.cpp | 2 +- .../expressions/EquivalenceChecker.cpp | 6 +- .../storage/expressions/EquivalenceChecker.h | 4 +- 12 files changed, 258 insertions(+), 223 deletions(-) diff --git a/src/storm/abstraction/AbstractionInformation.cpp b/src/storm/abstraction/AbstractionInformation.cpp index 4da158bf7..b7e61712e 100644 --- a/src/storm/abstraction/AbstractionInformation.cpp +++ b/src/storm/abstraction/AbstractionInformation.cpp @@ -1,5 +1,7 @@ #include "storm/abstraction/AbstractionInformation.h" +#include "storm/storage/BitVector.h" + #include "storm/storage/dd/DdManager.h" #include "storm/utility/macros.h" @@ -394,6 +396,43 @@ namespace storm { return result; } + template + std::map AbstractionInformation::decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd const& choice) const { + std::map result; + + storm::dd::Add lowerChoiceAsAdd = choice.template toAdd(); + for (auto const& successorValuePair : lowerChoiceAsAdd) { + uint_fast64_t updateIndex = this->decodeAux(successorValuePair.first, 0, this->getAuxVariableCount()); + +#ifdef LOCAL_DEBUG + std::cout << "update idx: " << updateIndex << std::endl; +#endif + storm::storage::BitVector successor(this->getNumberOfPredicates()); + for (uint_fast64_t index = 0; index < this->getOrderedSuccessorVariables().size(); ++index) { + auto const& successorVariable = this->getOrderedSuccessorVariables()[index]; +#ifdef LOCAL_DEBUG + std::cout << successorVariable.getName() << " has value"; +#endif + if (successorValuePair.first.getBooleanValue(successorVariable)) { + successor.set(index); +#ifdef LOCAL_DEBUG + std::cout << " true"; +#endif + } else { +#ifdef LOCAL_DEBUG + std::cout << " false"; +#endif + } +#ifdef LOCAL_DEBUG + std::cout << std::endl; +#endif + } + + result[updateIndex] = successor; + } + return result; + } + template class AbstractionInformation; template class AbstractionInformation; } diff --git a/src/storm/abstraction/AbstractionInformation.h b/src/storm/abstraction/AbstractionInformation.h index 64265f202..0a4f0ef03 100644 --- a/src/storm/abstraction/AbstractionInformation.h +++ b/src/storm/abstraction/AbstractionInformation.h @@ -426,6 +426,11 @@ namespace storm { */ std::vector> declareNewVariables(std::vector> const& oldPredicates, std::set const& newPredicates) const; + /*! + * Decodes the choice in the form of a BDD over the source and + */ + std::map decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd const& choice) const; + private: /*! * Encodes the given index with the given number of variables from the given variables. diff --git a/src/storm/abstraction/MenuGameAbstractor.h b/src/storm/abstraction/MenuGameAbstractor.h index e8bc703bd..8fa79491b 100644 --- a/src/storm/abstraction/MenuGameAbstractor.h +++ b/src/storm/abstraction/MenuGameAbstractor.h @@ -11,12 +11,15 @@ namespace storm { class MenuGameAbstractor { public: /// Retrieves the abstraction. - virtual storm::abstraction::MenuGame abstract() = 0; + virtual MenuGame abstract() = 0; + + /// Retrieves information about the abstraction. + virtual AbstractionInformation const& getAbstractionInformation() const = 0; /// Methods to refine the abstraction. virtual void refine(std::vector const& predicates) = 0; virtual void refine(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) = 0; - + /// Exports a representation of the current abstraction state in the dot format. virtual void exportToDot(std::string const& filename, storm::dd::Bdd const& highlightStates, storm::dd::Bdd const& filter) const = 0; }; diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index af8f73e2c..c2d7cd07d 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -8,7 +8,7 @@ namespace storm { namespace abstraction { template - MenuGameRefiner::MenuGameRefiner(MenuGameAbstractor& abstractor) : abstractor(abstractor) { + MenuGameRefiner::MenuGameRefiner(MenuGameAbstractor& abstractor, std::unique_ptr&& smtSolver) : abstractor(abstractor), splitter(), equivalenceChecker(std::move(smtSolver)) { // Intentionally left empty. } @@ -47,6 +47,124 @@ namespace storm { return pivotState; } + template + void refine(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) { + AbstractionInformation const& abstractionInformation = abstractor.get().getAbstractionInformation(); + + // Decode the index of the command chosen by player 1. + storm::dd::Add player1ChoiceAsAdd = player1Choice.template toAdd(); + auto pl1It = player1ChoiceAsAdd.begin(); + uint_fast64_t commandIndex = abstractionInformation.decodePlayer1Choice((*pl1It).first, abstractionInformation.getPlayer1VariableCount()); +#ifdef LOCAL_DEBUG + std::cout << "command index " << commandIndex << std::endl; + std::cout << program.get() << std::endl; + + for (auto stateValue : pivotState.template toAdd()) { + std::stringstream stateName; + stateName << "\tpl1_"; + for (auto const& var : currentGame->getRowVariables()) { + std::cout << "var " << var.getName() << std::endl; + if (stateValue.first.getBooleanValue(var)) { + stateName << "1"; + } else { + stateName << "0"; + } + } + std::cout << "pivot is " << stateName.str() << std::endl; + } +#endif + storm::abstraction::prism::AbstractCommand& abstractCommand = modules.front().getCommands()[commandIndex]; + storm::prism::Command const& concreteCommand = abstractCommand.getConcreteCommand(); +#ifdef LOCAL_DEBUG + player1Choice.template toAdd().exportToDot("pl1choice_ref.dot"); + std::cout << concreteCommand << std::endl; + + (currentGame->getTransitionMatrix() * player1Choice.template toAdd()).exportToDot("cuttrans.dot"); +#endif + + // Check whether there are bottom states in the game and whether one of the choices actually picks the + // bottom state as the successor. + bool buttomStateSuccessor = false; + if (!currentGame->getBottomStates().isZero()) { + buttomStateSuccessor = !((abstractionInformation.getBottomStateBdd(false, false) && lowerChoice) || (abstractionInformation.getBottomStateBdd(false, false) && upperChoice)).isZero(); + } + + // If one of the choices picks the bottom state, the new predicate is based on the guard of the appropriate + // command (that is the player 1 choice). + if (buttomStateSuccessor) { + STORM_LOG_TRACE("One of the successors is a bottom state, taking a guard as a new predicate."); + abstractCommand.notifyGuardIsPredicate(); + storm::expressions::Expression newPredicate = concreteCommand.getGuardExpression(); + STORM_LOG_DEBUG("Derived new predicate: " << newPredicate); + this->refine({std::make_pair(newPredicate, true)}); + } else { + STORM_LOG_TRACE("No bottom state successor. Deriving a new predicate using weakest precondition."); + +#ifdef LOCAL_DEBUG + lowerChoice.template toAdd().exportToDot("lowerchoice_ref.dot"); + upperChoice.template toAdd().exportToDot("upperchoice_ref.dot"); +#endif + + // Decode both choices to explicit mappings. +#ifdef LOCAL_DEBUG + std::cout << "lower" << std::endl; +#endif + std::map lowerChoiceUpdateToSuccessorMapping = decodeChoiceToUpdateSuccessorMapping(lowerChoice); +#ifdef LOCAL_DEBUG + std::cout << "upper" << std::endl; +#endif + std::map upperChoiceUpdateToSuccessorMapping = decodeChoiceToUpdateSuccessorMapping(upperChoice); + STORM_LOG_ASSERT(lowerChoiceUpdateToSuccessorMapping.size() == upperChoiceUpdateToSuccessorMapping.size(), "Mismatching sizes after decode (" << lowerChoiceUpdateToSuccessorMapping.size() << " vs. " << upperChoiceUpdateToSuccessorMapping.size() << ")."); + +#ifdef LOCAL_DEBUG + std::cout << "lower" << std::endl; + for (auto const& entry : lowerChoiceUpdateToSuccessorMapping) { + std::cout << entry.first << " -> " << entry.second << std::endl; + } + std::cout << "upper" << std::endl; + for (auto const& entry : upperChoiceUpdateToSuccessorMapping) { + std::cout << entry.first << " -> " << entry.second << std::endl; + } +#endif + + // Now go through the mappings and find points of deviation. Currently, we take the first deviation. + storm::expressions::Expression newPredicate; + auto lowerIt = lowerChoiceUpdateToSuccessorMapping.begin(); + auto lowerIte = lowerChoiceUpdateToSuccessorMapping.end(); + auto upperIt = upperChoiceUpdateToSuccessorMapping.begin(); + for (; lowerIt != lowerIte; ++lowerIt, ++upperIt) { + STORM_LOG_ASSERT(lowerIt->first == upperIt->first, "Update indices mismatch."); + uint_fast64_t updateIndex = lowerIt->first; +#ifdef LOCAL_DEBUG + std::cout << "update idx " << updateIndex << std::endl; +#endif + bool deviates = lowerIt->second != upperIt->second; + if (deviates) { + for (uint_fast64_t predicateIndex = 0; predicateIndex < lowerIt->second.size(); ++predicateIndex) { + if (lowerIt->second.get(predicateIndex) != upperIt->second.get(predicateIndex)) { + // Now we know the point of the deviation (command, update, predicate). + std::cout << "ref" << std::endl; + std::cout << abstractionInformation.getPredicateByIndex(predicateIndex) << std::endl; + std::cout << concreteCommand.getUpdate(updateIndex) << std::endl; + newPredicate = abstractionInformation.getPredicateByIndex(predicateIndex).substitute(concreteCommand.getUpdate(updateIndex).getAsVariableToExpressionMap()).simplify(); + break; + } + } + } + } + STORM_LOG_ASSERT(newPredicate.isInitialized(), "Could not derive new predicate as there is no deviation."); + + STORM_LOG_DEBUG("Derived new predicate: " << newPredicate); + + this->refine({std::make_pair(newPredicate, true)}); + } + + STORM_LOG_TRACE("Current set of predicates:"); + for (auto const& predicate : abstractionInformation.getPredicates()) { + STORM_LOG_TRACE(predicate); + } + } + template bool MenuGameRefiner::refine(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, QualitativeResultMinMax const& qualitativeResult) { STORM_LOG_TRACE("Trying refinement after qualitative check."); @@ -202,6 +320,39 @@ namespace storm { } + template + bool MenuGameRefiner::performRefinement(std::vector const& predicates) const { + for (auto const& predicate : predicates) { + storm::expressions::Expression const& predicate = predicateAllowSplitPair.first; + bool allowSplit = predicateAllowSplitPair.second; + STORM_LOG_THROW(predicate.hasBooleanType(), storm::exceptions::InvalidArgumentException, "Expecting a predicate of type bool."); + + if (allowSplit && splitPredicates) { + // Split the predicates. + std::vector atoms = splitter.split(predicate); + + // Check which of the atoms are redundant in the sense that they are equivalent to a predicate we already have. + for (auto const& atom : atoms) { + bool addAtom = true; + for (auto const& oldPredicate : abstractionInformation.getPredicates()) { + if (equivalenceChecker.areEquivalent(atom, oldPredicate)) { + addAtom = false; + break; + } + } + + if (addAtom) { + uint_fast64_t newPredicateIndex = abstractionInformation.addPredicate(atom); + newPredicateIndices.push_back(newPredicateIndex); + } + } + } else { + uint_fast64_t newPredicateIndex = abstractionInformation.addPredicate(predicate); + newPredicateIndices.push_back(newPredicateIndex); + } + } + } + template class MenuGameRefiner; template class MenuGameRefiner; diff --git a/src/storm/abstraction/MenuGameRefiner.h b/src/storm/abstraction/MenuGameRefiner.h index 03b12b710..32e16e5e7 100644 --- a/src/storm/abstraction/MenuGameRefiner.h +++ b/src/storm/abstraction/MenuGameRefiner.h @@ -2,14 +2,19 @@ #include #include +#include #include "storm/abstraction/QualitativeResultMinMax.h" #include "storm/abstraction/QuantitativeResultMinMax.h" #include "storm/storage/expressions/Expression.h" +#include "storm/storage/expressions/PredicateSplitter.h" +#include "storm/storage/expressions/EquivalenceChecker.h" #include "storm/storage/dd/DdType.h" +#include "storm/utility/solver.h" + namespace storm { namespace abstraction { @@ -25,7 +30,7 @@ namespace storm { /*! * Creates a refiner for the provided abstractor. */ - MenuGameRefiner(MenuGameAbstractor& abstractor); + MenuGameRefiner(MenuGameAbstractor& abstractor, std::unique_ptr&& smtSolver); /*! * Refines the abstractor with the given set of predicates. @@ -37,18 +42,29 @@ namespace storm { * * @param True if predicates for refinement could be derived, false otherwise. */ - bool refine(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, QualitativeResultMinMax const& qualitativeResult); + bool refine(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, QualitativeResultMinMax const& qualitativeResult) const; /*! * Refines the abstractor based on the quantitative result by trying to derive suitable predicates. * * @param True if predicates for refinement could be derived, false otherwise. */ - bool refine(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, QuantitativeResultMinMax const& quantitativeResult); + bool refine(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, QuantitativeResultMinMax const& quantitativeResult) const; private: + /*! + * Takes the given predicates, preprocesses them and then refines the abstractor. + */ + bool performRefinement(std::vector const& predicates) const; + /// The underlying abstractor to refine. std::reference_wrapper> abstractor; + + /// An object that can be used for splitting predicates. + storm::expressions::PredicateSplitter splitter; + + /// An object that can be used to determine whether predicates are equivalent. + storm::expressions::EquivalenceChecker equivalenceChecker; }; } diff --git a/src/storm/abstraction/prism/AbstractProgram.cpp b/src/storm/abstraction/prism/AbstractProgram.cpp index c6738a740..da7ae8f56 100644 --- a/src/storm/abstraction/prism/AbstractProgram.cpp +++ b/src/storm/abstraction/prism/AbstractProgram.cpp @@ -30,8 +30,8 @@ namespace storm { template AbstractProgram::AbstractProgram(storm::prism::Program const& program, std::shared_ptr const& smtSolverFactory, - bool addAllGuards, bool splitPredicates) - : program(program), smtSolverFactory(smtSolverFactory), abstractionInformation(program.getManager()), modules(), initialStateAbstractor(abstractionInformation, program.getAllExpressionVariables(), {program.getInitialStatesExpression()}, this->smtSolverFactory), splitPredicates(splitPredicates), splitter(), equivalenceChecker(smtSolverFactory->create(abstractionInformation.getExpressionManager()), abstractionInformation.getExpressionManager().boolean(true)), addedAllGuards(addAllGuards), currentGame(nullptr) { + bool addAllGuards) + : program(program), smtSolverFactory(smtSolverFactory), abstractionInformation(program.getManager()), modules(), initialStateAbstractor(abstractionInformation, program.getAllExpressionVariables(), {program.getInitialStatesExpression()}, this->smtSolverFactory), addedAllGuards(addAllGuards), 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. @@ -75,10 +75,10 @@ namespace storm { commandUpdateProbabilitiesAdd = modules.front().getCommandUpdateProbabilitiesAdd(); // Now that we have created all other DD variables, we create the DD variables for the predicates. - std::vector> initialPredicates; + std::vector initialPredicates; if (addAllGuards) { for (auto const& guard : allGuards) { - initialPredicates.push_back(std::make_pair(guard, true)); + initialPredicates.push_back(guard); } } @@ -87,37 +87,12 @@ namespace storm { } template - void AbstractProgram::refine(std::vector> const& predicates) { - // Add the predicates to the global list of predicates. + void AbstractProgram::refine(std::vector const& predicates) { + // Add the predicates to the global list of predicates and gather their indices. std::vector newPredicateIndices; - for (auto const& predicateAllowSplitPair : predicates) { - storm::expressions::Expression const& predicate = predicateAllowSplitPair.first; - bool allowSplit = predicateAllowSplitPair.second; + for (auto const& predicate : predicates) { STORM_LOG_THROW(predicate.hasBooleanType(), storm::exceptions::InvalidArgumentException, "Expecting a predicate of type bool."); - - if (allowSplit && splitPredicates) { - // Split the predicates. - std::vector atoms = splitter.split(predicate); - - // Check which of the atoms are redundant in the sense that they are equivalent to a predicate we already have. - for (auto const& atom : atoms) { - bool addAtom = true; - for (auto const& oldPredicate : abstractionInformation.getPredicates()) { - if (equivalenceChecker.areEquivalent(atom, oldPredicate)) { - addAtom = false; - break; - } - } - - if (addAtom) { - uint_fast64_t newPredicateIndex = abstractionInformation.addPredicate(atom); - newPredicateIndices.push_back(newPredicateIndex); - } - } - } else { - uint_fast64_t newPredicateIndex = abstractionInformation.addPredicate(predicate); - newPredicateIndices.push_back(newPredicateIndex); - } + newPredicateIndices.push_back(abstractionInformation.addPredicate(predicate)); } // Refine all abstract modules. @@ -131,166 +106,18 @@ namespace storm { // Finally, we rebuild the game. currentGame = buildGame(); } - - template - std::map AbstractProgram::decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd const& choice) const { - std::map result; - - storm::dd::Add lowerChoiceAsAdd = choice.template toAdd(); - for (auto const& successorValuePair : lowerChoiceAsAdd) { - uint_fast64_t updateIndex = abstractionInformation.decodeAux(successorValuePair.first, 0, currentGame->getProbabilisticBranchingVariables().size()); - -#ifdef LOCAL_DEBUG - std::cout << "update idx: " << updateIndex << std::endl; -#endif - storm::storage::BitVector successor(abstractionInformation.getNumberOfPredicates()); - for (uint_fast64_t index = 0; index < abstractionInformation.getOrderedSuccessorVariables().size(); ++index) { - auto const& successorVariable = abstractionInformation.getOrderedSuccessorVariables()[index]; -#ifdef LOCAL_DEBUG - std::cout << successorVariable.getName() << " has value"; -#endif - if (successorValuePair.first.getBooleanValue(successorVariable)) { - successor.set(index); -#ifdef LOCAL_DEBUG - std::cout << " true"; -#endif - } else { -#ifdef LOCAL_DEBUG - std::cout << " false"; -#endif - } -#ifdef LOCAL_DEBUG - std::cout << std::endl; -#endif - } - - result[updateIndex] = successor; - } - return result; - } - - template - void AbstractProgram::refine(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) { - // Decode the index of the command chosen by player 1. - storm::dd::Add player1ChoiceAsAdd = player1Choice.template toAdd(); - auto pl1It = player1ChoiceAsAdd.begin(); - uint_fast64_t commandIndex = abstractionInformation.decodePlayer1Choice((*pl1It).first, abstractionInformation.getPlayer1VariableCount()); -#ifdef LOCAL_DEBUG - std::cout << "command index " << commandIndex << std::endl; - std::cout << program.get() << std::endl; - - for (auto stateValue : pivotState.template toAdd()) { - std::stringstream stateName; - stateName << "\tpl1_"; - for (auto const& var : currentGame->getRowVariables()) { - std::cout << "var " << var.getName() << std::endl; - if (stateValue.first.getBooleanValue(var)) { - stateName << "1"; - } else { - stateName << "0"; - } - } - std::cout << "pivot is " << stateName.str() << std::endl; - } -#endif - storm::abstraction::prism::AbstractCommand& abstractCommand = modules.front().getCommands()[commandIndex]; - storm::prism::Command const& concreteCommand = abstractCommand.getConcreteCommand(); -#ifdef LOCAL_DEBUG - player1Choice.template toAdd().exportToDot("pl1choice_ref.dot"); - std::cout << concreteCommand << std::endl; - - (currentGame->getTransitionMatrix() * player1Choice.template toAdd()).exportToDot("cuttrans.dot"); -#endif - - // Check whether there are bottom states in the game and whether one of the choices actually picks the - // bottom state as the successor. - bool buttomStateSuccessor = false; - if (!currentGame->getBottomStates().isZero()) { - buttomStateSuccessor = !((abstractionInformation.getBottomStateBdd(false, false) && lowerChoice) || (abstractionInformation.getBottomStateBdd(false, false) && upperChoice)).isZero(); - } - - // If one of the choices picks the bottom state, the new predicate is based on the guard of the appropriate - // command (that is the player 1 choice). - if (buttomStateSuccessor) { - STORM_LOG_TRACE("One of the successors is a bottom state, taking a guard as a new predicate."); - abstractCommand.notifyGuardIsPredicate(); - storm::expressions::Expression newPredicate = concreteCommand.getGuardExpression(); - STORM_LOG_DEBUG("Derived new predicate: " << newPredicate); - this->refine({std::make_pair(newPredicate, true)}); - } else { - STORM_LOG_TRACE("No bottom state successor. Deriving a new predicate using weakest precondition."); - -#ifdef LOCAL_DEBUG - lowerChoice.template toAdd().exportToDot("lowerchoice_ref.dot"); - upperChoice.template toAdd().exportToDot("upperchoice_ref.dot"); -#endif - - // Decode both choices to explicit mappings. -#ifdef LOCAL_DEBUG - std::cout << "lower" << std::endl; -#endif - std::map lowerChoiceUpdateToSuccessorMapping = decodeChoiceToUpdateSuccessorMapping(lowerChoice); -#ifdef LOCAL_DEBUG - std::cout << "upper" << std::endl; -#endif - std::map upperChoiceUpdateToSuccessorMapping = decodeChoiceToUpdateSuccessorMapping(upperChoice); - STORM_LOG_ASSERT(lowerChoiceUpdateToSuccessorMapping.size() == upperChoiceUpdateToSuccessorMapping.size(), "Mismatching sizes after decode (" << lowerChoiceUpdateToSuccessorMapping.size() << " vs. " << upperChoiceUpdateToSuccessorMapping.size() << ")."); - -#ifdef LOCAL_DEBUG - std::cout << "lower" << std::endl; - for (auto const& entry : lowerChoiceUpdateToSuccessorMapping) { - std::cout << entry.first << " -> " << entry.second << std::endl; - } - std::cout << "upper" << std::endl; - for (auto const& entry : upperChoiceUpdateToSuccessorMapping) { - std::cout << entry.first << " -> " << entry.second << std::endl; - } -#endif - - // Now go through the mappings and find points of deviation. Currently, we take the first deviation. - storm::expressions::Expression newPredicate; - auto lowerIt = lowerChoiceUpdateToSuccessorMapping.begin(); - auto lowerIte = lowerChoiceUpdateToSuccessorMapping.end(); - auto upperIt = upperChoiceUpdateToSuccessorMapping.begin(); - for (; lowerIt != lowerIte; ++lowerIt, ++upperIt) { - STORM_LOG_ASSERT(lowerIt->first == upperIt->first, "Update indices mismatch."); - uint_fast64_t updateIndex = lowerIt->first; -#ifdef LOCAL_DEBUG - std::cout << "update idx " << updateIndex << std::endl; -#endif - bool deviates = lowerIt->second != upperIt->second; - if (deviates) { - for (uint_fast64_t predicateIndex = 0; predicateIndex < lowerIt->second.size(); ++predicateIndex) { - if (lowerIt->second.get(predicateIndex) != upperIt->second.get(predicateIndex)) { - // Now we know the point of the deviation (command, update, predicate). - std::cout << "ref" << std::endl; - std::cout << abstractionInformation.getPredicateByIndex(predicateIndex) << std::endl; - std::cout << concreteCommand.getUpdate(updateIndex) << std::endl; - newPredicate = abstractionInformation.getPredicateByIndex(predicateIndex).substitute(concreteCommand.getUpdate(updateIndex).getAsVariableToExpressionMap()).simplify(); - break; - } - } - } - } - STORM_LOG_ASSERT(newPredicate.isInitialized(), "Could not derive new predicate as there is no deviation."); - - STORM_LOG_DEBUG("Derived new predicate: " << newPredicate); - - this->refine({std::make_pair(newPredicate, true)}); - } - - STORM_LOG_TRACE("Current set of predicates:"); - for (auto const& predicate : abstractionInformation.getPredicates()) { - STORM_LOG_TRACE(predicate); - } - } - + template MenuGame AbstractProgram::getAbstractGame() { STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created."); return *currentGame; } + template + AbstractionInformation const& AbstractProgram::getAbstractionInformation() const { + return abstractionInformation; + } + template storm::dd::Bdd AbstractProgram::getStates(storm::expressions::Expression const& predicate) { STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created."); diff --git a/src/storm/abstraction/prism/AbstractProgram.h b/src/storm/abstraction/prism/AbstractProgram.h index d20ca12e0..b30d1eb39 100644 --- a/src/storm/abstraction/prism/AbstractProgram.h +++ b/src/storm/abstraction/prism/AbstractProgram.h @@ -9,8 +9,6 @@ #include "storm/storage/dd/Add.h" #include "storm/storage/expressions/Expression.h" -#include "storm/storage/expressions/PredicateSplitter.h" -#include "storm/storage/expressions/EquivalenceChecker.h" namespace storm { namespace utility { @@ -44,9 +42,8 @@ namespace storm { * @param program The concrete program for which to build the abstraction. * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. * @param addAllGuards A flag that indicates whether all guards of the program should be added to the initial set of predicates. - * @param splitPredicates A flag that indicates whether the predicates are to be split into atoms before being added. */ - AbstractProgram(storm::prism::Program const& program, std::shared_ptr const& smtSolverFactory = std::make_shared(), bool addAllGuards = false, bool splitPredicates = false); + AbstractProgram(storm::prism::Program const& program, std::shared_ptr const& smtSolverFactory = std::make_shared(), bool addAllGuards = false); AbstractProgram(AbstractProgram const&) = default; AbstractProgram& operator=(AbstractProgram const&) = default; @@ -60,6 +57,13 @@ namespace storm { */ MenuGame getAbstractGame(); + /*! + * Retrieves information about the abstraction. + * + * @return The abstraction information object. + */ + AbstractionInformation const& getAbstractionInformation() const; + /*! * 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. @@ -74,18 +78,7 @@ namespace storm { * * @param predicates The new predicates. */ - void refine(std::vector> const& predicates); - - /*! - * Refines the abstract program using the pivot state, and player 1 choice. The refinement guarantees that - * the two provided choices are not possible from the same pivot state using the given player 1 choice. - * - * @param pivotState The pivot state on which to base the refinement. - * @param player1Choice The player 1 choice that needs to be refined. - * @param lowerChoice The first of the two choices on which to base the refinement. - * @param upperChoice The first of the two choices on which to base the refinement. - */ - void refine(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice); + void refine(std::vector const& predicates); /*! * Exports the current state of the abstraction in the dot format to the given file. @@ -126,16 +119,7 @@ namespace storm { // A state-set abstractor used to determine the initial states of the abstraction. StateSetAbstractor initialStateAbstractor; - - // A flag indicating whether predicates are to be split into atoms or not. - bool splitPredicates; - - // An object that can be used for splitting predicates. - storm::expressions::PredicateSplitter splitter; - - // An object that can be used to determine whether predicates are equivalent. - storm::expressions::EquivalenceChecker equivalenceChecker; - + // A flag that stores whether all guards were added (which is relevant for determining the bottom states). bool addedAllGuards; diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index 7c5a22861..d2ac18a63 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -19,6 +19,10 @@ namespace storm { return abstractProgram.getAbstractGame(); } + AbstractionInformation const& PrismMenuGameAbstractor::getAbstractionInformation() const { + return abstractProgram.getAbstractionInformation(); + } + template void PrismMenuGameAbstractor::refine(std::vector const& predicates) { std::vector> predicatesWithFlags; diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h index 84fd5ec36..ff59beb8a 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h @@ -14,6 +14,8 @@ namespace storm { PrismMenuGameAbstractor(storm::prism::Program const& program, std::shared_ptr const& smtSolverFactory = std::make_shared()); virtual storm::abstraction::MenuGame abstract() override; + virtual AbstractionInformation const& getAbstractionInformation() const override; + virtual void refine(std::vector const& predicates) override; virtual void refine(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) override; diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 88a067cac..5a7c31d97 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -275,7 +275,7 @@ namespace storm { storm::abstraction::prism::PrismMenuGameAbstractor abstractor(preprocessedModel.asPrismProgram(), smtSolverFactory); // Create a refiner that can be used to refine the abstraction when needed. - storm::abstraction::MenuGameRefiner refiner(abstractor); + storm::abstraction::MenuGameRefiner refiner(abstractor, smtSolverFactory->create(preprocessedModel.getManager())); refiner.refine(initialPredicates); // Enter the main-loop of abstraction refinement. diff --git a/src/storm/storage/expressions/EquivalenceChecker.cpp b/src/storm/storage/expressions/EquivalenceChecker.cpp index 31ee34894..b8d538656 100644 --- a/src/storm/storage/expressions/EquivalenceChecker.cpp +++ b/src/storm/storage/expressions/EquivalenceChecker.cpp @@ -7,8 +7,10 @@ namespace storm { namespace expressions { - EquivalenceChecker::EquivalenceChecker(std::unique_ptr&& smtSolver, storm::expressions::Expression const& constraint) : smtSolver(std::move(smtSolver)) { - this->smtSolver->add(constraint); + EquivalenceChecker::EquivalenceChecker(std::unique_ptr&& smtSolver, boost::optional const& constraint) : smtSolver(std::move(smtSolver)) { + if (constraint) { + this->smtSolver->add(constraint.get()); + } } bool EquivalenceChecker::areEquivalent(storm::expressions::Expression const& first, storm::expressions::Expression const& second) { diff --git a/src/storm/storage/expressions/EquivalenceChecker.h b/src/storm/storage/expressions/EquivalenceChecker.h index eba773014..2ec39ba8a 100644 --- a/src/storm/storage/expressions/EquivalenceChecker.h +++ b/src/storm/storage/expressions/EquivalenceChecker.h @@ -2,6 +2,8 @@ #include +#include + #include "storm/solver/SmtSolver.h" namespace storm { @@ -16,7 +18,7 @@ namespace storm { * @param smtSolver The solver to use. * @param constraint An additional constraint. Must be satisfiable. */ - EquivalenceChecker(std::unique_ptr&& smtSolver, storm::expressions::Expression const& constraint); + EquivalenceChecker(std::unique_ptr&& smtSolver, boost::optional const& constraint = boost::none); bool areEquivalent(storm::expressions::Expression const& first, storm::expressions::Expression const& second);