diff --git a/src/abstraction/AbstractionInformation.cpp b/src/abstraction/AbstractionInformation.cpp index 7cb5f20d4..f21dfbcc5 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), allPredicateIdentities(ddManager->getBddZero()) { + AbstractionInformation::AbstractionInformation(storm::expressions::ExpressionManager& expressionManager, std::shared_ptr> ddManager) : expressionManager(expressionManager), ddManager(ddManager), allPredicateIdentities(ddManager->getBddOne()) { // Intentionally left empty. } @@ -133,21 +133,21 @@ namespace storm { STORM_LOG_THROW(player1Variables.empty() && player2Variables.empty() && probabilisticBranchingVariables.empty(), storm::exceptions::InvalidOperationException, "Variables have already been created."); for (uint64_t index = 0; index < player1VariableCount; ++index) { - storm::expressions::Variable newVariable = ddManager->addMetaVariable("pl1" + std::to_string(index)).first; + storm::expressions::Variable newVariable = ddManager->addMetaVariable("pl1_" + std::to_string(index)).first; player1Variables.push_back(newVariable); player1VariableBdds.push_back(ddManager->getEncoding(newVariable, 1)); } STORM_LOG_DEBUG("Created " << player1VariableCount << " player 1 variables."); for (uint64_t index = 0; index < player2VariableCount; ++index) { - storm::expressions::Variable newVariable = ddManager->addMetaVariable("pl2" + std::to_string(index)).first; + storm::expressions::Variable newVariable = ddManager->addMetaVariable("pl2_" + std::to_string(index)).first; player2Variables.push_back(newVariable); player2VariableBdds.push_back(ddManager->getEncoding(newVariable, 1)); } STORM_LOG_DEBUG("Created " << player2VariableCount << " player 2 variables."); for (uint64_t index = 0; index < probabilisticBranchingVariableCount; ++index) { - storm::expressions::Variable newVariable = ddManager->addMetaVariable("pb" + std::to_string(index)).first; + storm::expressions::Variable newVariable = ddManager->addMetaVariable("pb_" + std::to_string(index)).first; probabilisticBranchingVariables.push_back(newVariable); probabilisticBranchingVariableBdds.push_back(ddManager->getEncoding(newVariable, 1)); } @@ -172,7 +172,7 @@ namespace storm { template storm::dd::Bdd AbstractionInformation::getPlayer2ZeroCube(uint_fast64_t numberOfVariables, uint_fast64_t offset) const { storm::dd::Bdd result = ddManager->getBddOne(); - for (uint_fast64_t index = offset; index < numberOfVariables - offset; ++index) { + for (uint_fast64_t index = offset; index < numberOfVariables; ++index) { result &= player2VariableBdds[index]; } STORM_LOG_ASSERT(!result.isZero(), "Zero cube must not be zero."); @@ -184,16 +184,31 @@ namespace storm { return player1Variables; } + template + std::set AbstractionInformation::getPlayer1VariableSet(uint_fast64_t count) const { + return std::set(player1Variables.begin(), player1Variables.begin() + count); + } + template std::vector const& AbstractionInformation::getPlayer2Variables() const { return player2Variables; } + template + std::set AbstractionInformation::getPlayer2VariableSet(uint_fast64_t count) const { + return std::set(player2Variables.begin(), player2Variables.begin() + count); + } + template std::vector const& AbstractionInformation::getProbabilisticBranchingVariables() const { return probabilisticBranchingVariables; } + template + std::set AbstractionInformation::getProbabilisticBranchingVariableSet(uint_fast64_t count) const { + return std::set(probabilisticBranchingVariables.begin(), probabilisticBranchingVariables.begin() + count); + } + template std::set const& AbstractionInformation::getSourceVariables() const { return sourceVariables; diff --git a/src/abstraction/AbstractionInformation.h b/src/abstraction/AbstractionInformation.h index c0f698c16..76c721f77 100644 --- a/src/abstraction/AbstractionInformation.h +++ b/src/abstraction/AbstractionInformation.h @@ -214,6 +214,14 @@ namespace storm { */ std::vector const& getPlayer1Variables() const; + /*! + * Retrieves the set of player 1 variables. + * + * @param count The number of player 1 variables to include. + * @return The set of player 1 variables. + */ + std::set getPlayer1VariableSet(uint_fast64_t count) const; + /*! * Retrieves the number of player 1 variables. * @@ -235,6 +243,14 @@ namespace storm { */ std::size_t getPlayer2VariableCount() const; + /*! + * Retrieves the set of player 2 variables. + * + * @param count The number of player 2 variables to include. + * @return The set of player 2 variables. + */ + std::set getPlayer2VariableSet(uint_fast64_t count) const; + /*! * Retrieves the meta variables associated with the probabilistic branching. * @@ -242,6 +258,14 @@ namespace storm { */ std::vector const& getProbabilisticBranchingVariables() const; + /*! + * Retrieves the set of probabilistic branching variables. + * + * @param count The number of probabilistic branching variables to include. + * @return The set of probabilistic branching variables. + */ + std::set getProbabilisticBranchingVariableSet(uint_fast64_t count) const; + /*! * Retrieves the number of probabilistic branching variables. * diff --git a/src/abstraction/StateSetAbstractor.cpp b/src/abstraction/StateSetAbstractor.cpp index 313202662..e3d6b6949 100644 --- a/src/abstraction/StateSetAbstractor.cpp +++ b/src/abstraction/StateSetAbstractor.cpp @@ -13,11 +13,6 @@ namespace storm { template 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()) { - smtSolver->add(constraint); - } - // Assert all state predicates. for (auto const& predicate : statePredicates) { smtSolver->add(predicate); @@ -27,13 +22,6 @@ namespace storm { concretePredicateVariables.insert(usedVariables.begin(), usedVariables.end()); localExpressionInformation.relate(usedVariables); } - - // Refine the command based on all initial predicates. - std::vector allPredicateIndices(abstractionInformation.getNumberOfPredicates()); - for (auto index = 0; index < abstractionInformation.getNumberOfPredicates(); ++index) { - allPredicateIndices[index] = index; - } - this->refine(allPredicateIndices); } template @@ -58,6 +46,11 @@ namespace storm { needsRecomputation = true; } + template + void StateSetAbstractor::constrain(storm::expressions::Expression const& constraint) { + smtSolver->add(constraint); + } + template void StateSetAbstractor::constrain(storm::dd::Bdd const& newConstraint) { // If the constraint is different from the last one, we add it to the solver. @@ -109,7 +102,7 @@ namespace storm { storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddZero(); uint_fast64_t modelCounter = 0; - smtSolver->allSat(decisionVariables, [&result,this,&modelCounter] (storm::solver::SmtSolver::ModelReference const& model) { result |= getStateBdd(model); return true; } ); + smtSolver->allSat(decisionVariables, [&result,this,&modelCounter] (storm::solver::SmtSolver::ModelReference const& model) { result |= getStateBdd(model); ++modelCounter; return true; } ); cachedBdd = result; } diff --git a/src/abstraction/StateSetAbstractor.h b/src/abstraction/StateSetAbstractor.h index c5348accd..dad33e664 100644 --- a/src/abstraction/StateSetAbstractor.h +++ b/src/abstraction/StateSetAbstractor.h @@ -60,6 +60,14 @@ namespace storm { */ void refine(std::vector const& newPredicateIndices); + /*! + * Constrains the abstract states with the given expression. + * Note that all constaints must be added before the abstractor is used to retrieve the abstract states. + * + * @param constraint The constraint to add. + */ + void constrain(storm::expressions::Expression const& constraint); + /*! * Constraints the abstract states with the given BDD. * diff --git a/src/abstraction/prism/AbstractCommand.cpp b/src/abstraction/prism/AbstractCommand.cpp index 13dc67724..ca6a3a141 100644 --- a/src/abstraction/prism/AbstractCommand.cpp +++ b/src/abstraction/prism/AbstractCommand.cpp @@ -297,7 +297,7 @@ namespace storm { for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) { result += this->getAbstractionInformation().encodeProbabilisticChoice(updateIndex, this->getAbstractionInformation().getProbabilisticBranchingVariableCount()).template toAdd() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(command.get().getUpdate(updateIndex).getLikelihoodExpression())); } - result *= this->getAbstractionInformation().encodePlayer2Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer2VariableCount()).template toAdd(); + result *= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()).template toAdd(); return result; } diff --git a/src/abstraction/prism/AbstractModule.cpp b/src/abstraction/prism/AbstractModule.cpp index 7a396c517..3adcc9860 100644 --- a/src/abstraction/prism/AbstractModule.cpp +++ b/src/abstraction/prism/AbstractModule.cpp @@ -27,11 +27,6 @@ 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. diff --git a/src/abstraction/prism/AbstractModule.h b/src/abstraction/prism/AbstractModule.h index 77c267da1..28428e2f1 100644 --- a/src/abstraction/prism/AbstractModule.h +++ b/src/abstraction/prism/AbstractModule.h @@ -31,13 +31,11 @@ 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 const&) = default; + AbstractModule& operator=(AbstractModule const&) = default; AbstractModule(AbstractModule&&) = default; AbstractModule& operator=(AbstractModule&&) = default; - ~AbstractModule(); - /*! * Refines the abstract module with the given predicates. * diff --git a/src/abstraction/prism/AbstractProgram.cpp b/src/abstraction/prism/AbstractProgram.cpp index f8056ec72..1eeeef9ad 100644 --- a/src/abstraction/prism/AbstractProgram.cpp +++ b/src/abstraction/prism/AbstractProgram.cpp @@ -16,17 +16,12 @@ 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(abstractionInformation, program.getAllExpressionVariables(), {program.getInitialConstruct().getInitialStatesExpression()}, *this->smtSolverFactory), addedAllGuards(addAllGuards), bottomStateAbstractor(abstractionInformation, program.getAllExpressionVariables(), program.getAllGuards(true), *this->smtSolverFactory), currentGame(nullptr) { + : program(program), smtSolverFactory(std::move(smtSolverFactory)), abstractionInformation(expressionManager), modules(), 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. @@ -38,6 +33,8 @@ namespace storm { } for (auto const& range : this->program.get().getAllRangeExpressions()) { abstractionInformation.addConstraint(range); + initialStateAbstractor.constrain(range); + bottomStateAbstractor.constrain(range); } uint_fast64_t totalNumberOfCommands = 0; @@ -61,13 +58,14 @@ namespace storm { abstractionInformation.createEncodingVariables(static_cast(std::ceil(std::log2(totalNumberOfCommands))), 100, static_cast(std::ceil(std::log2(maximalUpdateCount)))); // Now that we have created all other DD variables, we create the DD variables for the predicates. + std::vector allPredicateIndices; if (addAllGuards) { for (auto const& guard : allGuards) { - abstractionInformation.addPredicate(guard); + allPredicateIndices.push_back(abstractionInformation.addPredicate(guard)); } } for (auto const& predicate : initialPredicates) { - abstractionInformation.addPredicate(predicate); + allPredicateIndices.push_back(abstractionInformation.addPredicate(predicate)); } // For each module of the concrete program, we create an abstract counterpart. @@ -75,13 +73,15 @@ namespace storm { this->modules.emplace_back(module, abstractionInformation, *this->smtSolverFactory); } + // Refine the state abstractors using the initial predicates. + initialStateAbstractor.refine(allPredicateIndices); + bottomStateAbstractor.refine(allPredicateIndices); + // Retrieve the command-update probability ADD, so we can multiply it with the abstraction BDD later. commandUpdateProbabilitiesAdd = modules.front().getCommandUpdateProbabilitiesAdd(); // Finally, we build the game the first time. currentGame = buildGame(); - - std::cout << "abs module at " << &modules.front() << std::endl; } template @@ -129,15 +129,17 @@ namespace storm { std::pair, uint_fast64_t> gameBdd = modules.front().getAbstractBdd(); // Construct a set of all unnecessary variables, so we can abstract from it. - std::set variablesToAbstract(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()); - variablesToAbstract.insert(abstractionInformation.getPlayer2Variables().begin(), abstractionInformation.getPlayer2Variables().end()); - variablesToAbstract.insert(abstractionInformation.getProbabilisticBranchingVariables().begin(), abstractionInformation.getProbabilisticBranchingVariables().begin() + gameBdd.second); - + std::set variablesToAbstract(abstractionInformation.getPlayer1VariableSet(abstractionInformation.getPlayer1VariableCount())); + auto player2Variables = abstractionInformation.getPlayer2VariableSet(gameBdd.second); + variablesToAbstract.insert(player2Variables.begin(), player2Variables.end()); + auto probBranchingVariables = abstractionInformation.getProbabilisticBranchingVariableSet(abstractionInformation.getProbabilisticBranchingVariableCount()); + variablesToAbstract.insert(probBranchingVariables.begin(), probBranchingVariables.end()); + // Do a reachability analysis on the raw transition relation. 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) { diff --git a/src/abstraction/prism/AbstractProgram.h b/src/abstraction/prism/AbstractProgram.h index 8c3f986c4..8b4eb9a82 100644 --- a/src/abstraction/prism/AbstractProgram.h +++ b/src/abstraction/prism/AbstractProgram.h @@ -49,7 +49,6 @@ namespace storm { 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. @@ -98,12 +97,12 @@ namespace storm { // A factory that can be used to create new SMT solvers. std::unique_ptr smtSolverFactory; + // An object containing all information about the abstraction like predicates and the corresponding DDs. + AbstractionInformation abstractionInformation; + // The abstract modules of the abstract program. std::vector> modules; - // An object containing all information about the abstraction like predicates and the corresponding DDs. - AbstractionInformation abstractionInformation; - // A state-set abstractor used to determine the initial states of the abstraction. StateSetAbstractor initialStateAbstractor;