From 7a4d3740debedf921469b0eb4b9f3e8ac74da093 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 7 Aug 2016 22:24:27 +0200 Subject: [PATCH] some more work, not fully working again (yet) Former-commit-id: 32c8c6eb7eb68a436cd73787826038113ebdfeff --- src/abstraction/AbstractionInformation.cpp | 2 +- src/abstraction/StateSetAbstractor.cpp | 7 +------ src/abstraction/StateSetAbstractor.h | 5 ++--- src/abstraction/prism/AbstractModule.cpp | 16 +++++++++++++--- src/abstraction/prism/AbstractModule.h | 16 +++++++++++++++- src/abstraction/prism/AbstractProgram.cpp | 21 ++++++++++++--------- src/abstraction/prism/AbstractProgram.h | 6 ++++++ 7 files changed, 50 insertions(+), 23 deletions(-) diff --git a/src/abstraction/AbstractionInformation.cpp b/src/abstraction/AbstractionInformation.cpp index e83fb9330..7cb5f20d4 100644 --- a/src/abstraction/AbstractionInformation.cpp +++ b/src/abstraction/AbstractionInformation.cpp @@ -9,7 +9,7 @@ namespace storm { namespace abstraction { template - AbstractionInformation::AbstractionInformation(storm::expressions::ExpressionManager& expressionManager, std::shared_ptr> ddManager) : expressionManager(expressionManager), ddManager(ddManager) { + AbstractionInformation::AbstractionInformation(storm::expressions::ExpressionManager& expressionManager, std::shared_ptr> ddManager) : expressionManager(expressionManager), ddManager(ddManager), allPredicateIdentities(ddManager->getBddZero()) { // Intentionally left empty. } diff --git a/src/abstraction/StateSetAbstractor.cpp b/src/abstraction/StateSetAbstractor.cpp index 2c6b18259..313202662 100644 --- a/src/abstraction/StateSetAbstractor.cpp +++ b/src/abstraction/StateSetAbstractor.cpp @@ -11,12 +11,7 @@ namespace storm { namespace abstraction { template - StateSetAbstractor::StateSetAbstractor(AbstractionInformation& abstractionInformation) : smtSolver(nullptr), abstractionInformation(abstractionInformation), localExpressionInformation(), relevantPredicatesAndVariables(), concretePredicateVariables(), decisionVariables(), needsRecomputation(false), cachedBdd(), constraint() { - // Intentionally left empty. - } - - template - StateSetAbstractor::StateSetAbstractor(AbstractionInformation& abstractionInformation, std::vector const& statePredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), localExpressionInformation(abstractionInformation.getExpressionVariables()), relevantPredicatesAndVariables(), concretePredicateVariables(), needsRecomputation(false), cachedBdd(abstractionInformation.getDdManager().getBddZero()), constraint(abstractionInformation.getDdManager().getBddOne()) { + StateSetAbstractor::StateSetAbstractor(AbstractionInformation& abstractionInformation, std::set const& allVariables, std::vector const& statePredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), localExpressionInformation(allVariables), relevantPredicatesAndVariables(), concretePredicateVariables(), needsRecomputation(false), cachedBdd(abstractionInformation.getDdManager().getBddZero()), constraint(abstractionInformation.getDdManager().getBddOne()) { // Assert all constraints to enforce legal variable values. for (auto const& constraint : abstractionInformation.getConstraints()) { diff --git a/src/abstraction/StateSetAbstractor.h b/src/abstraction/StateSetAbstractor.h index bbb679009..c5348accd 100644 --- a/src/abstraction/StateSetAbstractor.h +++ b/src/abstraction/StateSetAbstractor.h @@ -34,8 +34,6 @@ namespace storm { template class StateSetAbstractor { public: - StateSetAbstractor(AbstractionInformation& abstractionInformation); - StateSetAbstractor(StateSetAbstractor const& other) = default; StateSetAbstractor& operator=(StateSetAbstractor const& other) = default; @@ -48,11 +46,12 @@ namespace storm { * Creates a state set abstractor. * * @param abstractionInformation An object storing information about the abstraction such as predicates and BDDs. + * @param allVariables All variables that appear in the predicates. * @param statePredicates A set of predicates that have to hold in the concrete states this abstractor is * supposed to abstract. * @param smtSolverFactory A factory that can create new SMT solvers. */ - StateSetAbstractor(AbstractionInformation& abstractionInformation, std::vector const& statePredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory); + StateSetAbstractor(AbstractionInformation& abstractionInformation, std::set const& allVariables, std::vector const& statePredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory); /*! * Refines the abstractor by making the given predicates new abstract predicates. diff --git a/src/abstraction/prism/AbstractModule.cpp b/src/abstraction/prism/AbstractModule.cpp index 1626371a5..7a396c517 100644 --- a/src/abstraction/prism/AbstractModule.cpp +++ b/src/abstraction/prism/AbstractModule.cpp @@ -27,6 +27,11 @@ namespace storm { } } + template + AbstractModule::~AbstractModule() { + std::cout << "destructing abs module at " << this << std::endl; + } + template std::pair, uint_fast64_t> AbstractModule::getAbstractBdd() { // First, we retrieve the abstractions of all commands. @@ -39,22 +44,27 @@ namespace storm { // Then, we build the module BDD by adding the single command DDs. We need to make sure that all command // DDs use the same amount DD variable encoding the choices of player 2. - storm::dd::Bdd result = abstractionInformation.getDdManager().getBddZero(); + storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddZero(); for (auto const& commandDd : commandDdsAndUsedOptionVariableCounts) { - result |= commandDd.first && abstractionInformation.getPlayer2ZeroCube(maximalNumberOfUsedOptionVariables, commandDd.second); + result |= commandDd.first && this->getAbstractionInformation().getPlayer2ZeroCube(maximalNumberOfUsedOptionVariables, commandDd.second); } return std::make_pair(result, maximalNumberOfUsedOptionVariables); } template storm::dd::Add AbstractModule::getCommandUpdateProbabilitiesAdd() const { - storm::dd::Add result = abstractionInformation.getDdManager().template getAddZero(); + storm::dd::Add result = this->getAbstractionInformation().getDdManager().template getAddZero(); for (auto const& command : commands) { result += command.getCommandUpdateProbabilitiesAdd(); } return result; } + template + AbstractionInformation const& AbstractModule::getAbstractionInformation() const { + return abstractionInformation.get(); + } + template class AbstractModule; template class AbstractModule; } diff --git a/src/abstraction/prism/AbstractModule.h b/src/abstraction/prism/AbstractModule.h index 3fdc5fd2b..77c267da1 100644 --- a/src/abstraction/prism/AbstractModule.h +++ b/src/abstraction/prism/AbstractModule.h @@ -31,6 +31,13 @@ namespace storm { */ AbstractModule(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory); + AbstractModule(AbstractModule const&) = delete; + AbstractModule& operator=(AbstractModule const&) = delete; + AbstractModule(AbstractModule&&) = default; + AbstractModule& operator=(AbstractModule&&) = default; + + ~AbstractModule(); + /*! * Refines the abstract module with the given predicates. * @@ -53,11 +60,18 @@ namespace storm { storm::dd::Add getCommandUpdateProbabilitiesAdd() const; private: + /*! + * Retrieves the abstraction information. + * + * @return The abstraction information. + */ + AbstractionInformation const& getAbstractionInformation() const; + // A factory that can be used to create new SMT solvers. storm::utility::solver::SmtSolverFactory const& smtSolverFactory; // The DD-related information. - AbstractionInformation const& abstractionInformation; + std::reference_wrapper const> abstractionInformation; // The abstract commands of the abstract module. std::vector> commands; diff --git a/src/abstraction/prism/AbstractProgram.cpp b/src/abstraction/prism/AbstractProgram.cpp index 54b7cdbc2..f8056ec72 100644 --- a/src/abstraction/prism/AbstractProgram.cpp +++ b/src/abstraction/prism/AbstractProgram.cpp @@ -16,12 +16,17 @@ namespace storm { namespace abstraction { namespace prism { + template + AbstractProgram::~AbstractProgram() { + std::cout << "destructing abs program" << std::endl; + } + template AbstractProgram::AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector const& initialPredicates, std::unique_ptr&& smtSolverFactory, bool addAllGuards) - : program(program), smtSolverFactory(std::move(smtSolverFactory)), modules(), abstractionInformation(expressionManager), initialStateAbstractor(), addedAllGuards(addAllGuards), bottomStateAbstractor(), currentGame(nullptr) { + : program(program), smtSolverFactory(std::move(smtSolverFactory)), modules(), abstractionInformation(expressionManager), initialStateAbstractor(abstractionInformation, program.getAllExpressionVariables(), {program.getInitialConstruct().getInitialStatesExpression()}, *this->smtSolverFactory), addedAllGuards(addAllGuards), bottomStateAbstractor(abstractionInformation, program.getAllExpressionVariables(), program.getAllGuards(true), *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. @@ -50,7 +55,7 @@ namespace storm { totalNumberOfCommands += module.getNumberOfCommands(); } - // NOTE: currently we assume that 100 player 2variables suffice, which corresponds to 2^100 possible + // NOTE: currently we assume that 100 player 2 variables suffice, which corresponds to 2^100 possible // choices. If for some reason this should not be enough, we could grow this vector dynamically, but // odds are that it's impossible to treat such models in any event. abstractionInformation.createEncodingVariables(static_cast(std::ceil(std::log2(totalNumberOfCommands))), 100, static_cast(std::ceil(std::log2(maximalUpdateCount)))); @@ -67,18 +72,16 @@ namespace storm { // For each module of the concrete program, we create an abstract counterpart. for (auto const& module : program.getModules()) { - modules.emplace_back(module, abstractionInformation, *this->smtSolverFactory); + this->modules.emplace_back(module, abstractionInformation, *this->smtSolverFactory); } // Retrieve the command-update probability ADD, so we can multiply it with the abstraction BDD later. commandUpdateProbabilitiesAdd = modules.front().getCommandUpdateProbabilitiesAdd(); - // Create the state set abstractors. - initialStateAbstractor = storm::abstraction::StateSetAbstractor(abstractionInformation, {program.getInitialConstruct().getInitialStatesExpression()}, *this->smtSolverFactory); - bottomStateAbstractor = storm::abstraction::StateSetAbstractor(abstractionInformation, program.getAllGuards(true), *this->smtSolverFactory); - // Finally, we build the game the first time. currentGame = buildGame(); + + std::cout << "abs module at " << &modules.front() << std::endl; } template @@ -153,7 +156,7 @@ namespace storm { if (!deadlockStates.isZero()) { deadlockTransitions = (deadlockStates && abstractionInformation.getAllPredicateIdentities() && abstractionInformation.encodePlayer1Choice(0, abstractionInformation.getPlayer1VariableCount()) && abstractionInformation.encodePlayer2Choice(0, gameBdd.second) && abstractionInformation.encodeProbabilisticChoice(0, abstractionInformation.getProbabilisticBranchingVariableCount())).template toAdd(); } - + // Construct the transition matrix by cutting away the transitions of unreachable states. storm::dd::Add transitionMatrix = (gameBdd.first && reachableStates).template toAdd() * commandUpdateProbabilitiesAdd + deadlockTransitions; @@ -161,7 +164,7 @@ namespace storm { std::set allNondeterminismVariables = usedPlayer2Variables; allNondeterminismVariables.insert(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()); - + return std::make_unique>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStates, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables(), abstractionInformation.getSourceSuccessorVariablePairs(), std::set(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), usedPlayer2Variables, allNondeterminismVariables, std::set(abstractionInformation.getProbabilisticBranchingVariables().begin(), abstractionInformation.getProbabilisticBranchingVariables().end()), abstractionInformation.getPredicateToBddMap()); } diff --git a/src/abstraction/prism/AbstractProgram.h b/src/abstraction/prism/AbstractProgram.h index 497b22414..8c3f986c4 100644 --- a/src/abstraction/prism/AbstractProgram.h +++ b/src/abstraction/prism/AbstractProgram.h @@ -45,6 +45,12 @@ namespace storm { */ AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector const& initialPredicates, std::unique_ptr&& smtSolverFactory = std::make_unique(), bool addAllGuards = false); + AbstractProgram(AbstractProgram const&) = default; + AbstractProgram& operator=(AbstractProgram const&) = default; + AbstractProgram(AbstractProgram&&) = default; + AbstractProgram& operator=(AbstractProgram&&) = default; + ~AbstractProgram(); + /*! * Uses the current set of predicates to derive the abstract menu game in the form of an ADD. *