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 <storm::dd::DdType DdType, typename ValueType>
- AbstractProgram<DdType, ValueType>::AbstractProgram(storm::prism::Program const& program,
- std::shared_ptr<storm::utility::solver::SmtSolverFactory> 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<storm::expressions::Expression> 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<uint_fast64_t>(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<uint_fast64_t>(std::ceil(std::log2(totalNumberOfCommands))), 100, static_cast<uint_fast64_t>(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<storm::expressions::Expression> 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::dd::DdType DdType, typename ValueType>
- void AbstractProgram<DdType, ValueType>::refine(std::vector<storm::expressions::Expression> const& predicates) {
- // Add the predicates to the global list of predicates and gather their indices.
- std::vector<uint_fast64_t> 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 <storm::dd::DdType DdType, typename ValueType>
- MenuGame<DdType, ValueType> AbstractProgram<DdType, ValueType>::abstract() {
- if (refinementPerformed) {
- currentGame = buildGame();
- refinementPerformed = true;
- }
- return *currentGame;
- }
-
- template <storm::dd::DdType DdType, typename ValueType>
- AbstractionInformation<DdType> const& AbstractProgram<DdType, ValueType>::getAbstractionInformation() const {
- return abstractionInformation;
- }
-
- template <storm::dd::DdType DdType, typename ValueType>
- storm::expressions::Expression const& AbstractProgram<DdType, ValueType>::getGuard(uint64_t player1Choice) const {
- return modules.front().getGuard(player1Choice);
- }
-
- template <storm::dd::DdType DdType, typename ValueType>
- std::map<storm::expressions::Variable, storm::expressions::Expression> AbstractProgram<DdType, ValueType>::getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const {
- return modules.front().getVariableUpdates(player1Choice, auxiliaryChoice);
- }
-
- template <storm::dd::DdType DdType, typename ValueType>
- storm::dd::Bdd<DdType> AbstractProgram<DdType, ValueType>::getStates(storm::expressions::Expression const& predicate) {
- STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created.");
- return abstractionInformation.getPredicateSourceVariable(predicate);
- }
-
- template <storm::dd::DdType DdType, typename ValueType>
- std::unique_ptr<MenuGame<DdType, ValueType>> AbstractProgram<DdType, ValueType>::buildGame() {
- // As long as there is only one module, we only build its game representation.
- GameBddResult<DdType> game = modules.front().getAbstractBdd();
-
- // Construct a set of all unnecessary variables, so we can abstract from it.
- std::set<storm::expressions::Variable> 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<DdType> transitionRelation = game.bdd.existsAbstract(variablesToAbstract);
- storm::dd::Bdd<DdType> initialStates = initialStateAbstractor.getAbstractStates();
- storm::dd::Bdd<DdType> 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<DdType> deadlockStates = transitionRelation.existsAbstract(abstractionInformation.getSuccessorVariables());
- deadlockStates = reachableStates && !deadlockStates;
-
- // If there are deadlock states, we fix them now.
- storm::dd::Add<DdType, ValueType> deadlockTransitions = abstractionInformation.getDdManager().template getAddZero<ValueType>();
- 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<ValueType>();
- }
-
- // Compute bottom states and the appropriate transitions if necessary.
- BottomStateResult<DdType> 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<DdType, ValueType> transitionMatrix = (game.bdd && reachableStates).template toAdd<ValueType>();
- 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<ValueType>();
- 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<ValueType>();
- reachableStates |= bottomStateResult.states;
- }
-
- std::set<storm::expressions::Variable> usedPlayer2Variables(abstractionInformation.getPlayer2Variables().begin(), abstractionInformation.getPlayer2Variables().begin() + game.numberOfPlayer2Variables);
-
- std::set<storm::expressions::Variable> allNondeterminismVariables = usedPlayer2Variables;
- allNondeterminismVariables.insert(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end());
-
- std::set<storm::expressions::Variable> allSourceVariables(abstractionInformation.getSourceVariables());
- allSourceVariables.insert(abstractionInformation.getBottomStateVariable(true));
- std::set<storm::expressions::Variable> allSuccessorVariables(abstractionInformation.getSuccessorVariables());
- allSuccessorVariables.insert(abstractionInformation.getBottomStateVariable(false));
-
- return std::make_unique<MenuGame<DdType, ValueType>>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStateResult.states, allSourceVariables, allSuccessorVariables, abstractionInformation.getExtendedSourceSuccessorVariablePairs(), std::set<storm::expressions::Variable>(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), usedPlayer2Variables, allNondeterminismVariables, auxVariables, abstractionInformation.getPredicateToBddMap());
- }
-
- template <storm::dd::DdType DdType, typename ValueType>
- void AbstractProgram<DdType, ValueType>::exportToDot(std::string const& filename, storm::dd::Bdd<DdType> const& highlightStatesBdd, storm::dd::Bdd<DdType> const& filter) const {
- std::ofstream out(filename);
-
- storm::dd::Add<DdType, ValueType> filteredTransitions = filter.template toAdd<ValueType>() * currentGame->getTransitionMatrix();
- storm::dd::Bdd<DdType> filteredTransitionsBdd = filteredTransitions.toBdd().existsAbstract(currentGame->getNondeterminismVariables());
- storm::dd::Bdd<DdType> filteredReachableStates = storm::utility::dd::computeReachableStates(currentGame->getInitialStates(), filteredTransitionsBdd, currentGame->getRowVariables(), currentGame->getColumnVariables());
- filteredTransitions *= filteredReachableStates.template toAdd<ValueType>();
-
- // Determine all initial states so we can color them blue.
- std::unordered_set<std::string> initialStates;
- storm::dd::Add<DdType, ValueType> initialStatesAsAdd = currentGame->getInitialStates().template toAdd<ValueType>();
- 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<std::string> highlightStates;
- storm::dd::Add<DdType, ValueType> highlightStatesAdd = highlightStatesBdd.template toAdd<ValueType>();
- 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<DdType, ValueType> statesAsAdd = filteredReachableStates.template toAdd<ValueType>();
- 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<DdType, ValueType> player2States = filteredTransitions.toBdd().existsAbstract(currentGame->getColumnVariables()).existsAbstract(currentGame->getPlayer2Variables()).template toAdd<ValueType>();
- 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<DdType, ValueType> playerPStates = filteredTransitions.toBdd().existsAbstract(currentGame->getColumnVariables()).template toAdd<ValueType>();
- 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<storm::dd::DdType::CUDD, double>;
- template class AbstractProgram<storm::dd::DdType::Sylvan, double>;
-#ifdef STORM_HAVE_CARL
- template class AbstractProgram<storm::dd::DdType::Sylvan, storm::RationalFunction>;
-#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<storm::dd::DdType Type, typename ValueType>
- class StochasticTwoPlayerGame;
- }
- }
-
- namespace prism {
- // Forward-declare concrete Program class.
- class Program;
- }
-
- namespace abstraction {
- namespace prism {
-
- template <storm::dd::DdType DdType, typename ValueType>
- 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<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), 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<DdType, ValueType> abstract();
-
- /*!
- * Retrieves information about the abstraction.
- *
- * @return The abstraction information object.
- */
- AbstractionInformation<DdType> 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<storm::expressions::Variable, storm::expressions::Expression> 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<DdType> getStates(storm::expressions::Expression const& predicate);
-
- /*!
- * Refines the abstract program with the given predicates.
- *
- * @param predicates The new predicates.
- */
- void refine(std::vector<storm::expressions::Expression> 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<DdType> const& highlightStates, storm::dd::Bdd<DdType> const& filter) const;
-
- private:
- /*!
- * Builds the stochastic game representing the abstraction of the program.
- *
- * @return The stochastic game.
- */
- std::unique_ptr<MenuGame<DdType, ValueType>> 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<uint_fast64_t, storm::storage::BitVector> decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd<DdType> const& choice) const;
-
- // The concrete program this abstract program refers to.
- std::reference_wrapper<storm::prism::Program const> program;
-
- // A factory that can be used to create new SMT solvers.
- std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory;
-
- // An object containing all information about the abstraction like predicates and the corresponding DDs.
- AbstractionInformation<DdType> abstractionInformation;
-
- // The abstract modules of the abstract program.
- std::vector<AbstractModule<DdType, ValueType>> modules;
-
- // A state-set abstractor used to determine the initial states of the abstraction.
- StateSetAbstractor<DdType, ValueType> 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<DdType, ValueType> commandUpdateProbabilitiesAdd;
-
- // The current game-based abstraction.
- std::unique_ptr<MenuGame<DdType, ValueType>> 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 <chrono>
@@ -23,7 +23,7 @@ namespace storm {
namespace abstraction {
namespace prism {
template <storm::dd::DdType DdType, typename ValueType>
- AbstractCommand<DdType, ValueType>::AbstractCommand(storm::prism::Command const& command, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> 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<DdType, ValueType>::CommandAbstractor(storm::prism::Command const& command, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> 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 <storm::dd::DdType DdType, typename ValueType>
- void AbstractCommand<DdType, ValueType>::refine(std::vector<uint_fast64_t> const& predicates) {
+ void CommandAbstractor<DdType, ValueType>::refine(std::vector<uint_fast64_t> 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::dd::DdType DdType, typename ValueType>
- storm::expressions::Expression const& AbstractCommand<DdType, ValueType>::getGuard() const {
+ storm::expressions::Expression const& CommandAbstractor<DdType, ValueType>::getGuard() const {
return command.get().getGuardExpression();
}
template <storm::dd::DdType DdType, typename ValueType>
- std::map<storm::expressions::Variable, storm::expressions::Expression> AbstractCommand<DdType, ValueType>::getVariableUpdates(uint64_t auxiliaryChoice) const {
+ std::map<storm::expressions::Variable, storm::expressions::Expression> CommandAbstractor<DdType, ValueType>::getVariableUpdates(uint64_t auxiliaryChoice) const {
return command.get().getUpdate(auxiliaryChoice).getAsVariableToExpressionMap();
}
template <storm::dd::DdType DdType, typename ValueType>
- void AbstractCommand<DdType, ValueType>::recomputeCachedBdd() {
+ void CommandAbstractor<DdType, ValueType>::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 <storm::dd::DdType DdType, typename ValueType>
- std::pair<std::set<uint_fast64_t>, std::set<uint_fast64_t>> AbstractCommand<DdType, ValueType>::computeRelevantPredicates(std::vector<storm::prism::Assignment> const& assignments) const {
+ std::pair<std::set<uint_fast64_t>, std::set<uint_fast64_t>> CommandAbstractor<DdType, ValueType>::computeRelevantPredicates(std::vector<storm::prism::Assignment> const& assignments) const {
std::pair<std::set<uint_fast64_t>, std::set<uint_fast64_t>> result;
std::set<storm::expressions::Variable> assignedVariables;
@@ -162,7 +162,7 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename ValueType>
- std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> AbstractCommand<DdType, ValueType>::computeRelevantPredicates() const {
+ std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> CommandAbstractor<DdType, ValueType>::computeRelevantPredicates() const {
std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> result;
// To start with, all predicates related to the guard are relevant source predicates.
@@ -179,7 +179,7 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename ValueType>
- bool AbstractCommand<DdType, ValueType>::relevantPredicatesChanged(std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> const& newRelevantPredicates) const {
+ bool CommandAbstractor<DdType, ValueType>::relevantPredicatesChanged(std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> const& newRelevantPredicates) const {
if (newRelevantPredicates.first.size() > relevantPredicatesAndVariables.first.size()) {
return true;
}
@@ -194,7 +194,7 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename ValueType>
- void AbstractCommand<DdType, ValueType>::addMissingPredicates(std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> const& newRelevantPredicates) {
+ void CommandAbstractor<DdType, ValueType>::addMissingPredicates(std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> const& newRelevantPredicates) {
// Determine and add new relevant source predicates.
std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newSourceVariables = this->getAbstractionInformation().declareNewVariables(relevantPredicatesAndVariables.first, newRelevantPredicates.first);
for (auto const& element : newSourceVariables) {
@@ -220,7 +220,7 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename ValueType>
- storm::dd::Bdd<DdType> AbstractCommand<DdType, ValueType>::getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model) const {
+ storm::dd::Bdd<DdType> CommandAbstractor<DdType, ValueType>::getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model) const {
storm::dd::Bdd<DdType> 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::DdType DdType, typename ValueType>
- storm::dd::Bdd<DdType> AbstractCommand<DdType, ValueType>::getDistributionBdd(storm::solver::SmtSolver::ModelReference const& model) const {
+ storm::dd::Bdd<DdType> CommandAbstractor<DdType, ValueType>::getDistributionBdd(storm::solver::SmtSolver::ModelReference const& model) const {
storm::dd::Bdd<DdType> 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::DdType DdType, typename ValueType>
- storm::dd::Bdd<DdType> AbstractCommand<DdType, ValueType>::computeMissingIdentities() const {
+ storm::dd::Bdd<DdType> CommandAbstractor<DdType, ValueType>::computeMissingIdentities() const {
storm::dd::Bdd<DdType> identities = computeMissingGlobalIdentities();
identities &= computeMissingUpdateIdentities();
return identities;
}
template <storm::dd::DdType DdType, typename ValueType>
- storm::dd::Bdd<DdType> AbstractCommand<DdType, ValueType>::computeMissingUpdateIdentities() const {
+ storm::dd::Bdd<DdType> CommandAbstractor<DdType, ValueType>::computeMissingUpdateIdentities() const {
storm::dd::Bdd<DdType> 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::DdType DdType, typename ValueType>
- storm::dd::Bdd<DdType> AbstractCommand<DdType, ValueType>::computeMissingGlobalIdentities() const {
+ storm::dd::Bdd<DdType> CommandAbstractor<DdType, ValueType>::computeMissingGlobalIdentities() const {
auto relevantIt = relevantPredicatesAndVariables.first.begin();
auto relevantIte = relevantPredicatesAndVariables.first.end();
@@ -309,7 +309,7 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename ValueType>
- GameBddResult<DdType> AbstractCommand<DdType, ValueType>::getAbstractBdd() {
+ GameBddResult<DdType> CommandAbstractor<DdType, ValueType>::abstract() {
if (forceRecomputation) {
this->recomputeCachedBdd();
} else {
@@ -320,7 +320,7 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename ValueType>
- BottomStateResult<DdType> AbstractCommand<DdType, ValueType>::getBottomStateTransitions(storm::dd::Bdd<DdType> const& reachableStates, uint_fast64_t numberOfPlayer2Variables) {
+ BottomStateResult<DdType> CommandAbstractor<DdType, ValueType>::getBottomStateTransitions(storm::dd::Bdd<DdType> const& reachableStates, uint_fast64_t numberOfPlayer2Variables) {
STORM_LOG_TRACE("Computing bottom state transitions of command " << command.get());
BottomStateResult<DdType> result(this->getAbstractionInformation().getDdManager().getBddZero(), this->getAbstractionInformation().getDdManager().getBddZero());
@@ -353,7 +353,7 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename ValueType>
- storm::dd::Add<DdType, ValueType> AbstractCommand<DdType, ValueType>::getCommandUpdateProbabilitiesAdd() const {
+ storm::dd::Add<DdType, ValueType> CommandAbstractor<DdType, ValueType>::getCommandUpdateProbabilitiesAdd() const {
storm::dd::Add<DdType, ValueType> result = this->getAbstractionInformation().getDdManager().template getAddZero<ValueType>();
for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) {
result += this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()).template toAdd<ValueType>() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(command.get().getUpdate(updateIndex).getLikelihoodExpression()));
@@ -363,24 +363,24 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename ValueType>
- storm::prism::Command const& AbstractCommand<DdType, ValueType>::getConcreteCommand() const {
+ storm::prism::Command const& CommandAbstractor<DdType, ValueType>::getConcreteCommand() const {
return command.get();
}
template <storm::dd::DdType DdType, typename ValueType>
- AbstractionInformation<DdType> const& AbstractCommand<DdType, ValueType>::getAbstractionInformation() const {
+ AbstractionInformation<DdType> const& CommandAbstractor<DdType, ValueType>::getAbstractionInformation() const {
return abstractionInformation.get();
}
template <storm::dd::DdType DdType, typename ValueType>
- AbstractionInformation<DdType>& AbstractCommand<DdType, ValueType>::getAbstractionInformation() {
+ AbstractionInformation<DdType>& CommandAbstractor<DdType, ValueType>::getAbstractionInformation() {
return abstractionInformation.get();
}
- template class AbstractCommand<storm::dd::DdType::CUDD, double>;
- template class AbstractCommand<storm::dd::DdType::Sylvan, double>;
+ template class CommandAbstractor<storm::dd::DdType::CUDD, double>;
+ template class CommandAbstractor<storm::dd::DdType::Sylvan, double>;
#ifdef STORM_HAVE_CARL
- template class AbstractCommand<storm::dd::DdType::Sylvan, storm::RationalFunction>;
+ template class CommandAbstractor<storm::dd::DdType::Sylvan, storm::RationalFunction>;
#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 <storm::dd::DdType DdType, typename ValueType>
- 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<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool guardIsPredicate = false);
+ CommandAbstractor(storm::prism::Command const& command, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> 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<DdType> getAbstractBdd();
+ GameBddResult<DdType> 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 <storm::dd::DdType DdType, typename ValueType>
- AbstractModule<DdType, ValueType>::AbstractModule(storm::prism::Module const& module, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool allGuardsAdded) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), commands(), module(module) {
+ ModuleAbstractor<DdType, ValueType>::ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> 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 <storm::dd::DdType DdType, typename ValueType>
- void AbstractModule<DdType, ValueType>::refine(std::vector<uint_fast64_t> const& predicates) {
+ void ModuleAbstractor<DdType, ValueType>::refine(std::vector<uint_fast64_t> const& predicates) {
for (uint_fast64_t index = 0; index < commands.size(); ++index) {
STORM_LOG_TRACE("Refining command with index " << index << ".");
- AbstractCommand<DdType, ValueType>& command = commands[index];
+ CommandAbstractor<DdType, ValueType>& command = commands[index];
command.refine(predicates);
}
}
template <storm::dd::DdType DdType, typename ValueType>
- storm::expressions::Expression const& AbstractModule<DdType, ValueType>::getGuard(uint64_t player1Choice) const {
+ storm::expressions::Expression const& ModuleAbstractor<DdType, ValueType>::getGuard(uint64_t player1Choice) const {
return commands[player1Choice].getGuard();
}
template <storm::dd::DdType DdType, typename ValueType>
- std::map<storm::expressions::Variable, storm::expressions::Expression> AbstractModule<DdType, ValueType>::getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const {
+ std::map<storm::expressions::Variable, storm::expressions::Expression> ModuleAbstractor<DdType, ValueType>::getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const {
return commands[player1Choice].getVariableUpdates(auxiliaryChoice);
}
template <storm::dd::DdType DdType, typename ValueType>
- GameBddResult<DdType> AbstractModule<DdType, ValueType>::getAbstractBdd() {
+ GameBddResult<DdType> ModuleAbstractor<DdType, ValueType>::abstract() {
// First, we retrieve the abstractions of all commands.
std::vector<GameBddResult<DdType>> 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 <storm::dd::DdType DdType, typename ValueType>
- BottomStateResult<DdType> AbstractModule<DdType, ValueType>::getBottomStateTransitions(storm::dd::Bdd<DdType> const& reachableStates, uint_fast64_t numberOfPlayer2Variables) {
+ BottomStateResult<DdType> ModuleAbstractor<DdType, ValueType>::getBottomStateTransitions(storm::dd::Bdd<DdType> const& reachableStates, uint_fast64_t numberOfPlayer2Variables) {
BottomStateResult<DdType> result(this->getAbstractionInformation().getDdManager().getBddZero(), this->getAbstractionInformation().getDdManager().getBddZero());
for (auto& command : commands) {
@@ -79,7 +79,7 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename ValueType>
- storm::dd::Add<DdType, ValueType> AbstractModule<DdType, ValueType>::getCommandUpdateProbabilitiesAdd() const {
+ storm::dd::Add<DdType, ValueType> ModuleAbstractor<DdType, ValueType>::getCommandUpdateProbabilitiesAdd() const {
storm::dd::Add<DdType, ValueType> result = this->getAbstractionInformation().getDdManager().template getAddZero<ValueType>();
for (auto const& command : commands) {
result += command.getCommandUpdateProbabilitiesAdd();
@@ -88,24 +88,24 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename ValueType>
- std::vector<AbstractCommand<DdType, ValueType>> const& AbstractModule<DdType, ValueType>::getCommands() const {
+ std::vector<CommandAbstractor<DdType, ValueType>> const& ModuleAbstractor<DdType, ValueType>::getCommands() const {
return commands;
}
template <storm::dd::DdType DdType, typename ValueType>
- std::vector<AbstractCommand<DdType, ValueType>>& AbstractModule<DdType, ValueType>::getCommands() {
+ std::vector<CommandAbstractor<DdType, ValueType>>& ModuleAbstractor<DdType, ValueType>::getCommands() {
return commands;
}
template <storm::dd::DdType DdType, typename ValueType>
- AbstractionInformation<DdType> const& AbstractModule<DdType, ValueType>::getAbstractionInformation() const {
+ AbstractionInformation<DdType> const& ModuleAbstractor<DdType, ValueType>::getAbstractionInformation() const {
return abstractionInformation.get();
}
- template class AbstractModule<storm::dd::DdType::CUDD, double>;
- template class AbstractModule<storm::dd::DdType::Sylvan, double>;
+ template class ModuleAbstractor<storm::dd::DdType::CUDD, double>;
+ template class ModuleAbstractor<storm::dd::DdType::Sylvan, double>;
#ifdef STORM_HAVE_CARL
- template class AbstractModule<storm::dd::DdType::Sylvan, storm::RationalFunction>;
+ template class ModuleAbstractor<storm::dd::DdType::Sylvan, storm::RationalFunction>;
#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 <storm::dd::DdType DdType, typename ValueType>
- 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<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), bool allGuardsAdded = false);
+ ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), 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<DdType> getAbstractBdd();
+ GameBddResult<DdType> abstract();
/*!
* Retrieves the transitions to bottom states of this module.
@@ -92,14 +92,14 @@ namespace storm {
*
* @return The abstract commands.
*/
- std::vector<AbstractCommand<DdType, ValueType>> const& getCommands() const;
+ std::vector<CommandAbstractor<DdType, ValueType>> const& getCommands() const;
/*!
* Retrieves the abstract commands of this abstract module.
*
* @return The abstract commands.
*/
- std::vector<AbstractCommand<DdType, ValueType>>& getCommands();
+ std::vector<CommandAbstractor<DdType, ValueType>>& getCommands();
private:
/*!
@@ -116,7 +116,7 @@ namespace storm {
std::reference_wrapper<AbstractionInformation<DdType> const> abstractionInformation;
// The abstract commands of the abstract module.
- std::vector<AbstractCommand<DdType, ValueType>> commands;
+ std::vector<CommandAbstractor<DdType, ValueType>> commands;
// The concrete module this abstract module refers to.
std::reference_wrapper<storm::prism::Module const> 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 <storm::dd::DdType DdType, typename ValueType>
- PrismMenuGameAbstractor<DdType, ValueType>::PrismMenuGameAbstractor(storm::prism::Program const& program, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : abstractProgram(program, smtSolverFactory, storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isAddAllGuardsSet()) {
- // Intentionally left empty.
+ PrismMenuGameAbstractor<DdType, ValueType>::PrismMenuGameAbstractor(storm::prism::Program const& program,
+ std::shared_ptr<storm::utility::solver::SmtSolverFactory> 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<storm::expressions::Expression> 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<uint_fast64_t>(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<uint_fast64_t>(std::ceil(std::log2(totalNumberOfCommands))), 100, static_cast<uint_fast64_t>(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<storm::expressions::Expression> 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::dd::DdType DdType, typename ValueType>
- storm::abstraction::MenuGame<DdType, ValueType> PrismMenuGameAbstractor<DdType, ValueType>::abstract() {
- return abstractProgram.abstract();
+ void PrismMenuGameAbstractor<DdType, ValueType>::refine(std::vector<storm::expressions::Expression> const& predicates) {
+ // Add the predicates to the global list of predicates and gather their indices.
+ std::vector<uint_fast64_t> 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 <storm::dd::DdType DdType, typename ValueType>
+ MenuGame<DdType, ValueType> PrismMenuGameAbstractor<DdType, ValueType>::abstract() {
+ if (refinementPerformed) {
+ currentGame = buildGame();
+ refinementPerformed = true;
+ }
+ return *currentGame;
}
template <storm::dd::DdType DdType, typename ValueType>
AbstractionInformation<DdType> const& PrismMenuGameAbstractor<DdType, ValueType>::getAbstractionInformation() const {
- return abstractProgram.getAbstractionInformation();
+ return abstractionInformation;
}
template <storm::dd::DdType DdType, typename ValueType>
storm::expressions::Expression const& PrismMenuGameAbstractor<DdType, ValueType>::getGuard(uint64_t player1Choice) const {
- return abstractProgram.getGuard(player1Choice);
+ return modules.front().getGuard(player1Choice);
}
template <storm::dd::DdType DdType, typename ValueType>
std::map<storm::expressions::Variable, storm::expressions::Expression> PrismMenuGameAbstractor<DdType, ValueType>::getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const {
- return abstractProgram.getVariableUpdates(player1Choice, auxiliaryChoice);
+ return modules.front().getVariableUpdates(player1Choice, auxiliaryChoice);
}
template <storm::dd::DdType DdType, typename ValueType>
- void PrismMenuGameAbstractor<DdType, ValueType>::refine(std::vector<storm::expressions::Expression> const& predicates) {
- abstractProgram.refine(predicates);
+ storm::dd::Bdd<DdType> PrismMenuGameAbstractor<DdType, ValueType>::getStates(storm::expressions::Expression const& predicate) {
+ STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created.");
+ return abstractionInformation.getPredicateSourceVariable(predicate);
}
template <storm::dd::DdType DdType, typename ValueType>
- void PrismMenuGameAbstractor<DdType, ValueType>::exportToDot(std::string const& filename, storm::dd::Bdd<DdType> const& highlightStates, storm::dd::Bdd<DdType> const& filter) const {
- abstractProgram.exportToDot(filename, highlightStates, filter);
+ std::unique_ptr<MenuGame<DdType, ValueType>> PrismMenuGameAbstractor<DdType, ValueType>::buildGame() {
+ // As long as there is only one module, we only build its game representation.
+ GameBddResult<DdType> game = modules.front().abstract();
+
+ // Construct a set of all unnecessary variables, so we can abstract from it.
+ std::set<storm::expressions::Variable> 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<DdType> transitionRelation = game.bdd.existsAbstract(variablesToAbstract);
+ storm::dd::Bdd<DdType> initialStates = initialStateAbstractor.getAbstractStates();
+ storm::dd::Bdd<DdType> 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<DdType> deadlockStates = transitionRelation.existsAbstract(abstractionInformation.getSuccessorVariables());
+ deadlockStates = reachableStates && !deadlockStates;
+
+ // If there are deadlock states, we fix them now.
+ storm::dd::Add<DdType, ValueType> deadlockTransitions = abstractionInformation.getDdManager().template getAddZero<ValueType>();
+ 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<ValueType>();
+ }
+
+ // Compute bottom states and the appropriate transitions if necessary.
+ BottomStateResult<DdType> 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<DdType, ValueType> transitionMatrix = (game.bdd && reachableStates).template toAdd<ValueType>();
+ 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<ValueType>();
+ 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<ValueType>();
+ reachableStates |= bottomStateResult.states;
+ }
+
+ std::set<storm::expressions::Variable> usedPlayer2Variables(abstractionInformation.getPlayer2Variables().begin(), abstractionInformation.getPlayer2Variables().begin() + game.numberOfPlayer2Variables);
+
+ std::set<storm::expressions::Variable> allNondeterminismVariables = usedPlayer2Variables;
+ allNondeterminismVariables.insert(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end());
+
+ std::set<storm::expressions::Variable> allSourceVariables(abstractionInformation.getSourceVariables());
+ allSourceVariables.insert(abstractionInformation.getBottomStateVariable(true));
+ std::set<storm::expressions::Variable> allSuccessorVariables(abstractionInformation.getSuccessorVariables());
+ allSuccessorVariables.insert(abstractionInformation.getBottomStateVariable(false));
+
+ return std::make_unique<MenuGame<DdType, ValueType>>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStateResult.states, allSourceVariables, allSuccessorVariables, abstractionInformation.getExtendedSourceSuccessorVariablePairs(), std::set<storm::expressions::Variable>(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), usedPlayer2Variables, allNondeterminismVariables, auxVariables, abstractionInformation.getPredicateToBddMap());
}
-
+
+ template <storm::dd::DdType DdType, typename ValueType>
+ void PrismMenuGameAbstractor<DdType, ValueType>::exportToDot(std::string const& filename, storm::dd::Bdd<DdType> const& highlightStatesBdd, storm::dd::Bdd<DdType> const& filter) const {
+ std::ofstream out(filename);
+
+ storm::dd::Add<DdType, ValueType> filteredTransitions = filter.template toAdd<ValueType>() * currentGame->getTransitionMatrix();
+ storm::dd::Bdd<DdType> filteredTransitionsBdd = filteredTransitions.toBdd().existsAbstract(currentGame->getNondeterminismVariables());
+ storm::dd::Bdd<DdType> filteredReachableStates = storm::utility::dd::computeReachableStates(currentGame->getInitialStates(), filteredTransitionsBdd, currentGame->getRowVariables(), currentGame->getColumnVariables());
+ filteredTransitions *= filteredReachableStates.template toAdd<ValueType>();
+
+ // Determine all initial states so we can color them blue.
+ std::unordered_set<std::string> initialStates;
+ storm::dd::Add<DdType, ValueType> initialStatesAsAdd = currentGame->getInitialStates().template toAdd<ValueType>();
+ 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<std::string> highlightStates;
+ storm::dd::Add<DdType, ValueType> highlightStatesAdd = highlightStatesBdd.template toAdd<ValueType>();
+ 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<DdType, ValueType> statesAsAdd = filteredReachableStates.template toAdd<ValueType>();
+ 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<DdType, ValueType> player2States = filteredTransitions.toBdd().existsAbstract(currentGame->getColumnVariables()).existsAbstract(currentGame->getPlayer2Variables()).template toAdd<ValueType>();
+ 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<DdType, ValueType> playerPStates = filteredTransitions.toBdd().existsAbstract(currentGame->getColumnVariables()).template toAdd<ValueType>();
+ 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<storm::dd::DdType::CUDD, double>;
template class PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double>;
+#ifdef STORM_HAVE_CARL
+ template class PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, storm::RationalFunction>;
+#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<storm::dd::DdType Type, typename ValueType>
+ class StochasticTwoPlayerGame;
+ }
+ }
+
+ namespace prism {
+ // Forward-declare concrete Program class.
+ class Program;
+ }
+
namespace abstraction {
namespace prism {
template <storm::dd::DdType DdType, typename ValueType>
class PrismMenuGameAbstractor : public MenuGameAbstractor<DdType, ValueType> {
public:
- PrismMenuGameAbstractor(storm::prism::Program const& program, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
+ /*!
+ * 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<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), bool addAllGuards = false);
- virtual storm::abstraction::MenuGame<DdType, ValueType> abstract() override;
-
- virtual AbstractionInformation<DdType> const& getAbstractionInformation() const override;
- virtual storm::expressions::Expression const& getGuard(uint64_t player1Choice) const override;
- virtual std::map<storm::expressions::Variable, storm::expressions::Expression> getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const override;
-
- virtual void refine(std::vector<storm::expressions::Expression> 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<DdType, ValueType> abstract();
+
+ /*!
+ * Retrieves information about the abstraction.
+ *
+ * @return The abstraction information object.
+ */
+ AbstractionInformation<DdType> 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<storm::expressions::Variable, storm::expressions::Expression> 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<DdType> getStates(storm::expressions::Expression const& predicate);
+
+ /*!
+ * Refines the abstract program with the given predicates.
+ *
+ * @param predicates The new predicates.
+ */
+ void refine(std::vector<storm::expressions::Expression> 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<DdType> const& highlightStates, storm::dd::Bdd<DdType> const& filter) const;
+
+ private:
+ /*!
+ * Builds the stochastic game representing the abstraction of the program.
+ *
+ * @return The stochastic game.
+ */
+ std::unique_ptr<MenuGame<DdType, ValueType>> 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<uint_fast64_t, storm::storage::BitVector> decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd<DdType> const& choice) const;
+
+ // The concrete program this abstract program refers to.
+ std::reference_wrapper<storm::prism::Program const> program;
- void exportToDot(std::string const& filename, storm::dd::Bdd<DdType> const& highlightStates, storm::dd::Bdd<DdType> const& filter) const override;
+ // A factory that can be used to create new SMT solvers.
+ std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory;
- private:
- /// The abstract program that performs the actual abstraction.
- AbstractProgram<DdType, ValueType> abstractProgram;
+ // An object containing all information about the abstraction like predicates and the corresponding DDs.
+ AbstractionInformation<DdType> abstractionInformation;
+
+ // The abstract modules of the abstract program.
+ std::vector<ModuleAbstractor<DdType, ValueType>> modules;
+
+ // A state-set abstractor used to determine the initial states of the abstraction.
+ StateSetAbstractor<DdType, ValueType> 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<DdType, ValueType> commandUpdateProbabilitiesAdd;
+
+ // The current game-based abstraction.
+ std::unique_ptr<MenuGame<DdType, ValueType>> 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<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+ storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
- storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
+ storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> 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<storm::dd::DdType::Sylvan, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+ storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
- storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
+ storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> 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<storm::dd::DdType::Sylvan, storm::RationalFunction> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+ storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, storm::RationalFunction> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
- storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, storm::RationalFunction> game = abstractProgram.getAbstractGame();
+ storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, storm::RationalFunction> 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<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+ storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), 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<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
+ storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> 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<storm::dd::DdType::Sylvan, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+ storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), 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<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
+ storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> 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<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+ storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
- storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
+ storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> 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<storm::dd::DdType::Sylvan, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+ storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
- storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
+ storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> 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<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+ storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
- storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
+ storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> 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<storm::dd::DdType::Sylvan, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+ storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
- storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
+ storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> 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<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+ storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), 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<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
+ storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> 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<storm::dd::DdType::Sylvan, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+ storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), 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<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
+ storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> 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<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+ storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
- storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
+ storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> 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<storm::dd::DdType::Sylvan, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+ storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
- storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
+ storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> 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<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+ storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
- storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
+ storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> 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<storm::dd::DdType::Sylvan, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+ storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
- storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
+ storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> 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<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+ storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), 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<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
+ storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> 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<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+ storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), 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<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
+ storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> 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<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+ storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
- storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
+ storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> 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<storm::dd::DdType::Sylvan, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+ storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
- storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
+ storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> 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<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+ storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
- storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
+ storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> 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<storm::dd::DdType::Sylvan, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+ storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
- storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
+ storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> 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<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+ storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), 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<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
+ storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> 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<storm::dd::DdType::Sylvan, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+ storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), 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<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
+ storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> 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<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+ storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
- storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
+ storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> 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<storm::dd::DdType::Sylvan, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+ storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
- storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
+ storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> 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<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+ storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
- storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
+ storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractor.abstract();
// The target states are those states where !(s < 3).
storm::dd::Bdd<storm::dd::DdType::CUDD> 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<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+ storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
- storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
+ storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractor.abstract();
// The target states are those states where s1 == 7 & s2 == 7 & d1 + d2 == 1.
storm::dd::Bdd<storm::dd::DdType::CUDD> 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<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+ storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
- storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
+ storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractor.abstract();
// The target states are those states where col == 2.
storm::dd::Bdd<storm::dd::DdType::CUDD> targetStates = game.getStates(initialPredicates[2], false);