added location support to JANI menu game abstractor

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 <storm::dd::DdType DdType, typename ValueType>
-            AutomatonAbstractor<DdType, ValueType>::AutomatonAbstractor(storm::jani::Automaton const& automaton, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), edges(), automaton(automaton) {
+            AutomatonAbstractor<DdType, ValueType>::AutomatonAbstractor(storm::jani::Automaton const& automaton, JaniAbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> 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::DdType DdType, typename ValueType>
-            storm::dd::Add<DdType, ValueType> AutomatonAbstractor<DdType, ValueType>::getEdgeUpdateProbabilitiesAdd() const {
+            storm::dd::Add<DdType, ValueType> AutomatonAbstractor<DdType, ValueType>::getEdgeDecoratorAdd() const {
                 storm::dd::Add<DdType, ValueType> result = this->getAbstractionInformation().getDdManager().template getAddZero<ValueType>();
                 for (auto const& edge : edges) {
-                    result += edge.getEdgeUpdateProbabilitiesAdd();
+                    result += edge.getEdgeDecoratorAdd();
                 }
                 return result;
             }
@@ -108,7 +108,7 @@ namespace storm {
             }
 
             template <storm::dd::DdType DdType, typename ValueType>
-            AbstractionInformation<DdType> const& AutomatonAbstractor<DdType, ValueType>::getAbstractionInformation() const {
+            JaniAbstractionInformation<DdType> const& AutomatonAbstractor<DdType, ValueType>::getAbstractionInformation() const {
                 return abstractionInformation.get();
             }
             

src/storm/abstraction/jani/AutomatonAbstractor.h

@@ -17,13 +17,13 @@ namespace storm {
     }
     
     namespace abstraction {
-        template <storm::dd::DdType DdType>
-        class AbstractionInformation;
-
         template<storm::dd::DdType DdType>
         struct BottomStateResult;
 
         namespace jani {
+            template <storm::dd::DdType DdType>
+            class JaniAbstractionInformation;
+            
             template <storm::dd::DdType DdType, typename ValueType>
             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<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition);
+                AutomatonAbstractor(storm::jani::Automaton const& automaton, JaniAbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition);
                 
                 AutomatonAbstractor(AutomatonAbstractor const&) = default;
                 AutomatonAbstractor& operator=(AutomatonAbstractor const&) = default;
@@ -80,11 +80,11 @@ namespace storm {
                 BottomStateResult<DdType> getBottomStateTransitions(storm::dd::Bdd<DdType> 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<DdType, ValueType> getEdgeUpdateProbabilitiesAdd() const;
+                storm::dd::Add<DdType, ValueType> getEdgeDecoratorAdd() const;
                 
                 /*!
                  * Retrieves the abstract edges of this abstract automton.
@@ -113,13 +113,13 @@ namespace storm {
                  *
                  * @return The abstraction information.
                  */
-                AbstractionInformation<DdType> const& getAbstractionInformation() const;
+                JaniAbstractionInformation<DdType> const& getAbstractionInformation() const;
                 
                 // A factory that can be used to create new SMT solvers.
                 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory;
                 
                 // The DD-related information.
-                std::reference_wrapper<AbstractionInformation<DdType> const> abstractionInformation;
+                std::reference_wrapper<JaniAbstractionInformation<DdType> const> abstractionInformation;
                 
                 // The abstract edge of the abstract automaton.
                 std::vector<EdgeAbstractor<DdType, ValueType>> edges;

src/storm/abstraction/jani/EdgeAbstractor.cpp

@@ -4,8 +4,8 @@
 
 #include <boost/iterator/transform_iterator.hpp>
 
-#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 <storm::dd::DdType DdType, typename ValueType>
-            EdgeAbstractor<DdType, ValueType>::EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> 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<DdType, ValueType>::EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, JaniAbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> 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<storm::expressions::Variable> allVariables(getAbstractionInformation().getSuccessorVariables());
-                        auto player2Variables = getAbstractionInformation().getPlayer2VariableSet(usedNondeterminismVariables);
+                        std::set<storm::expressions::Variable> 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<storm::expressions::Variable> variablesToAbstract;
@@ -653,12 +653,12 @@ namespace storm {
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
-            storm::dd::Add<DdType, ValueType> EdgeAbstractor<DdType, ValueType>::getEdgeUpdateProbabilitiesAdd() const {
+            storm::dd::Add<DdType, ValueType> EdgeAbstractor<DdType, ValueType>::getEdgeDecoratorAdd() const {
                 storm::dd::Add<DdType, ValueType> result = this->getAbstractionInformation().getDdManager().template getAddZero<ValueType>();
-                for (uint_fast64_t updateIndex = 0; updateIndex < edge.get().getNumberOfDestinations(); ++updateIndex) {
-                    result += this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()).template toAdd<ValueType>() * 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<ValueType>() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(edge.get().getDestination(destinationIndex).getProbability())) * this->getAbstractionInformation().encodeLocation(edge.get().getDestination(destinationIndex).getLocationIndex(), false).template toAdd<ValueType>();
                 }
-                result *= this->getAbstractionInformation().encodePlayer1Choice(edgeId, this->getAbstractionInformation().getPlayer1VariableCount()).template toAdd<ValueType>();
+                result *= this->getAbstractionInformation().encodeLocation(edge.get().getSourceLocationIndex(), true).template toAdd<ValueType>() * this->getAbstractionInformation().encodePlayer1Choice(edgeId, this->getAbstractionInformation().getPlayer1VariableCount()).template toAdd<ValueType>();
                 return result;
             }
             
@@ -668,12 +668,12 @@ namespace storm {
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
-            AbstractionInformation<DdType> const& EdgeAbstractor<DdType, ValueType>::getAbstractionInformation() const {
+            JaniAbstractionInformation<DdType> const& EdgeAbstractor<DdType, ValueType>::getAbstractionInformation() const {
                 return abstractionInformation.get();
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
-            AbstractionInformation<DdType>& EdgeAbstractor<DdType, ValueType>::getAbstractionInformation() {
+            JaniAbstractionInformation<DdType>& EdgeAbstractor<DdType, ValueType>::getAbstractionInformation() {
                 return abstractionInformation.get();
             }
             

src/storm/abstraction/jani/EdgeAbstractor.h

@@ -39,13 +39,13 @@ namespace storm {
     }
     
     namespace abstraction {
-        template <storm::dd::DdType DdType>
-        class AbstractionInformation;
-
         template <storm::dd::DdType DdType>
         class BottomStateResult;
 
         namespace jani {
+            template <storm::dd::DdType DdType>
+            class JaniAbstractionInformation;
+
             template <storm::dd::DdType DdType, typename ValueType>
             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<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition);
+                EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, JaniAbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition);
                                
                 /*!
                  * Refines the abstract edge with the given predicates.
@@ -96,11 +96,11 @@ namespace storm {
                 BottomStateResult<DdType> getBottomStateTransitions(storm::dd::Bdd<DdType> 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<DdType, ValueType> getEdgeUpdateProbabilitiesAdd() const;
+                storm::dd::Add<DdType, ValueType> 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<DdType> const& getAbstractionInformation() const;
+                JaniAbstractionInformation<DdType> const& getAbstractionInformation() const;
 
                 /*!
                  * Retrieves the abstraction information object.
                  *
                  * @return The abstraction information object.
                  */
-                AbstractionInformation<DdType>& getAbstractionInformation();
+                JaniAbstractionInformation<DdType>& getAbstractionInformation();
                 
                 /*!
                  * Computes the globally missing state identities.
@@ -215,7 +215,7 @@ namespace storm {
                 std::unique_ptr<storm::solver::SmtSolver> smtSolver;
 
                 // The abstraction-related information.
-                std::reference_wrapper<AbstractionInformation<DdType>> abstractionInformation;
+                std::reference_wrapper<JaniAbstractionInformation<DdType>> abstractionInformation;
                 
                 // The ID of the edge.
                 uint64_t edgeId;

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<storm::dd::DdType DdType>
+            JaniAbstractionInformation<DdType>::JaniAbstractionInformation(storm::expressions::ExpressionManager& expressionManager, std::set<storm::expressions::Variable> const& allVariables, uint64_t numberOfLocations, std::unique_ptr<storm::solver::SmtSolver>&& smtSolver, std::shared_ptr<storm::dd::DdManager<DdType>> ddManager) : AbstractionInformation<DdType>(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::DdType DdType>
+            storm::dd::Bdd<DdType> JaniAbstractionInformation<DdType>::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<storm::dd::DdType DdType>
+            std::set<storm::expressions::Variable> const& JaniAbstractionInformation<DdType>::getSourceLocationVariables() const {
+                return sourceLocationVariables;
+            }
+            
+            template<storm::dd::DdType DdType>
+            std::set<storm::expressions::Variable> const& JaniAbstractionInformation<DdType>::getSuccessorLocationVariables() const {
+                return successorLocationVariables;
+            }
+
+            template class JaniAbstractionInformation<storm::dd::DdType::CUDD>;
+            template class JaniAbstractionInformation<storm::dd::DdType::Sylvan>;
+            
+        }
+    }
+}

src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp

@@ -31,7 +31,7 @@ namespace storm {
             using storm::settings::modules::AbstractionSettings;
             
             template <storm::dd::DdType DdType, typename ValueType>
-            JaniMenuGameAbstractor<DdType, ValueType>::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> 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<DdType, ValueType>::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> 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 <storm::dd::DdType DdType, typename ValueType>
@@ -167,7 +167,7 @@ namespace storm {
                 
                 // 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 *= 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<storm::expressions::Variable> allSourceVariables(abstractionInformation.getSourceVariables());
                 allSourceVariables.insert(abstractionInformation.getBottomStateVariable(true));
+                allSourceVariables.insert(abstractionInformation.getSourceLocationVariables().begin(), abstractionInformation.getSourceLocationVariables().end());
                 std::set<storm::expressions::Variable> allSuccessorVariables(abstractionInformation.getSuccessorVariables());
                 allSuccessorVariables.insert(abstractionInformation.getBottomStateVariable(false));
+                allSuccessorVariables.insert(abstractionInformation.getSuccessorLocationVariables().begin(), abstractionInformation.getSuccessorLocationVariables().end());
                 
                 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());
             }

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<storm::utility::solver::SmtSolverFactory> smtSolverFactory;
                 
                 // An object containing all information about the abstraction like predicates and the corresponding DDs.
-                AbstractionInformation<DdType> abstractionInformation;
+                JaniAbstractionInformation<DdType> abstractionInformation;
                 
                 // The abstract modules of the abstract program.
                 std::vector<AutomatonAbstractor<DdType, ValueType>> automata;
@@ -150,8 +150,8 @@ namespace storm {
                 // An object that is used to compute the valid blocks.
                 ValidBlockAbstractor<DdType> validBlockAbstractor;
                                 
-                // An ADD characterizing the probabilities of edges and their updates.
-                storm::dd::Add<DdType, ValueType> edgeUpdateProbabilitiesAdd;
+                // An ADD characterizing the probabilities and source/target locations of edges and their updates.
+                storm::dd::Add<DdType, ValueType> edgeDecoratorAdd;
                 
                 // The current game-based abstraction.
                 std::unique_ptr<MenuGame<DdType, ValueType>> currentGame;

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 << "'.");

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.
              */