diff --git a/src/storm/abstraction/jani/AutomatonAbstractor.cpp b/src/storm/abstraction/jani/AutomatonAbstractor.cpp index 32e53cf7f..4f4098d92 100644 --- a/src/storm/abstraction/jani/AutomatonAbstractor.cpp +++ b/src/storm/abstraction/jani/AutomatonAbstractor.cpp @@ -1,8 +1,8 @@ #include "storm/abstraction/jani/AutomatonAbstractor.h" -#include "storm/abstraction/AbstractionInformation.h" #include "storm/abstraction/BottomStateResult.h" #include "storm/abstraction/GameBddResult.h" +#include "storm/abstraction/jani/JaniAbstractionInformation.h" #include "storm/storage/dd/DdManager.h" #include "storm/storage/dd/Add.h" @@ -23,7 +23,7 @@ namespace storm { using storm::settings::modules::AbstractionSettings; template - AutomatonAbstractor::AutomatonAbstractor(storm::jani::Automaton const& automaton, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), edges(), automaton(automaton) { + AutomatonAbstractor::AutomatonAbstractor(storm::jani::Automaton const& automaton, JaniAbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), edges(), automaton(automaton) { // For each concrete command, we create an abstract counterpart. uint64_t edgeId = 0; @@ -84,10 +84,10 @@ namespace storm { } template - storm::dd::Add AutomatonAbstractor::getEdgeUpdateProbabilitiesAdd() const { + storm::dd::Add AutomatonAbstractor::getEdgeDecoratorAdd() const { storm::dd::Add result = this->getAbstractionInformation().getDdManager().template getAddZero(); for (auto const& edge : edges) { - result += edge.getEdgeUpdateProbabilitiesAdd(); + result += edge.getEdgeDecoratorAdd(); } return result; } @@ -108,7 +108,7 @@ namespace storm { } template - AbstractionInformation const& AutomatonAbstractor::getAbstractionInformation() const { + JaniAbstractionInformation const& AutomatonAbstractor::getAbstractionInformation() const { return abstractionInformation.get(); } diff --git a/src/storm/abstraction/jani/AutomatonAbstractor.h b/src/storm/abstraction/jani/AutomatonAbstractor.h index b75a61b0d..e564d2dde 100644 --- a/src/storm/abstraction/jani/AutomatonAbstractor.h +++ b/src/storm/abstraction/jani/AutomatonAbstractor.h @@ -17,13 +17,13 @@ namespace storm { } namespace abstraction { - template - class AbstractionInformation; - template struct BottomStateResult; namespace jani { + template + class JaniAbstractionInformation; + template class AutomatonAbstractor { public: @@ -35,7 +35,7 @@ namespace storm { * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. * @param useDecomposition A flag indicating whether to use the decomposition during abstraction. */ - AutomatonAbstractor(storm::jani::Automaton const& automaton, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition); + AutomatonAbstractor(storm::jani::Automaton const& automaton, JaniAbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition); AutomatonAbstractor(AutomatonAbstractor const&) = default; AutomatonAbstractor& operator=(AutomatonAbstractor const&) = default; @@ -80,11 +80,11 @@ namespace storm { BottomStateResult getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables); /*! - * Retrieves an ADD that maps the encodings of edges and their updates to their probabilities. + * Retrieves an ADD that maps the encodings of edges, source/target locations and their updates to their probabilities. * - * @return The edge-update probability ADD. + * @return The edge decorator ADD. */ - storm::dd::Add getEdgeUpdateProbabilitiesAdd() const; + storm::dd::Add getEdgeDecoratorAdd() const; /*! * Retrieves the abstract edges of this abstract automton. @@ -113,13 +113,13 @@ namespace storm { * * @return The abstraction information. */ - AbstractionInformation const& getAbstractionInformation() const; + JaniAbstractionInformation const& getAbstractionInformation() const; // A factory that can be used to create new SMT solvers. std::shared_ptr smtSolverFactory; // The DD-related information. - std::reference_wrapper const> abstractionInformation; + std::reference_wrapper const> abstractionInformation; // The abstract edge of the abstract automaton. std::vector> edges; diff --git a/src/storm/abstraction/jani/EdgeAbstractor.cpp b/src/storm/abstraction/jani/EdgeAbstractor.cpp index 6fab837ab..ebaf89d58 100644 --- a/src/storm/abstraction/jani/EdgeAbstractor.cpp +++ b/src/storm/abstraction/jani/EdgeAbstractor.cpp @@ -4,8 +4,8 @@ #include -#include "storm/abstraction/AbstractionInformation.h" #include "storm/abstraction/BottomStateResult.h" +#include "storm/abstraction/jani/JaniAbstractionInformation.h" #include "storm/storage/dd/DdManager.h" #include "storm/storage/dd/Add.h" @@ -23,7 +23,7 @@ namespace storm { namespace abstraction { namespace jani { template - EdgeAbstractor::EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), edgeId(edgeId), edge(edge), localExpressionInformation(abstractionInformation), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), useDecomposition(useDecomposition), skipBottomStates(false), forceRecomputation(true), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, {!edge.getGuard()}, smtSolverFactory) { + EdgeAbstractor::EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, JaniAbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), edgeId(edgeId), edge(edge), localExpressionInformation(abstractionInformation), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), useDecomposition(useDecomposition), skipBottomStates(false), forceRecomputation(true), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, {!edge.getGuard()}, smtSolverFactory) { // Make the second component of relevant predicates have the right size. relevantPredicatesAndVariables.second.resize(edge.getNumberOfDestinations()); @@ -337,10 +337,10 @@ namespace storm { // if we did not explicitly enumerate the guard, we can construct it from the result BDD. if (!enumerateAbstractGuard) { - std::set allVariables(getAbstractionInformation().getSuccessorVariables()); - auto player2Variables = getAbstractionInformation().getPlayer2VariableSet(usedNondeterminismVariables); + std::set allVariables(this->getAbstractionInformation().getSuccessorVariables()); + auto player2Variables = this->getAbstractionInformation().getPlayer2VariableSet(usedNondeterminismVariables); allVariables.insert(player2Variables.begin(), player2Variables.end()); - auto auxVariables = getAbstractionInformation().getAuxVariableSet(0, getAbstractionInformation().getAuxVariableCount()); + auto auxVariables = this->getAbstractionInformation().getAuxVariableSet(0, this->getAbstractionInformation().getAuxVariableCount()); allVariables.insert(auxVariables.begin(), auxVariables.end()); std::set variablesToAbstract; @@ -653,12 +653,12 @@ namespace storm { } template - storm::dd::Add EdgeAbstractor::getEdgeUpdateProbabilitiesAdd() const { + storm::dd::Add EdgeAbstractor::getEdgeDecoratorAdd() const { storm::dd::Add result = this->getAbstractionInformation().getDdManager().template getAddZero(); - for (uint_fast64_t updateIndex = 0; updateIndex < edge.get().getNumberOfDestinations(); ++updateIndex) { - result += this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()).template toAdd() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(edge.get().getDestination(updateIndex).getProbability())); + for (uint_fast64_t destinationIndex = 0; destinationIndex < edge.get().getNumberOfDestinations(); ++destinationIndex) { + result += this->getAbstractionInformation().encodeAux(destinationIndex, 0, this->getAbstractionInformation().getAuxVariableCount()).template toAdd() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(edge.get().getDestination(destinationIndex).getProbability())) * this->getAbstractionInformation().encodeLocation(edge.get().getDestination(destinationIndex).getLocationIndex(), false).template toAdd(); } - result *= this->getAbstractionInformation().encodePlayer1Choice(edgeId, this->getAbstractionInformation().getPlayer1VariableCount()).template toAdd(); + result *= this->getAbstractionInformation().encodeLocation(edge.get().getSourceLocationIndex(), true).template toAdd() * this->getAbstractionInformation().encodePlayer1Choice(edgeId, this->getAbstractionInformation().getPlayer1VariableCount()).template toAdd(); return result; } @@ -668,12 +668,12 @@ namespace storm { } template - AbstractionInformation const& EdgeAbstractor::getAbstractionInformation() const { + JaniAbstractionInformation const& EdgeAbstractor::getAbstractionInformation() const { return abstractionInformation.get(); } template - AbstractionInformation& EdgeAbstractor::getAbstractionInformation() { + JaniAbstractionInformation& EdgeAbstractor::getAbstractionInformation() { return abstractionInformation.get(); } diff --git a/src/storm/abstraction/jani/EdgeAbstractor.h b/src/storm/abstraction/jani/EdgeAbstractor.h index 02240b34c..30c9b07a3 100644 --- a/src/storm/abstraction/jani/EdgeAbstractor.h +++ b/src/storm/abstraction/jani/EdgeAbstractor.h @@ -39,13 +39,13 @@ namespace storm { } namespace abstraction { - template - class AbstractionInformation; - template class BottomStateResult; namespace jani { + template + class JaniAbstractionInformation; + template class EdgeAbstractor { public: @@ -58,7 +58,7 @@ namespace storm { * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. * @param useDecomposition A flag indicating whether to use an edge decomposition during abstraction. */ - EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition); + EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, JaniAbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition); /*! * Refines the abstract edge with the given predicates. @@ -96,11 +96,11 @@ namespace storm { BottomStateResult getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables); /*! - * Retrieves an ADD that maps the encoding of the edge and its updates to their probabilities. + * Retrieves an ADD that maps the encoding of the edge, source/target locations and its updates to their probabilities. * - * @return The edge-update probability ADD. + * @return The decorator ADD. */ - storm::dd::Add getEdgeUpdateProbabilitiesAdd() const; + storm::dd::Add getEdgeDecoratorAdd() const; /*! * Retrieves the concrete edge that is abstracted by this abstract edge. @@ -194,14 +194,14 @@ namespace storm { * * @return The abstraction information object. */ - AbstractionInformation const& getAbstractionInformation() const; + JaniAbstractionInformation const& getAbstractionInformation() const; /*! * Retrieves the abstraction information object. * * @return The abstraction information object. */ - AbstractionInformation& getAbstractionInformation(); + JaniAbstractionInformation& getAbstractionInformation(); /*! * Computes the globally missing state identities. @@ -215,7 +215,7 @@ namespace storm { std::unique_ptr smtSolver; // The abstraction-related information. - std::reference_wrapper> abstractionInformation; + std::reference_wrapper> abstractionInformation; // The ID of the edge. uint64_t edgeId; diff --git a/src/storm/abstraction/jani/JaniAbstractionInformation.cpp b/src/storm/abstraction/jani/JaniAbstractionInformation.cpp new file mode 100644 index 000000000..53dcdf934 --- /dev/null +++ b/src/storm/abstraction/jani/JaniAbstractionInformation.cpp @@ -0,0 +1,48 @@ +#include "storm/abstraction/jani/JaniAbstractionInformation.h" + +#include "storm/storage/dd/DdManager.h" + +namespace storm { + namespace abstraction { + namespace jani { + + template + JaniAbstractionInformation::JaniAbstractionInformation(storm::expressions::ExpressionManager& expressionManager, std::set const& allVariables, uint64_t numberOfLocations, std::unique_ptr&& smtSolver, std::shared_ptr> ddManager) : AbstractionInformation(expressionManager, allVariables, std::move(smtSolver), ddManager) { + + // Create the location variable to have the appropriate dimension. + if (numberOfLocations > 1) { + locationVariables = ddManager->addMetaVariable("loc", 0, numberOfLocations - 1); + sourceLocationVariables.insert(locationVariables.get().first); + successorLocationVariables.insert(locationVariables.get().second); + } + } + + template + storm::dd::Bdd JaniAbstractionInformation::encodeLocation(uint64_t locationIndex, bool source) const { + if (locationVariables) { + if (source) { + return this->getDdManager().getEncoding(locationVariables.get().first, locationIndex); + } else { + return this->getDdManager().getEncoding(locationVariables.get().second, locationIndex); + } + } else { + return this->getDdManager().getBddOne(); + } + } + + template + std::set const& JaniAbstractionInformation::getSourceLocationVariables() const { + return sourceLocationVariables; + } + + template + std::set const& JaniAbstractionInformation::getSuccessorLocationVariables() const { + return successorLocationVariables; + } + + template class JaniAbstractionInformation; + template class JaniAbstractionInformation; + + } + } +} diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp index e2bcd456b..8dc61ec87 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp @@ -31,7 +31,7 @@ namespace storm { using storm::settings::modules::AbstractionSettings; template - JaniMenuGameAbstractor::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr const& smtSolverFactory) : model(model), smtSolverFactory(smtSolverFactory), abstractionInformation(model.getManager(), model.getAllExpressionVariables(), smtSolverFactory->create(model.getManager())), automata(), initialStateAbstractor(abstractionInformation, {model.getInitialStatesExpression()}, this->smtSolverFactory), validBlockAbstractor(abstractionInformation, smtSolverFactory), currentGame(nullptr), refinementPerformed(false) { + JaniMenuGameAbstractor::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr const& smtSolverFactory) : model(model), smtSolverFactory(smtSolverFactory), abstractionInformation(model.getManager(), model.getAllExpressionVariables(), model.getAutomaton(0).getNumberOfLocations(), smtSolverFactory->create(model.getManager())), automata(), initialStateAbstractor(abstractionInformation, {model.getInitialStatesExpression()}, this->smtSolverFactory), validBlockAbstractor(abstractionInformation, smtSolverFactory), 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. @@ -65,8 +65,8 @@ namespace storm { automata.emplace_back(automaton, abstractionInformation, this->smtSolverFactory, useDecomposition); } - // Retrieve the edge-update probability ADD, so we can multiply it with the abstraction BDD later. - edgeUpdateProbabilitiesAdd = automata.front().getEdgeUpdateProbabilitiesAdd(); + // Retrieve the decorator ADD, so we can multiply it with the abstraction BDD later. + edgeDecoratorAdd = automata.front().getEdgeDecoratorAdd(); } template @@ -167,7 +167,7 @@ namespace storm { // Construct the transition matrix by cutting away the transitions of unreachable states. storm::dd::Add transitionMatrix = (game.bdd && reachableStates).template toAdd(); - transitionMatrix *= edgeUpdateProbabilitiesAdd; + transitionMatrix *= edgeDecoratorAdd; transitionMatrix += deadlockTransitions; // Extend the current game information with the 'non-bottom' tag before potentially adding bottom state transitions. @@ -188,8 +188,10 @@ namespace storm { std::set allSourceVariables(abstractionInformation.getSourceVariables()); allSourceVariables.insert(abstractionInformation.getBottomStateVariable(true)); + allSourceVariables.insert(abstractionInformation.getSourceLocationVariables().begin(), abstractionInformation.getSourceLocationVariables().end()); std::set allSuccessorVariables(abstractionInformation.getSuccessorVariables()); allSuccessorVariables.insert(abstractionInformation.getBottomStateVariable(false)); + allSuccessorVariables.insert(abstractionInformation.getSuccessorLocationVariables().begin(), abstractionInformation.getSuccessorLocationVariables().end()); return std::make_unique>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStateResult.states, allSourceVariables, allSuccessorVariables, abstractionInformation.getExtendedSourceSuccessorVariablePairs(), std::set(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), usedPlayer2Variables, allNondeterminismVariables, auxVariables, abstractionInformation.getPredicateToBddMap()); } diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.h b/src/storm/abstraction/jani/JaniMenuGameAbstractor.h index 781579d56..329da0fcd 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.h +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.h @@ -3,10 +3,10 @@ #include "storm/storage/dd/DdType.h" #include "storm/abstraction/MenuGameAbstractor.h" -#include "storm/abstraction/AbstractionInformation.h" #include "storm/abstraction/MenuGame.h" #include "storm/abstraction/RefinementCommand.h" #include "storm/abstraction/ValidBlockAbstractor.h" +#include "storm/abstraction/jani/JaniAbstractionInformation.h" #include "storm/abstraction/jani/AutomatonAbstractor.h" #include "storm/storage/dd/Add.h" @@ -139,7 +139,7 @@ namespace storm { std::shared_ptr smtSolverFactory; // An object containing all information about the abstraction like predicates and the corresponding DDs. - AbstractionInformation abstractionInformation; + JaniAbstractionInformation abstractionInformation; // The abstract modules of the abstract program. std::vector> automata; @@ -150,8 +150,8 @@ namespace storm { // An object that is used to compute the valid blocks. ValidBlockAbstractor validBlockAbstractor; - // An ADD characterizing the probabilities of edges and their updates. - storm::dd::Add edgeUpdateProbabilitiesAdd; + // An ADD characterizing the probabilities and source/target locations of edges and their updates. + storm::dd::Add edgeDecoratorAdd; // The current game-based abstraction. std::unique_ptr> currentGame; diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 9ad1035b7..8de253c0b 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -698,6 +698,9 @@ namespace storm { return automata[index]; } + Automaton const& Model::getAutomaton(uint64_t index) const { + return automata[index]; } + Automaton const& Model::getAutomaton(std::string const& name) const { auto it = automatonToIndex.find(name); STORM_LOG_THROW(it != automatonToIndex.end(), storm::exceptions::InvalidOperationException, "Unable to retrieve unknown automaton '" << name << "'."); diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index de3cf6657..5d56e8e1e 100644 --- a/src/storm/storage/jani/Model.h +++ b/src/storm/storage/jani/Model.h @@ -239,6 +239,11 @@ namespace storm { */ Automaton& getAutomaton(uint64_t index); + /*! + * Retrieves the automaton with the given index. + */ + Automaton const& getAutomaton(uint64_t index) const; + /*! * Retrieves the automaton with the given name. */