From 82a7c065034864a6db243b877f950aa8920be9d0 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 27 Nov 2016 14:49:35 +0100 Subject: [PATCH] renamed abstraction classes for Sebastian --- .../abstraction/prism/AbstractProgram.cpp | 349 ------------------ src/storm/abstraction/prism/AbstractProgram.h | 151 -------- ...tractCommand.cpp => CommandAbstractor.cpp} | 48 +-- ...{AbstractCommand.h => CommandAbstractor.h} | 6 +- ...bstractModule.cpp => ModuleAbstractor.cpp} | 32 +- .../{AbstractModule.h => ModuleAbstractor.h} | 22 +- .../prism/PrismMenuGameAbstractor.cpp | 326 +++++++++++++++- .../prism/PrismMenuGameAbstractor.h | 147 +++++++- src/test/abstraction/PrismMenuGameTest.cpp | 118 +++--- src/test/utility/GraphTest.cpp | 18 +- 10 files changed, 567 insertions(+), 650 deletions(-) delete mode 100644 src/storm/abstraction/prism/AbstractProgram.cpp delete mode 100644 src/storm/abstraction/prism/AbstractProgram.h rename src/storm/abstraction/prism/{AbstractCommand.cpp => CommandAbstractor.cpp} (86%) rename src/storm/abstraction/prism/{AbstractCommand.h => CommandAbstractor.h} (97%) rename src/storm/abstraction/prism/{AbstractModule.cpp => ModuleAbstractor.cpp} (69%) rename src/storm/abstraction/prism/{AbstractModule.h => ModuleAbstractor.h} (82%) diff --git a/src/storm/abstraction/prism/AbstractProgram.cpp b/src/storm/abstraction/prism/AbstractProgram.cpp deleted file mode 100644 index f2e5f718d..000000000 --- a/src/storm/abstraction/prism/AbstractProgram.cpp +++ /dev/null @@ -1,349 +0,0 @@ -#include "storm/abstraction/prism/AbstractProgram.h" - -#include "storm/abstraction/BottomStateResult.h" -#include "storm/abstraction/GameBddResult.h" - -#include "storm/storage/BitVector.h" - -#include "storm/storage/prism/Program.h" - -#include "storm/storage/dd/DdManager.h" -#include "storm/storage/dd/Add.h" - -#include "storm/models/symbolic/StandardRewardModel.h" - -#include "storm/utility/dd.h" -#include "storm/utility/macros.h" -#include "storm/utility/solver.h" -#include "storm/exceptions/WrongFormatException.h" -#include "storm/exceptions/InvalidArgumentException.h" - -#include "storm-config.h" -#include "storm/adapters/CarlAdapter.h" - -namespace storm { - namespace abstraction { - namespace prism { - -#undef LOCAL_DEBUG - - template - AbstractProgram::AbstractProgram(storm::prism::Program const& program, - std::shared_ptr const& smtSolverFactory, - bool addAllGuards) - : program(program), smtSolverFactory(smtSolverFactory), abstractionInformation(program.getManager()), modules(), initialStateAbstractor(abstractionInformation, program.getAllExpressionVariables(), {program.getInitialStatesExpression()}, this->smtSolverFactory), addedAllGuards(addAllGuards), currentGame(nullptr), refinementPerformed(false) { - - // 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. - STORM_LOG_THROW(program.getNumberOfModules() == 1, storm::exceptions::WrongFormatException, "Cannot create abstract program from program containing too many modules."); - - // Add all variables and range expressions to the information object. - for (auto const& variable : this->program.get().getAllExpressionVariables()) { - abstractionInformation.addExpressionVariable(variable); - } - for (auto const& range : this->program.get().getAllRangeExpressions()) { - abstractionInformation.addConstraint(range); - initialStateAbstractor.constrain(range); - } - - uint_fast64_t totalNumberOfCommands = 0; - uint_fast64_t maximalUpdateCount = 0; - std::vector allGuards; - for (auto const& module : program.getModules()) { - // If we were requested to add all guards to the set of predicates, we do so now. - for (auto const& command : module.getCommands()) { - if (addAllGuards) { - allGuards.push_back(command.getGuardExpression()); - } - maximalUpdateCount = std::max(maximalUpdateCount, static_cast(command.getNumberOfUpdates())); - } - - totalNumberOfCommands += module.getNumberOfCommands(); - } - - // 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)))); - - // For each module of the concrete program, we create an abstract counterpart. - for (auto const& module : program.getModules()) { - this->modules.emplace_back(module, abstractionInformation, this->smtSolverFactory, addAllGuards); - } - - // Retrieve the command-update probability ADD, so we can multiply it with the abstraction BDD later. - commandUpdateProbabilitiesAdd = modules.front().getCommandUpdateProbabilitiesAdd(); - - // Now that we have created all other DD variables, we create the DD variables for the predicates. - std::vector initialPredicates; - if (addAllGuards) { - for (auto const& guard : allGuards) { - initialPredicates.push_back(guard); - } - } - - // Finally, refine using the all predicates and build game as a by-product. - this->refine(initialPredicates); - } - - template - 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& predicate : predicates) { - STORM_LOG_THROW(predicate.hasBooleanType(), storm::exceptions::InvalidArgumentException, "Expecting a predicate of type bool."); - newPredicateIndices.push_back(abstractionInformation.addPredicate(predicate)); - } - - // Refine all abstract modules. - for (auto& module : modules) { - module.refine(newPredicateIndices); - } - - // Refine initial state abstractor. - initialStateAbstractor.refine(newPredicateIndices); - - // Update the flag that stores whether a refinement was performed. - refinementPerformed = refinementPerformed || !newPredicateIndices.empty(); - } - - template - MenuGame AbstractProgram::abstract() { - if (refinementPerformed) { - currentGame = buildGame(); - refinementPerformed = true; - } - return *currentGame; - } - - template - AbstractionInformation const& AbstractProgram::getAbstractionInformation() const { - return abstractionInformation; - } - - template - storm::expressions::Expression const& AbstractProgram::getGuard(uint64_t player1Choice) const { - return modules.front().getGuard(player1Choice); - } - - template - std::map AbstractProgram::getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const { - return modules.front().getVariableUpdates(player1Choice, auxiliaryChoice); - } - - template - storm::dd::Bdd AbstractProgram::getStates(storm::expressions::Expression const& predicate) { - STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created."); - return abstractionInformation.getPredicateSourceVariable(predicate); - } - - template - std::unique_ptr> AbstractProgram::buildGame() { - // As long as there is only one module, we only build its game representation. - GameBddResult game = modules.front().getAbstractBdd(); - - // Construct a set of all unnecessary variables, so we can abstract from it. - std::set variablesToAbstract(abstractionInformation.getPlayer1VariableSet(abstractionInformation.getPlayer1VariableCount())); - auto player2Variables = abstractionInformation.getPlayer2VariableSet(game.numberOfPlayer2Variables); - variablesToAbstract.insert(player2Variables.begin(), player2Variables.end()); - auto auxVariables = abstractionInformation.getAuxVariableSet(0, abstractionInformation.getAuxVariableCount()); - variablesToAbstract.insert(auxVariables.begin(), auxVariables.end()); - - // Do a reachability analysis on the raw transition relation. - storm::dd::Bdd transitionRelation = game.bdd.existsAbstract(variablesToAbstract); - storm::dd::Bdd initialStates = initialStateAbstractor.getAbstractStates(); - storm::dd::Bdd reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); - - // Find the deadlock states in the model. Note that this does not find the 'deadlocks' in bottom states, - // as the bottom states are not contained in the reachable states. - storm::dd::Bdd deadlockStates = transitionRelation.existsAbstract(abstractionInformation.getSuccessorVariables()); - deadlockStates = reachableStates && !deadlockStates; - - // 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, game.numberOfPlayer2Variables) && abstractionInformation.encodeAux(0, 0, abstractionInformation.getAuxVariableCount())).template toAdd(); - } - - // Compute bottom states and the appropriate transitions if necessary. - BottomStateResult bottomStateResult(abstractionInformation.getDdManager().getBddZero(), abstractionInformation.getDdManager().getBddZero()); - bool hasBottomStates = false; - if (!addedAllGuards) { - bottomStateResult = modules.front().getBottomStateTransitions(reachableStates, game.numberOfPlayer2Variables); - hasBottomStates = !bottomStateResult.states.isZero(); - } - - // Construct the transition matrix by cutting away the transitions of unreachable states. - storm::dd::Add transitionMatrix = (game.bdd && reachableStates).template toAdd(); - transitionMatrix *= commandUpdateProbabilitiesAdd; - transitionMatrix += deadlockTransitions; - - // Extend the current game information with the 'non-bottom' tag before potentially adding bottom state transitions. - transitionMatrix *= (abstractionInformation.getBottomStateBdd(true, true) && abstractionInformation.getBottomStateBdd(false, true)).template toAdd(); - reachableStates &= abstractionInformation.getBottomStateBdd(true, true); - initialStates &= abstractionInformation.getBottomStateBdd(true, true); - - // If there are bottom transitions, exnted the transition matrix and reachable states now. - if (hasBottomStates) { - transitionMatrix += bottomStateResult.transitions.template toAdd(); - reachableStates |= bottomStateResult.states; - } - - std::set usedPlayer2Variables(abstractionInformation.getPlayer2Variables().begin(), abstractionInformation.getPlayer2Variables().begin() + game.numberOfPlayer2Variables); - - std::set allNondeterminismVariables = usedPlayer2Variables; - allNondeterminismVariables.insert(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()); - - std::set allSourceVariables(abstractionInformation.getSourceVariables()); - allSourceVariables.insert(abstractionInformation.getBottomStateVariable(true)); - std::set allSuccessorVariables(abstractionInformation.getSuccessorVariables()); - allSuccessorVariables.insert(abstractionInformation.getBottomStateVariable(false)); - - return std::make_unique>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStateResult.states, allSourceVariables, allSuccessorVariables, abstractionInformation.getExtendedSourceSuccessorVariablePairs(), std::set(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), usedPlayer2Variables, allNondeterminismVariables, auxVariables, abstractionInformation.getPredicateToBddMap()); - } - - template - void AbstractProgram::exportToDot(std::string const& filename, storm::dd::Bdd const& highlightStatesBdd, storm::dd::Bdd const& filter) const { - std::ofstream out(filename); - - storm::dd::Add filteredTransitions = filter.template toAdd() * currentGame->getTransitionMatrix(); - storm::dd::Bdd filteredTransitionsBdd = filteredTransitions.toBdd().existsAbstract(currentGame->getNondeterminismVariables()); - storm::dd::Bdd filteredReachableStates = storm::utility::dd::computeReachableStates(currentGame->getInitialStates(), filteredTransitionsBdd, currentGame->getRowVariables(), currentGame->getColumnVariables()); - filteredTransitions *= filteredReachableStates.template toAdd(); - - // Determine all initial states so we can color them blue. - std::unordered_set initialStates; - storm::dd::Add initialStatesAsAdd = currentGame->getInitialStates().template toAdd(); - for (auto stateValue : initialStatesAsAdd) { - std::stringstream stateName; - for (auto const& var : currentGame->getRowVariables()) { - if (stateValue.first.getBooleanValue(var)) { - stateName << "1"; - } else { - stateName << "0"; - } - } - initialStates.insert(stateName.str()); - } - - // Determine all highlight states so we can color them red. - std::unordered_set highlightStates; - storm::dd::Add highlightStatesAdd = highlightStatesBdd.template toAdd(); - for (auto stateValue : highlightStatesAdd) { - std::stringstream stateName; - for (auto const& var : currentGame->getRowVariables()) { - if (stateValue.first.getBooleanValue(var)) { - stateName << "1"; - } else { - stateName << "0"; - } - } - highlightStates.insert(stateName.str()); - } - - out << "digraph game {" << std::endl; - - // Create the player 1 nodes. - storm::dd::Add statesAsAdd = filteredReachableStates.template toAdd(); - for (auto stateValue : statesAsAdd) { - out << "\tpl1_"; - std::stringstream stateName; - for (auto const& var : currentGame->getRowVariables()) { - if (stateValue.first.getBooleanValue(var)) { - stateName << "1"; - } else { - stateName << "0"; - } - } - std::string stateNameAsString = stateName.str(); - out << stateNameAsString; - out << " [ label=\""; - if (stateValue.first.getBooleanValue(abstractionInformation.getBottomStateVariable(true))) { - out << "*\", margin=0, width=0, height=0, shape=\"none\""; - } else { - out << stateName.str() << "\", margin=0, width=0, height=0, shape=\"oval\""; - } - bool isInitial = initialStates.find(stateNameAsString) != initialStates.end(); - bool isHighlight = highlightStates.find(stateNameAsString) != highlightStates.end(); - if (isInitial && isHighlight) { - out << ", style=\"filled\", fillcolor=\"yellow\""; - } else if (isInitial) { - out << ", style=\"filled\", fillcolor=\"blue\""; - } else if (isHighlight) { - out << ", style=\"filled\", fillcolor=\"red\""; - } - out << " ];" << std::endl; - } - - // Create the nodes of the second player. - storm::dd::Add player2States = filteredTransitions.toBdd().existsAbstract(currentGame->getColumnVariables()).existsAbstract(currentGame->getPlayer2Variables()).template toAdd(); - for (auto stateValue : player2States) { - out << "\tpl2_"; - std::stringstream stateName; - for (auto const& var : currentGame->getRowVariables()) { - if (stateValue.first.getBooleanValue(var)) { - stateName << "1"; - } else { - stateName << "0"; - } - } - uint_fast64_t index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount()); - out << stateName.str() << "_" << index; - out << " [ shape=\"square\", width=0, height=0, margin=0, label=\"" << index << "\" ];" << std::endl; - out << "\tpl1_" << stateName.str() << " -> " << "pl2_" << stateName.str() << "_" << index << " [ label=\"" << index << "\" ];" << std::endl; - } - - // Create the nodes of the probabilistic player. - storm::dd::Add playerPStates = filteredTransitions.toBdd().existsAbstract(currentGame->getColumnVariables()).template toAdd(); - for (auto stateValue : playerPStates) { - out << "\tplp_"; - std::stringstream stateName; - for (auto const& var : currentGame->getRowVariables()) { - if (stateValue.first.getBooleanValue(var)) { - stateName << "1"; - } else { - stateName << "0"; - } - } - uint_fast64_t index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount()); - stateName << "_" << index; - index = abstractionInformation.decodePlayer2Choice(stateValue.first, currentGame->getPlayer2Variables().size()); - out << stateName.str() << "_" << index; - out << " [ shape=\"point\", label=\"\" ];" << std::endl; - out << "\tpl2_" << stateName.str() << " -> " << "plp_" << stateName.str() << "_" << index << " [ label=\"" << index << "\" ];" << std::endl; - } - - for (auto stateValue : filteredTransitions) { - std::stringstream sourceStateName; - std::stringstream successorStateName; - for (auto const& var : currentGame->getRowVariables()) { - if (stateValue.first.getBooleanValue(var)) { - sourceStateName << "1"; - } else { - sourceStateName << "0"; - } - } - for (auto const& var : currentGame->getColumnVariables()) { - if (stateValue.first.getBooleanValue(var)) { - successorStateName << "1"; - } else { - successorStateName << "0"; - } - } - uint_fast64_t pl1Index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount()); - uint_fast64_t pl2Index = abstractionInformation.decodePlayer2Choice(stateValue.first, currentGame->getPlayer2Variables().size()); - out << "\tplp_" << sourceStateName.str() << "_" << pl1Index << "_" << pl2Index << " -> pl1_" << successorStateName.str() << " [ label=\"" << stateValue.second << "\"];" << std::endl; - } - - out << "}" << std::endl; - } - - // Explicitly instantiate the class. - template class AbstractProgram; - template class AbstractProgram; -#ifdef STORM_HAVE_CARL - template class AbstractProgram; -#endif - } - } -} diff --git a/src/storm/abstraction/prism/AbstractProgram.h b/src/storm/abstraction/prism/AbstractProgram.h deleted file mode 100644 index c67506e61..000000000 --- a/src/storm/abstraction/prism/AbstractProgram.h +++ /dev/null @@ -1,151 +0,0 @@ -#pragma once - -#include "storm/storage/dd/DdType.h" - -#include "storm/abstraction/AbstractionInformation.h" -#include "storm/abstraction/MenuGame.h" -#include "storm/abstraction/prism/AbstractModule.h" - -#include "storm/storage/dd/Add.h" - -#include "storm/storage/expressions/Expression.h" - -namespace storm { - namespace utility { - namespace solver { - class SmtSolverFactory; - } - } - - namespace models { - namespace symbolic { - template - class StochasticTwoPlayerGame; - } - } - - namespace prism { - // Forward-declare concrete Program class. - class Program; - } - - namespace abstraction { - namespace prism { - - template - class AbstractProgram { - public: - /*! - * Constructs an abstract program from the given program and the initial predicates. - * - * @param expressionManager The manager responsible for the expressions of the program. - * @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. - */ - 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; - AbstractProgram(AbstractProgram&&) = default; - AbstractProgram& operator=(AbstractProgram&&) = default; - - /*! - * Uses the current set of predicates to derive the abstract menu game in the form of an ADD. - * - * @return The abstract stochastic two player game. - */ - MenuGame abstract(); - - /*! - * Retrieves information about the abstraction. - * - * @return The abstraction information object. - */ - AbstractionInformation const& getAbstractionInformation() const; - - /*! - * Retrieves the guard predicate of the given player 1 choice. - * - * @param player1Choice The choice for which to retrieve the guard. - * @return The guard of the player 1 choice. - */ - storm::expressions::Expression const& getGuard(uint64_t player1Choice) const; - - /*! - * Retrieves a mapping from variables to expressions that define their updates wrt. to the given player - * 1 choice and auxiliary choice. - */ - std::map getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) 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. - * - * @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); - - /*! - * Refines the abstract program with the given predicates. - * - * @param predicates The new predicates. - */ - void refine(std::vector const& predicates); - - /*! - * Exports the current state of the abstraction in the dot format to the given file. - * - * @param filename The name of the file to which to write the dot output. - * @param highlightStates A BDD characterizing states that will be highlighted. - * @param filter A filter that is applied to select which part of the game to export. - */ - void exportToDot(std::string const& filename, storm::dd::Bdd const& highlightStates, storm::dd::Bdd const& filter) const; - - private: - /*! - * Builds the stochastic game representing the abstraction of the program. - * - * @return The stochastic game. - */ - std::unique_ptr> buildGame(); - - /*! - * Decodes the given choice over the auxiliary and successor variables to a mapping from update indices - * to bit vectors representing the successors under these updates. - * - * @param choice The choice to decode. - */ - std::map decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd const& choice) const; - - // The concrete program this abstract program refers to. - std::reference_wrapper program; - - // A factory that can be used to create new SMT solvers. - std::shared_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; - - // 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; - - // An ADD characterizing the probabilities of commands and their updates. - storm::dd::Add commandUpdateProbabilitiesAdd; - - // The current game-based abstraction. - std::unique_ptr> currentGame; - - // A flag storing whether a refinement was performed. - bool refinementPerformed; - }; - } - } -} diff --git a/src/storm/abstraction/prism/AbstractCommand.cpp b/src/storm/abstraction/prism/CommandAbstractor.cpp similarity index 86% rename from src/storm/abstraction/prism/AbstractCommand.cpp rename to src/storm/abstraction/prism/CommandAbstractor.cpp index 0124d24d2..605bd0e9b 100644 --- a/src/storm/abstraction/prism/AbstractCommand.cpp +++ b/src/storm/abstraction/prism/CommandAbstractor.cpp @@ -1,4 +1,4 @@ -#include "storm/abstraction/prism/AbstractCommand.h" +#include "storm/abstraction/prism/CommandAbstractor.h" #include @@ -23,7 +23,7 @@ namespace storm { namespace abstraction { namespace prism { template - AbstractCommand::AbstractCommand(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool guardIsPredicate) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), command(command), localExpressionInformation(abstractionInformation.getVariables()), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), skipBottomStates(false), forceRecomputation(true), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, abstractionInformation.getExpressionVariables(), {!command.getGuardExpression()}, smtSolverFactory) { + CommandAbstractor::CommandAbstractor(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool guardIsPredicate) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), command(command), localExpressionInformation(abstractionInformation.getVariables()), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), skipBottomStates(false), forceRecomputation(true), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, abstractionInformation.getExpressionVariables(), {!command.getGuardExpression()}, smtSolverFactory) { // Make the second component of relevant predicates have the right size. relevantPredicatesAndVariables.second.resize(command.getNumberOfUpdates()); @@ -39,7 +39,7 @@ namespace storm { } template - void AbstractCommand::refine(std::vector const& predicates) { + void CommandAbstractor::refine(std::vector const& predicates) { // Add all predicates to the variable partition. for (auto predicateIndex : predicates) { localExpressionInformation.addExpression(this->getAbstractionInformation().getPredicateByIndex(predicateIndex), predicateIndex); @@ -63,17 +63,17 @@ namespace storm { } template - storm::expressions::Expression const& AbstractCommand::getGuard() const { + storm::expressions::Expression const& CommandAbstractor::getGuard() const { return command.get().getGuardExpression(); } template - std::map AbstractCommand::getVariableUpdates(uint64_t auxiliaryChoice) const { + std::map CommandAbstractor::getVariableUpdates(uint64_t auxiliaryChoice) const { return command.get().getUpdate(auxiliaryChoice).getAsVariableToExpressionMap(); } template - void AbstractCommand::recomputeCachedBdd() { + void CommandAbstractor::recomputeCachedBdd() { STORM_LOG_TRACE("Recomputing BDD for command " << command.get()); auto start = std::chrono::high_resolution_clock::now(); @@ -136,7 +136,7 @@ namespace storm { } template - std::pair, std::set> AbstractCommand::computeRelevantPredicates(std::vector const& assignments) const { + std::pair, std::set> CommandAbstractor::computeRelevantPredicates(std::vector const& assignments) const { std::pair, std::set> result; std::set assignedVariables; @@ -162,7 +162,7 @@ namespace storm { } template - std::pair, std::vector>> AbstractCommand::computeRelevantPredicates() const { + std::pair, std::vector>> CommandAbstractor::computeRelevantPredicates() const { std::pair, std::vector>> result; // To start with, all predicates related to the guard are relevant source predicates. @@ -179,7 +179,7 @@ namespace storm { } template - bool AbstractCommand::relevantPredicatesChanged(std::pair, std::vector>> const& newRelevantPredicates) const { + bool CommandAbstractor::relevantPredicatesChanged(std::pair, std::vector>> const& newRelevantPredicates) const { if (newRelevantPredicates.first.size() > relevantPredicatesAndVariables.first.size()) { return true; } @@ -194,7 +194,7 @@ namespace storm { } template - void AbstractCommand::addMissingPredicates(std::pair, std::vector>> const& newRelevantPredicates) { + void CommandAbstractor::addMissingPredicates(std::pair, std::vector>> const& newRelevantPredicates) { // Determine and add new relevant source predicates. std::vector> newSourceVariables = this->getAbstractionInformation().declareNewVariables(relevantPredicatesAndVariables.first, newRelevantPredicates.first); for (auto const& element : newSourceVariables) { @@ -220,7 +220,7 @@ namespace storm { } template - storm::dd::Bdd AbstractCommand::getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model) const { + storm::dd::Bdd CommandAbstractor::getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model) const { storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddOne(); for (auto const& variableIndexPair : relevantPredicatesAndVariables.first) { if (model.getBooleanValue(variableIndexPair.first)) { @@ -235,7 +235,7 @@ namespace storm { } template - storm::dd::Bdd AbstractCommand::getDistributionBdd(storm::solver::SmtSolver::ModelReference const& model) const { + storm::dd::Bdd CommandAbstractor::getDistributionBdd(storm::solver::SmtSolver::ModelReference const& model) const { storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddZero(); for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) { @@ -259,14 +259,14 @@ namespace storm { } template - storm::dd::Bdd AbstractCommand::computeMissingIdentities() const { + storm::dd::Bdd CommandAbstractor::computeMissingIdentities() const { storm::dd::Bdd identities = computeMissingGlobalIdentities(); identities &= computeMissingUpdateIdentities(); return identities; } template - storm::dd::Bdd AbstractCommand::computeMissingUpdateIdentities() const { + storm::dd::Bdd CommandAbstractor::computeMissingUpdateIdentities() const { storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddZero(); for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) { // Compute the identities that are missing for this update. @@ -293,7 +293,7 @@ namespace storm { } template - storm::dd::Bdd AbstractCommand::computeMissingGlobalIdentities() const { + storm::dd::Bdd CommandAbstractor::computeMissingGlobalIdentities() const { auto relevantIt = relevantPredicatesAndVariables.first.begin(); auto relevantIte = relevantPredicatesAndVariables.first.end(); @@ -309,7 +309,7 @@ namespace storm { } template - GameBddResult AbstractCommand::getAbstractBdd() { + GameBddResult CommandAbstractor::abstract() { if (forceRecomputation) { this->recomputeCachedBdd(); } else { @@ -320,7 +320,7 @@ namespace storm { } template - BottomStateResult AbstractCommand::getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables) { + BottomStateResult CommandAbstractor::getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables) { STORM_LOG_TRACE("Computing bottom state transitions of command " << command.get()); BottomStateResult result(this->getAbstractionInformation().getDdManager().getBddZero(), this->getAbstractionInformation().getDdManager().getBddZero()); @@ -353,7 +353,7 @@ namespace storm { } template - storm::dd::Add AbstractCommand::getCommandUpdateProbabilitiesAdd() const { + storm::dd::Add CommandAbstractor::getCommandUpdateProbabilitiesAdd() const { storm::dd::Add result = this->getAbstractionInformation().getDdManager().template getAddZero(); for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) { result += this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()).template toAdd() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(command.get().getUpdate(updateIndex).getLikelihoodExpression())); @@ -363,24 +363,24 @@ namespace storm { } template - storm::prism::Command const& AbstractCommand::getConcreteCommand() const { + storm::prism::Command const& CommandAbstractor::getConcreteCommand() const { return command.get(); } template - AbstractionInformation const& AbstractCommand::getAbstractionInformation() const { + AbstractionInformation const& CommandAbstractor::getAbstractionInformation() const { return abstractionInformation.get(); } template - AbstractionInformation& AbstractCommand::getAbstractionInformation() { + AbstractionInformation& CommandAbstractor::getAbstractionInformation() { return abstractionInformation.get(); } - template class AbstractCommand; - template class AbstractCommand; + template class CommandAbstractor; + template class CommandAbstractor; #ifdef STORM_HAVE_CARL - template class AbstractCommand; + template class CommandAbstractor; #endif } } diff --git a/src/storm/abstraction/prism/AbstractCommand.h b/src/storm/abstraction/prism/CommandAbstractor.h similarity index 97% rename from src/storm/abstraction/prism/AbstractCommand.h rename to src/storm/abstraction/prism/CommandAbstractor.h index f62ae3838..dbf2b862d 100644 --- a/src/storm/abstraction/prism/AbstractCommand.h +++ b/src/storm/abstraction/prism/CommandAbstractor.h @@ -49,7 +49,7 @@ namespace storm { namespace prism { template - class AbstractCommand { + class CommandAbstractor { public: /*! * Constructs an abstract command from the given command and the initial predicates. @@ -59,7 +59,7 @@ namespace storm { * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. * @param guardIsPredicate A flag indicating whether the guard of the command was added as a predicate. */ - AbstractCommand(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool guardIsPredicate = false); + CommandAbstractor(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool guardIsPredicate = false); /*! * Refines the abstract command with the given predicates. @@ -85,7 +85,7 @@ namespace storm { * @return The abstraction of the command in the form of a BDD together with the number of DD variables * used to encode the choices of player 2. */ - GameBddResult getAbstractBdd(); + GameBddResult abstract(); /*! * Retrieves the transitions to bottom states of this command. diff --git a/src/storm/abstraction/prism/AbstractModule.cpp b/src/storm/abstraction/prism/ModuleAbstractor.cpp similarity index 69% rename from src/storm/abstraction/prism/AbstractModule.cpp rename to src/storm/abstraction/prism/ModuleAbstractor.cpp index 2c50b1401..ab9b6c592 100644 --- a/src/storm/abstraction/prism/AbstractModule.cpp +++ b/src/storm/abstraction/prism/ModuleAbstractor.cpp @@ -1,4 +1,4 @@ -#include "storm/abstraction/prism/AbstractModule.h" +#include "storm/abstraction/prism/ModuleAbstractor.h" #include "storm/abstraction/AbstractionInformation.h" #include "storm/abstraction/BottomStateResult.h" @@ -19,7 +19,7 @@ namespace storm { namespace prism { template - AbstractModule::AbstractModule(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool allGuardsAdded) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), commands(), module(module) { + ModuleAbstractor::ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool allGuardsAdded) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), commands(), module(module) { // For each concrete command, we create an abstract counterpart. for (auto const& command : module.getCommands()) { @@ -28,31 +28,31 @@ namespace storm { } template - void AbstractModule::refine(std::vector const& predicates) { + void ModuleAbstractor::refine(std::vector const& predicates) { for (uint_fast64_t index = 0; index < commands.size(); ++index) { STORM_LOG_TRACE("Refining command with index " << index << "."); - AbstractCommand& command = commands[index]; + CommandAbstractor& command = commands[index]; command.refine(predicates); } } template - storm::expressions::Expression const& AbstractModule::getGuard(uint64_t player1Choice) const { + storm::expressions::Expression const& ModuleAbstractor::getGuard(uint64_t player1Choice) const { return commands[player1Choice].getGuard(); } template - std::map AbstractModule::getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const { + std::map ModuleAbstractor::getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const { return commands[player1Choice].getVariableUpdates(auxiliaryChoice); } template - GameBddResult AbstractModule::getAbstractBdd() { + GameBddResult ModuleAbstractor::abstract() { // First, we retrieve the abstractions of all commands. std::vector> commandDdsAndUsedOptionVariableCounts; uint_fast64_t maximalNumberOfUsedOptionVariables = 0; for (auto& command : commands) { - commandDdsAndUsedOptionVariableCounts.push_back(command.getAbstractBdd()); + commandDdsAndUsedOptionVariableCounts.push_back(command.abstract()); maximalNumberOfUsedOptionVariables = std::max(maximalNumberOfUsedOptionVariables, commandDdsAndUsedOptionVariableCounts.back().numberOfPlayer2Variables); } @@ -66,7 +66,7 @@ namespace storm { } template - BottomStateResult AbstractModule::getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables) { + BottomStateResult ModuleAbstractor::getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables) { BottomStateResult result(this->getAbstractionInformation().getDdManager().getBddZero(), this->getAbstractionInformation().getDdManager().getBddZero()); for (auto& command : commands) { @@ -79,7 +79,7 @@ namespace storm { } template - storm::dd::Add AbstractModule::getCommandUpdateProbabilitiesAdd() const { + storm::dd::Add ModuleAbstractor::getCommandUpdateProbabilitiesAdd() const { storm::dd::Add result = this->getAbstractionInformation().getDdManager().template getAddZero(); for (auto const& command : commands) { result += command.getCommandUpdateProbabilitiesAdd(); @@ -88,24 +88,24 @@ namespace storm { } template - std::vector> const& AbstractModule::getCommands() const { + std::vector> const& ModuleAbstractor::getCommands() const { return commands; } template - std::vector>& AbstractModule::getCommands() { + std::vector>& ModuleAbstractor::getCommands() { return commands; } template - AbstractionInformation const& AbstractModule::getAbstractionInformation() const { + AbstractionInformation const& ModuleAbstractor::getAbstractionInformation() const { return abstractionInformation.get(); } - template class AbstractModule; - template class AbstractModule; + template class ModuleAbstractor; + template class ModuleAbstractor; #ifdef STORM_HAVE_CARL - template class AbstractModule; + template class ModuleAbstractor; #endif } } diff --git a/src/storm/abstraction/prism/AbstractModule.h b/src/storm/abstraction/prism/ModuleAbstractor.h similarity index 82% rename from src/storm/abstraction/prism/AbstractModule.h rename to src/storm/abstraction/prism/ModuleAbstractor.h index 82fb73f9f..5bb3e0f07 100644 --- a/src/storm/abstraction/prism/AbstractModule.h +++ b/src/storm/abstraction/prism/ModuleAbstractor.h @@ -2,7 +2,7 @@ #include "storm/storage/dd/DdType.h" -#include "storm/abstraction/prism/AbstractCommand.h" +#include "storm/abstraction/prism/CommandAbstractor.h" #include "storm/storage/expressions/Expression.h" @@ -26,7 +26,7 @@ namespace storm { namespace prism { template - class AbstractModule { + class ModuleAbstractor { public: /*! * Constructs an abstract module from the given module and the initial predicates. @@ -36,12 +36,12 @@ namespace storm { * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. * @param allGuardsAdded A flag indicating whether all guards of the program were added. */ - AbstractModule(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory = std::make_shared(), bool allGuardsAdded = false); + ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory = std::make_shared(), bool allGuardsAdded = false); - AbstractModule(AbstractModule const&) = default; - AbstractModule& operator=(AbstractModule const&) = default; - AbstractModule(AbstractModule&&) = default; - AbstractModule& operator=(AbstractModule&&) = default; + ModuleAbstractor(ModuleAbstractor const&) = default; + ModuleAbstractor& operator=(ModuleAbstractor const&) = default; + ModuleAbstractor(ModuleAbstractor&&) = default; + ModuleAbstractor& operator=(ModuleAbstractor&&) = default; /*! * Refines the abstract module with the given predicates. @@ -69,7 +69,7 @@ namespace storm { * * @return The abstraction of the module in the form of a BDD together with how many option variables were used. */ - GameBddResult getAbstractBdd(); + GameBddResult abstract(); /*! * Retrieves the transitions to bottom states of this module. @@ -92,14 +92,14 @@ namespace storm { * * @return The abstract commands. */ - std::vector> const& getCommands() const; + std::vector> const& getCommands() const; /*! * Retrieves the abstract commands of this abstract module. * * @return The abstract commands. */ - std::vector>& getCommands(); + std::vector>& getCommands(); private: /*! @@ -116,7 +116,7 @@ namespace storm { std::reference_wrapper const> abstractionInformation; // The abstract commands of the abstract module. - std::vector> commands; + std::vector> commands; // The concrete module this abstract module refers to. std::reference_wrapper module; diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index 7789bfc8a..c52f972cd 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -1,51 +1,349 @@ #include "storm/abstraction/prism/PrismMenuGameAbstractor.h" +#include "storm/abstraction/BottomStateResult.h" +#include "storm/abstraction/GameBddResult.h" + +#include "storm/storage/BitVector.h" + +#include "storm/storage/prism/Program.h" + +#include "storm/storage/dd/DdManager.h" +#include "storm/storage/dd/Add.h" + #include "storm/models/symbolic/StandardRewardModel.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/AbstractionSettings.h" +#include "storm/utility/dd.h" +#include "storm/utility/macros.h" +#include "storm/utility/solver.h" +#include "storm/exceptions/WrongFormatException.h" +#include "storm/exceptions/InvalidArgumentException.h" + +#include "storm-config.h" +#include "storm/adapters/CarlAdapter.h" namespace storm { namespace abstraction { namespace prism { +#undef LOCAL_DEBUG + template - PrismMenuGameAbstractor::PrismMenuGameAbstractor(storm::prism::Program const& program, std::shared_ptr const& smtSolverFactory) : abstractProgram(program, smtSolverFactory, storm::settings::getModule().isAddAllGuardsSet()) { - // Intentionally left empty. + PrismMenuGameAbstractor::PrismMenuGameAbstractor(storm::prism::Program const& program, + std::shared_ptr const& smtSolverFactory, + bool addAllGuards) + : program(program), smtSolverFactory(smtSolverFactory), abstractionInformation(program.getManager()), modules(), initialStateAbstractor(abstractionInformation, program.getAllExpressionVariables(), {program.getInitialStatesExpression()}, this->smtSolverFactory), addedAllGuards(addAllGuards), currentGame(nullptr), refinementPerformed(false) { + + // 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. + STORM_LOG_THROW(program.getNumberOfModules() == 1, storm::exceptions::WrongFormatException, "Cannot create abstract program from program containing too many modules."); + + // Add all variables and range expressions to the information object. + for (auto const& variable : this->program.get().getAllExpressionVariables()) { + abstractionInformation.addExpressionVariable(variable); + } + for (auto const& range : this->program.get().getAllRangeExpressions()) { + abstractionInformation.addConstraint(range); + initialStateAbstractor.constrain(range); + } + + uint_fast64_t totalNumberOfCommands = 0; + uint_fast64_t maximalUpdateCount = 0; + std::vector allGuards; + for (auto const& module : program.getModules()) { + // If we were requested to add all guards to the set of predicates, we do so now. + for (auto const& command : module.getCommands()) { + if (addAllGuards) { + allGuards.push_back(command.getGuardExpression()); + } + maximalUpdateCount = std::max(maximalUpdateCount, static_cast(command.getNumberOfUpdates())); + } + + totalNumberOfCommands += module.getNumberOfCommands(); + } + + // 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)))); + + // For each module of the concrete program, we create an abstract counterpart. + for (auto const& module : program.getModules()) { + this->modules.emplace_back(module, abstractionInformation, this->smtSolverFactory, addAllGuards); + } + + // Retrieve the command-update probability ADD, so we can multiply it with the abstraction BDD later. + commandUpdateProbabilitiesAdd = modules.front().getCommandUpdateProbabilitiesAdd(); + + // Now that we have created all other DD variables, we create the DD variables for the predicates. + std::vector initialPredicates; + if (addAllGuards) { + for (auto const& guard : allGuards) { + initialPredicates.push_back(guard); + } + } + + // Finally, refine using the all predicates and build game as a by-product. + this->refine(initialPredicates); } template - storm::abstraction::MenuGame PrismMenuGameAbstractor::abstract() { - return abstractProgram.abstract(); + void PrismMenuGameAbstractor::refine(std::vector const& predicates) { + // Add the predicates to the global list of predicates and gather their indices. + std::vector newPredicateIndices; + for (auto const& predicate : predicates) { + STORM_LOG_THROW(predicate.hasBooleanType(), storm::exceptions::InvalidArgumentException, "Expecting a predicate of type bool."); + newPredicateIndices.push_back(abstractionInformation.addPredicate(predicate)); + } + + // Refine all abstract modules. + for (auto& module : modules) { + module.refine(newPredicateIndices); + } + + // Refine initial state abstractor. + initialStateAbstractor.refine(newPredicateIndices); + + // Update the flag that stores whether a refinement was performed. + refinementPerformed = refinementPerformed || !newPredicateIndices.empty(); + } + + template + MenuGame PrismMenuGameAbstractor::abstract() { + if (refinementPerformed) { + currentGame = buildGame(); + refinementPerformed = true; + } + return *currentGame; } template AbstractionInformation const& PrismMenuGameAbstractor::getAbstractionInformation() const { - return abstractProgram.getAbstractionInformation(); + return abstractionInformation; } template storm::expressions::Expression const& PrismMenuGameAbstractor::getGuard(uint64_t player1Choice) const { - return abstractProgram.getGuard(player1Choice); + return modules.front().getGuard(player1Choice); } template std::map PrismMenuGameAbstractor::getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const { - return abstractProgram.getVariableUpdates(player1Choice, auxiliaryChoice); + return modules.front().getVariableUpdates(player1Choice, auxiliaryChoice); } template - void PrismMenuGameAbstractor::refine(std::vector const& predicates) { - abstractProgram.refine(predicates); + storm::dd::Bdd PrismMenuGameAbstractor::getStates(storm::expressions::Expression const& predicate) { + STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created."); + return abstractionInformation.getPredicateSourceVariable(predicate); } template - void PrismMenuGameAbstractor::exportToDot(std::string const& filename, storm::dd::Bdd const& highlightStates, storm::dd::Bdd const& filter) const { - abstractProgram.exportToDot(filename, highlightStates, filter); + std::unique_ptr> PrismMenuGameAbstractor::buildGame() { + // As long as there is only one module, we only build its game representation. + GameBddResult game = modules.front().abstract(); + + // Construct a set of all unnecessary variables, so we can abstract from it. + std::set variablesToAbstract(abstractionInformation.getPlayer1VariableSet(abstractionInformation.getPlayer1VariableCount())); + auto player2Variables = abstractionInformation.getPlayer2VariableSet(game.numberOfPlayer2Variables); + variablesToAbstract.insert(player2Variables.begin(), player2Variables.end()); + auto auxVariables = abstractionInformation.getAuxVariableSet(0, abstractionInformation.getAuxVariableCount()); + variablesToAbstract.insert(auxVariables.begin(), auxVariables.end()); + + // Do a reachability analysis on the raw transition relation. + storm::dd::Bdd transitionRelation = game.bdd.existsAbstract(variablesToAbstract); + storm::dd::Bdd initialStates = initialStateAbstractor.getAbstractStates(); + storm::dd::Bdd reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); + + // Find the deadlock states in the model. Note that this does not find the 'deadlocks' in bottom states, + // as the bottom states are not contained in the reachable states. + storm::dd::Bdd deadlockStates = transitionRelation.existsAbstract(abstractionInformation.getSuccessorVariables()); + deadlockStates = reachableStates && !deadlockStates; + + // 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, game.numberOfPlayer2Variables) && abstractionInformation.encodeAux(0, 0, abstractionInformation.getAuxVariableCount())).template toAdd(); + } + + // Compute bottom states and the appropriate transitions if necessary. + BottomStateResult bottomStateResult(abstractionInformation.getDdManager().getBddZero(), abstractionInformation.getDdManager().getBddZero()); + bool hasBottomStates = false; + if (!addedAllGuards) { + bottomStateResult = modules.front().getBottomStateTransitions(reachableStates, game.numberOfPlayer2Variables); + hasBottomStates = !bottomStateResult.states.isZero(); + } + + // Construct the transition matrix by cutting away the transitions of unreachable states. + storm::dd::Add transitionMatrix = (game.bdd && reachableStates).template toAdd(); + transitionMatrix *= commandUpdateProbabilitiesAdd; + transitionMatrix += deadlockTransitions; + + // Extend the current game information with the 'non-bottom' tag before potentially adding bottom state transitions. + transitionMatrix *= (abstractionInformation.getBottomStateBdd(true, true) && abstractionInformation.getBottomStateBdd(false, true)).template toAdd(); + reachableStates &= abstractionInformation.getBottomStateBdd(true, true); + initialStates &= abstractionInformation.getBottomStateBdd(true, true); + + // If there are bottom transitions, exnted the transition matrix and reachable states now. + if (hasBottomStates) { + transitionMatrix += bottomStateResult.transitions.template toAdd(); + reachableStates |= bottomStateResult.states; + } + + std::set usedPlayer2Variables(abstractionInformation.getPlayer2Variables().begin(), abstractionInformation.getPlayer2Variables().begin() + game.numberOfPlayer2Variables); + + std::set allNondeterminismVariables = usedPlayer2Variables; + allNondeterminismVariables.insert(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()); + + std::set allSourceVariables(abstractionInformation.getSourceVariables()); + allSourceVariables.insert(abstractionInformation.getBottomStateVariable(true)); + std::set allSuccessorVariables(abstractionInformation.getSuccessorVariables()); + allSuccessorVariables.insert(abstractionInformation.getBottomStateVariable(false)); + + return std::make_unique>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStateResult.states, allSourceVariables, allSuccessorVariables, abstractionInformation.getExtendedSourceSuccessorVariablePairs(), std::set(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), usedPlayer2Variables, allNondeterminismVariables, auxVariables, abstractionInformation.getPredicateToBddMap()); } - + + template + void PrismMenuGameAbstractor::exportToDot(std::string const& filename, storm::dd::Bdd const& highlightStatesBdd, storm::dd::Bdd const& filter) const { + std::ofstream out(filename); + + storm::dd::Add filteredTransitions = filter.template toAdd() * currentGame->getTransitionMatrix(); + storm::dd::Bdd filteredTransitionsBdd = filteredTransitions.toBdd().existsAbstract(currentGame->getNondeterminismVariables()); + storm::dd::Bdd filteredReachableStates = storm::utility::dd::computeReachableStates(currentGame->getInitialStates(), filteredTransitionsBdd, currentGame->getRowVariables(), currentGame->getColumnVariables()); + filteredTransitions *= filteredReachableStates.template toAdd(); + + // Determine all initial states so we can color them blue. + std::unordered_set initialStates; + storm::dd::Add initialStatesAsAdd = currentGame->getInitialStates().template toAdd(); + for (auto stateValue : initialStatesAsAdd) { + std::stringstream stateName; + for (auto const& var : currentGame->getRowVariables()) { + if (stateValue.first.getBooleanValue(var)) { + stateName << "1"; + } else { + stateName << "0"; + } + } + initialStates.insert(stateName.str()); + } + + // Determine all highlight states so we can color them red. + std::unordered_set highlightStates; + storm::dd::Add highlightStatesAdd = highlightStatesBdd.template toAdd(); + for (auto stateValue : highlightStatesAdd) { + std::stringstream stateName; + for (auto const& var : currentGame->getRowVariables()) { + if (stateValue.first.getBooleanValue(var)) { + stateName << "1"; + } else { + stateName << "0"; + } + } + highlightStates.insert(stateName.str()); + } + + out << "digraph game {" << std::endl; + + // Create the player 1 nodes. + storm::dd::Add statesAsAdd = filteredReachableStates.template toAdd(); + for (auto stateValue : statesAsAdd) { + out << "\tpl1_"; + std::stringstream stateName; + for (auto const& var : currentGame->getRowVariables()) { + if (stateValue.first.getBooleanValue(var)) { + stateName << "1"; + } else { + stateName << "0"; + } + } + std::string stateNameAsString = stateName.str(); + out << stateNameAsString; + out << " [ label=\""; + if (stateValue.first.getBooleanValue(abstractionInformation.getBottomStateVariable(true))) { + out << "*\", margin=0, width=0, height=0, shape=\"none\""; + } else { + out << stateName.str() << "\", margin=0, width=0, height=0, shape=\"oval\""; + } + bool isInitial = initialStates.find(stateNameAsString) != initialStates.end(); + bool isHighlight = highlightStates.find(stateNameAsString) != highlightStates.end(); + if (isInitial && isHighlight) { + out << ", style=\"filled\", fillcolor=\"yellow\""; + } else if (isInitial) { + out << ", style=\"filled\", fillcolor=\"blue\""; + } else if (isHighlight) { + out << ", style=\"filled\", fillcolor=\"red\""; + } + out << " ];" << std::endl; + } + + // Create the nodes of the second player. + storm::dd::Add player2States = filteredTransitions.toBdd().existsAbstract(currentGame->getColumnVariables()).existsAbstract(currentGame->getPlayer2Variables()).template toAdd(); + for (auto stateValue : player2States) { + out << "\tpl2_"; + std::stringstream stateName; + for (auto const& var : currentGame->getRowVariables()) { + if (stateValue.first.getBooleanValue(var)) { + stateName << "1"; + } else { + stateName << "0"; + } + } + uint_fast64_t index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount()); + out << stateName.str() << "_" << index; + out << " [ shape=\"square\", width=0, height=0, margin=0, label=\"" << index << "\" ];" << std::endl; + out << "\tpl1_" << stateName.str() << " -> " << "pl2_" << stateName.str() << "_" << index << " [ label=\"" << index << "\" ];" << std::endl; + } + + // Create the nodes of the probabilistic player. + storm::dd::Add playerPStates = filteredTransitions.toBdd().existsAbstract(currentGame->getColumnVariables()).template toAdd(); + for (auto stateValue : playerPStates) { + out << "\tplp_"; + std::stringstream stateName; + for (auto const& var : currentGame->getRowVariables()) { + if (stateValue.first.getBooleanValue(var)) { + stateName << "1"; + } else { + stateName << "0"; + } + } + uint_fast64_t index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount()); + stateName << "_" << index; + index = abstractionInformation.decodePlayer2Choice(stateValue.first, currentGame->getPlayer2Variables().size()); + out << stateName.str() << "_" << index; + out << " [ shape=\"point\", label=\"\" ];" << std::endl; + out << "\tpl2_" << stateName.str() << " -> " << "plp_" << stateName.str() << "_" << index << " [ label=\"" << index << "\" ];" << std::endl; + } + + for (auto stateValue : filteredTransitions) { + std::stringstream sourceStateName; + std::stringstream successorStateName; + for (auto const& var : currentGame->getRowVariables()) { + if (stateValue.first.getBooleanValue(var)) { + sourceStateName << "1"; + } else { + sourceStateName << "0"; + } + } + for (auto const& var : currentGame->getColumnVariables()) { + if (stateValue.first.getBooleanValue(var)) { + successorStateName << "1"; + } else { + successorStateName << "0"; + } + } + uint_fast64_t pl1Index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount()); + uint_fast64_t pl2Index = abstractionInformation.decodePlayer2Choice(stateValue.first, currentGame->getPlayer2Variables().size()); + out << "\tplp_" << sourceStateName.str() << "_" << pl1Index << "_" << pl2Index << " -> pl1_" << successorStateName.str() << " [ label=\"" << stateValue.second << "\"];" << std::endl; + } + + out << "}" << std::endl; + } + + // Explicitly instantiate the class. template class PrismMenuGameAbstractor; template class PrismMenuGameAbstractor; +#ifdef STORM_HAVE_CARL + template class PrismMenuGameAbstractor; +#endif } } } diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h index 9b856ba3d..9d64d3eac 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h @@ -1,33 +1,152 @@ #pragma once +#include "storm/storage/dd/DdType.h" + #include "storm/abstraction/MenuGameAbstractor.h" +#include "storm/abstraction/AbstractionInformation.h" +#include "storm/abstraction/MenuGame.h" +#include "storm/abstraction/prism/ModuleAbstractor.h" + +#include "storm/storage/dd/Add.h" -#include "storm/abstraction/prism/AbstractProgram.h" +#include "storm/storage/expressions/Expression.h" namespace storm { + namespace utility { + namespace solver { + class SmtSolverFactory; + } + } + + namespace models { + namespace symbolic { + template + class StochasticTwoPlayerGame; + } + } + + namespace prism { + // Forward-declare concrete Program class. + class Program; + } + namespace abstraction { namespace prism { template class PrismMenuGameAbstractor : public MenuGameAbstractor { public: - PrismMenuGameAbstractor(storm::prism::Program const& program, std::shared_ptr const& smtSolverFactory = std::make_shared()); + /*! + * Constructs an abstract program from the given program and the initial predicates. + * + * @param expressionManager The manager responsible for the expressions of the program. + * @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. + */ + PrismMenuGameAbstractor(storm::prism::Program const& program, std::shared_ptr const& smtSolverFactory = std::make_shared(), bool addAllGuards = false); - virtual storm::abstraction::MenuGame abstract() override; - - virtual AbstractionInformation const& getAbstractionInformation() const override; - virtual storm::expressions::Expression const& getGuard(uint64_t player1Choice) const override; - virtual std::map getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const override; - - virtual void refine(std::vector const& predicates) override; + PrismMenuGameAbstractor(PrismMenuGameAbstractor const&) = default; + PrismMenuGameAbstractor& operator=(PrismMenuGameAbstractor const&) = default; + PrismMenuGameAbstractor(PrismMenuGameAbstractor&&) = default; + PrismMenuGameAbstractor& operator=(PrismMenuGameAbstractor&&) = default; + + /*! + * Uses the current set of predicates to derive the abstract menu game in the form of an ADD. + * + * @return The abstract stochastic two player game. + */ + MenuGame abstract(); + + /*! + * Retrieves information about the abstraction. + * + * @return The abstraction information object. + */ + AbstractionInformation const& getAbstractionInformation() const; + + /*! + * Retrieves the guard predicate of the given player 1 choice. + * + * @param player1Choice The choice for which to retrieve the guard. + * @return The guard of the player 1 choice. + */ + storm::expressions::Expression const& getGuard(uint64_t player1Choice) const; + + /*! + * Retrieves a mapping from variables to expressions that define their updates wrt. to the given player + * 1 choice and auxiliary choice. + */ + std::map getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) 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. + * + * @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); + + /*! + * Refines the abstract program with the given predicates. + * + * @param predicates The new predicates. + */ + void refine(std::vector const& predicates); + + /*! + * Exports the current state of the abstraction in the dot format to the given file. + * + * @param filename The name of the file to which to write the dot output. + * @param highlightStates A BDD characterizing states that will be highlighted. + * @param filter A filter that is applied to select which part of the game to export. + */ + void exportToDot(std::string const& filename, storm::dd::Bdd const& highlightStates, storm::dd::Bdd const& filter) const; + + private: + /*! + * Builds the stochastic game representing the abstraction of the program. + * + * @return The stochastic game. + */ + std::unique_ptr> buildGame(); + + /*! + * Decodes the given choice over the auxiliary and successor variables to a mapping from update indices + * to bit vectors representing the successors under these updates. + * + * @param choice The choice to decode. + */ + std::map decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd const& choice) const; + + // The concrete program this abstract program refers to. + std::reference_wrapper program; - void exportToDot(std::string const& filename, storm::dd::Bdd const& highlightStates, storm::dd::Bdd const& filter) const override; + // A factory that can be used to create new SMT solvers. + std::shared_ptr smtSolverFactory; - private: - /// The abstract program that performs the actual abstraction. - AbstractProgram abstractProgram; + // 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; + + // 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; + + // An ADD characterizing the probabilities of commands and their updates. + storm::dd::Add commandUpdateProbabilitiesAdd; + + // The current game-based abstraction. + std::unique_ptr> currentGame; + + // A flag storing whether a refinement was performed. + bool refinementPerformed; }; - } } } diff --git a/src/test/abstraction/PrismMenuGameTest.cpp b/src/test/abstraction/PrismMenuGameTest.cpp index 76c91adc2..9c99941d0 100644 --- a/src/test/abstraction/PrismMenuGameTest.cpp +++ b/src/test/abstraction/PrismMenuGameTest.cpp @@ -5,7 +5,7 @@ #include "storm/parser/PrismParser.h" -#include "storm/abstraction/prism/AbstractProgram.h" +#include "storm/abstraction/prism/PrismMenuGameAbstractor.h" #include "storm/storage/expressions/Expression.h" @@ -26,9 +26,9 @@ TEST(PrismMenuGame, DieAbstractionTest_Cudd) { initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3)); - storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, initialPredicates, std::make_shared(), false); - storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractor.abstract(); EXPECT_EQ(26, game.getNumberOfTransitions()); EXPECT_EQ(4, game.getNumberOfStates()); @@ -43,9 +43,9 @@ TEST(PrismMenuGame, DieAbstractionTest_Sylvan) { initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3)); - storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, initialPredicates, std::make_shared(), false); - storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractor.abstract(); EXPECT_EQ(26, game.getNumberOfTransitions()); EXPECT_EQ(4, game.getNumberOfStates()); @@ -61,9 +61,9 @@ TEST(PrismMenuGame, DieAbstractionTest_SylvanWithRationalFunction) { initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3)); - storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, initialPredicates, std::make_shared(), false); - storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractor.abstract(); EXPECT_EQ(26, game.getNumberOfTransitions()); EXPECT_EQ(4, game.getNumberOfStates()); @@ -79,11 +79,11 @@ TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Cudd) { initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3)); - storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, initialPredicates, std::make_shared(), false); - ASSERT_NO_THROW(abstractProgram.refine({std::make_pair(manager.getVariableExpression("s") == manager.integer(7), true)})); + ASSERT_NO_THROW(abstractor.refine({std::make_pair(manager.getVariableExpression("s") == manager.integer(7), true)})); - storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractor.abstract(); EXPECT_EQ(24, game.getNumberOfTransitions()); EXPECT_EQ(5, game.getNumberOfStates()); @@ -98,11 +98,11 @@ TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Sylvan) { initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3)); - storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, initialPredicates, std::make_shared(), false); - ASSERT_NO_THROW(abstractProgram.refine({std::make_pair(manager.getVariableExpression("s") == manager.integer(7), true)})); + ASSERT_NO_THROW(abstractor.refine({std::make_pair(manager.getVariableExpression("s") == manager.integer(7), true)})); - storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractor.abstract(); EXPECT_EQ(24, game.getNumberOfTransitions()); EXPECT_EQ(5, game.getNumberOfStates()); @@ -132,9 +132,9 @@ TEST(PrismMenuGame, DieFullAbstractionTest_Cudd) { initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(5)); initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(6)); - storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, initialPredicates, std::make_shared(), false); - storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractor.abstract(); EXPECT_EQ(20, game.getNumberOfTransitions()); EXPECT_EQ(13, game.getNumberOfStates()); @@ -164,9 +164,9 @@ TEST(PrismMenuGame, DieFullAbstractionTest_Sylvan) { initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(5)); initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(6)); - storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, initialPredicates, std::make_shared(), false); - storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractor.abstract(); EXPECT_EQ(20, game.getNumberOfTransitions()); EXPECT_EQ(13, game.getNumberOfStates()); @@ -182,9 +182,9 @@ TEST(PrismMenuGame, CrowdsAbstractionTest_Cudd) { initialPredicates.push_back(manager.getVariableExpression("phase") < manager.integer(3)); - storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, initialPredicates, std::make_shared(), false); - storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractor.abstract(); EXPECT_EQ(31, game.getNumberOfTransitions()); EXPECT_EQ(4, game.getNumberOfStates()); @@ -200,9 +200,9 @@ TEST(PrismMenuGame, CrowdsAbstractionTest_Sylvan) { initialPredicates.push_back(manager.getVariableExpression("phase") < manager.integer(3)); - storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, initialPredicates, std::make_shared(), false); - storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractor.abstract(); EXPECT_EQ(31, game.getNumberOfTransitions()); EXPECT_EQ(4, game.getNumberOfStates()); @@ -218,11 +218,11 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Cudd) { initialPredicates.push_back(manager.getVariableExpression("phase") < manager.integer(3)); - storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, initialPredicates, std::make_shared(), false); - ASSERT_NO_THROW(abstractProgram.refine({std::make_pair(manager.getVariableExpression("observe0") + manager.getVariableExpression("observe1") + manager.getVariableExpression("observe2") + manager.getVariableExpression("observe3") + manager.getVariableExpression("observe4") <= manager.getVariableExpression("runCount"), true)})); + ASSERT_NO_THROW(abstractor.refine({std::make_pair(manager.getVariableExpression("observe0") + manager.getVariableExpression("observe1") + manager.getVariableExpression("observe2") + manager.getVariableExpression("observe3") + manager.getVariableExpression("observe4") <= manager.getVariableExpression("runCount"), true)})); - storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractor.abstract(); EXPECT_EQ(68, game.getNumberOfTransitions()); EXPECT_EQ(8, game.getNumberOfStates()); @@ -238,11 +238,11 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Sylvan) { initialPredicates.push_back(manager.getVariableExpression("phase") < manager.integer(3)); - storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, initialPredicates, std::make_shared(), false); - ASSERT_NO_THROW(abstractProgram.refine({std::make_pair(manager.getVariableExpression("observe0") + manager.getVariableExpression("observe1") + manager.getVariableExpression("observe2") + manager.getVariableExpression("observe3") + manager.getVariableExpression("observe4") <= manager.getVariableExpression("runCount"), true)})); + ASSERT_NO_THROW(abstractor.refine({std::make_pair(manager.getVariableExpression("observe0") + manager.getVariableExpression("observe1") + manager.getVariableExpression("observe2") + manager.getVariableExpression("observe3") + manager.getVariableExpression("observe4") <= manager.getVariableExpression("runCount"), true)})); - storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractor.abstract(); EXPECT_EQ(68, game.getNumberOfTransitions()); EXPECT_EQ(8, game.getNumberOfStates()); @@ -312,9 +312,9 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest_Cudd) { initialPredicates.push_back(manager.getVariableExpression("lastSeen") == manager.integer(3)); initialPredicates.push_back(manager.getVariableExpression("lastSeen") == manager.integer(4)); - storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, initialPredicates, std::make_shared(), false); - storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractor.abstract(); EXPECT_EQ(15113, game.getNumberOfTransitions()); EXPECT_EQ(8607, game.getNumberOfStates()); @@ -384,9 +384,9 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest_Sylvan) { initialPredicates.push_back(manager.getVariableExpression("lastSeen") == manager.integer(3)); initialPredicates.push_back(manager.getVariableExpression("lastSeen") == manager.integer(4)); - storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, initialPredicates, std::make_shared(), false); - storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractor.abstract(); EXPECT_EQ(15113, game.getNumberOfTransitions()); EXPECT_EQ(8607, game.getNumberOfStates()); @@ -404,9 +404,9 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest_Cudd) { initialPredicates.push_back(manager.getVariableExpression("s1") < manager.integer(3)); initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(0)); - storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, initialPredicates, std::make_shared(), false); - storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractor.abstract(); EXPECT_EQ(90, game.getNumberOfTransitions()); EXPECT_EQ(8, game.getNumberOfStates()); @@ -424,9 +424,9 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest_Sylvan) { initialPredicates.push_back(manager.getVariableExpression("s1") < manager.integer(3)); initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(0)); - storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, initialPredicates, std::make_shared(), false); - storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractor.abstract(); EXPECT_EQ(90, game.getNumberOfTransitions()); EXPECT_EQ(8, game.getNumberOfStates()); @@ -444,11 +444,11 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Cudd) { initialPredicates.push_back(manager.getVariableExpression("s1") < manager.integer(3)); initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(0)); - storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, initialPredicates, std::make_shared(), false); - ASSERT_NO_THROW(abstractProgram.refine({std::make_pair(manager.getVariableExpression("d1") + manager.getVariableExpression("d2") == manager.integer(7), true)})); + ASSERT_NO_THROW(abstractor.refine({std::make_pair(manager.getVariableExpression("d1") + manager.getVariableExpression("d2") == manager.integer(7), true)})); - storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractor.abstract(); EXPECT_EQ(276, game.getNumberOfTransitions()); EXPECT_EQ(16, game.getNumberOfStates()); @@ -466,11 +466,11 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Sylvan) { initialPredicates.push_back(manager.getVariableExpression("s1") < manager.integer(3)); initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(0)); - storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, initialPredicates, std::make_shared(), false); - ASSERT_NO_THROW(abstractProgram.refine({std::make_pair(manager.getVariableExpression("d1") + manager.getVariableExpression("d2") == manager.integer(7), true)})); + ASSERT_NO_THROW(abstractor.refine({std::make_pair(manager.getVariableExpression("d1") + manager.getVariableExpression("d2") == manager.integer(7), true)})); - storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractor.abstract(); EXPECT_EQ(276, game.getNumberOfTransitions()); EXPECT_EQ(16, game.getNumberOfStates()); @@ -519,9 +519,9 @@ TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Cudd) { initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(5)); initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(6)); - storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, initialPredicates, std::make_shared(), false); - storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractor.abstract(); EXPECT_EQ(436, game.getNumberOfTransitions()); EXPECT_EQ(169, game.getNumberOfStates()); @@ -570,9 +570,9 @@ TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Sylvan) { initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(5)); initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(6)); - storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, initialPredicates, std::make_shared(), false); - storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractor.abstract(); EXPECT_EQ(436, game.getNumberOfTransitions()); EXPECT_EQ(169, game.getNumberOfStates()); @@ -591,9 +591,9 @@ TEST(PrismMenuGame, WlanAbstractionTest_Cudd) { initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(0)); initialPredicates.push_back(manager.getVariableExpression("c1") == manager.getVariableExpression("c2")); - storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, initialPredicates, std::make_shared(), false); - storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractor.abstract(); EXPECT_EQ(1379, game.getNumberOfTransitions()); EXPECT_EQ(12, game.getNumberOfStates()); @@ -612,9 +612,9 @@ TEST(PrismMenuGame, WlanAbstractionTest_Sylvan) { initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(0)); initialPredicates.push_back(manager.getVariableExpression("c1") == manager.getVariableExpression("c2")); - storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, initialPredicates, std::make_shared(), false); - storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractor.abstract(); EXPECT_EQ(1379, game.getNumberOfTransitions()); EXPECT_EQ(12, game.getNumberOfStates()); @@ -633,11 +633,11 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Cudd) { initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(0)); initialPredicates.push_back(manager.getVariableExpression("c1") == manager.getVariableExpression("c2")); - storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, initialPredicates, std::make_shared(), false); - ASSERT_NO_THROW(abstractProgram.refine({std::make_pair(manager.getVariableExpression("backoff1") < manager.integer(7), true)})); + ASSERT_NO_THROW(abstractor.refine({std::make_pair(manager.getVariableExpression("backoff1") < manager.integer(7), true)})); - storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractor.abstract(); EXPECT_EQ(2744, game.getNumberOfTransitions()); EXPECT_EQ(24, game.getNumberOfStates()); @@ -656,11 +656,11 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Sylvan) { initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(0)); initialPredicates.push_back(manager.getVariableExpression("c1") == manager.getVariableExpression("c2")); - storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, initialPredicates, std::make_shared(), false); - ASSERT_NO_THROW(abstractProgram.refine({std::make_pair(manager.getVariableExpression("backoff1") < manager.integer(7), true)})); + ASSERT_NO_THROW(abstractor.refine({std::make_pair(manager.getVariableExpression("backoff1") < manager.integer(7), true)})); - storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractor.abstract(); EXPECT_EQ(2744, game.getNumberOfTransitions()); EXPECT_EQ(24, game.getNumberOfStates()); @@ -777,9 +777,9 @@ TEST(PrismMenuGame, WlanFullAbstractionTest_Cudd) { initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(0)); initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(1)); - storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, initialPredicates, std::make_shared(), false); - storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractor.abstract(); EXPECT_EQ(9503, game.getNumberOfTransitions()); EXPECT_EQ(5523, game.getNumberOfStates()); @@ -896,9 +896,9 @@ TEST(PrismMenuGame, WlanFullAbstractionTest_Sylvan) { initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(0)); initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(1)); - storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, initialPredicates, std::make_shared(), false); - storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractor.abstract(); EXPECT_EQ(9503, game.getNumberOfTransitions()); EXPECT_EQ(5523, game.getNumberOfStates()); diff --git a/src/test/utility/GraphTest.cpp b/src/test/utility/GraphTest.cpp index 3571e685e..14e7d1a71 100644 --- a/src/test/utility/GraphTest.cpp +++ b/src/test/utility/GraphTest.cpp @@ -202,7 +202,7 @@ TEST(GraphTest, SymbolicProb01MinMax_Sylvan) { #ifdef STORM_HAVE_MSAT -#include "src/abstraction/prism/AbstractProgram.h" +#include "src/abstraction/prism/PrismMenuGameAbstractor.h" #include "src/storage/expressions/Expression.h" @@ -216,9 +216,9 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3)); - storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, initialPredicates, std::make_shared(), false); - storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractor.abstract(); // The target states are those states where !(s < 3). storm::dd::Bdd targetStates = game.getStates(initialPredicates[0], true); @@ -251,8 +251,8 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { EXPECT_TRUE(result.hasPlayer1Strategy()); EXPECT_TRUE(result.hasPlayer2Strategy()); - abstractProgram.refine({manager.getVariableExpression("s") < manager.integer(2)}); - game = abstractProgram.getAbstractGame(); + abstractor.refine({manager.getVariableExpression("s") < manager.integer(2)}); + game = abstractor.abstract(); // We need to create a new BDD for the target states since the reachable states might have changed. targetStates = game.getStates(initialPredicates[0], true); @@ -352,9 +352,9 @@ TEST(GraphTest, SymbolicProb01StochasticGameTwoDice) { initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(5)); initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(6)); - storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, initialPredicates, std::make_shared(), false); - storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractor.abstract(); // The target states are those states where s1 == 7 & s2 == 7 & d1 + d2 == 1. storm::dd::Bdd targetStates = game.getStates(initialPredicates[7], false) && game.getStates(initialPredicates[22], false) && game.getStates(initialPredicates[9], false) && game.getStates(initialPredicates[24], false); @@ -521,9 +521,9 @@ TEST(GraphTest, SymbolicProb01StochasticGameWlan) { initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(0)); initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(1)); - storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, initialPredicates, std::make_shared(), false); - storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractor.abstract(); // The target states are those states where col == 2. storm::dd::Bdd targetStates = game.getStates(initialPredicates[2], false);