equipped automata in JANI models with expression variable representing their location

src/storm/generator/VariableInformation.cpp

@@ -79,7 +79,7 @@ namespace storm {
             }
             for (auto const& automaton : model.getAutomata()) {
                 uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(automaton.getNumberOfLocations())));
-                locationVariables.emplace_back(model.getManager().declareFreshIntegerVariable(false, "loc"), automaton.getNumberOfLocations() - 1, totalBitOffset, bitwidth);
+                locationVariables.emplace_back(automaton.getLocationExpressionVariable(), automaton.getNumberOfLocations() - 1, totalBitOffset, bitwidth);
                 totalBitOffset += bitwidth;
                 
                 for (auto const& variable : automaton.getVariables().getBooleanVariables()) {

src/storm/parser/JaniParser.cpp

@@ -958,7 +958,7 @@ namespace storm {
         storm::jani::Automaton JaniParser::parseAutomaton(json const &automatonStructure, storm::jani::Model const& parentModel) {
             STORM_LOG_THROW(automatonStructure.count("name") == 1, storm::exceptions::InvalidJaniException, "Each automaton must have a name");
             std::string name = getString(automatonStructure.at("name"), " the name field for automaton");
-            storm::jani::Automaton automaton(name);
+            storm::jani::Automaton automaton(name, expressionManager->declareIntegerVariable("_loc_" + name));
             STORM_LOG_THROW(automatonStructure.count("locations") > 0, storm::exceptions::InvalidJaniException, "Automaton '" << name << "' does not have locations.");
             std::unordered_map<std::string, uint64_t> locIds;
             for(auto const& locEntry : automatonStructure.at("locations")) {

src/storm/storage/expressions/ExpressionManager.cpp

@@ -56,6 +56,10 @@ namespace storm {
             // Intentionally left empty.
         }
         
+        ExpressionManager::~ExpressionManager() {
+            // Intentionally left empty.
+        }
+        
         std::shared_ptr<ExpressionManager> ExpressionManager::clone() const {
             return std::shared_ptr<ExpressionManager>(new ExpressionManager(*this));
         }

src/storm/storage/expressions/ExpressionManager.h

@@ -71,6 +71,8 @@ namespace storm {
              */
             ExpressionManager();
             
+            ~ExpressionManager();
+            
             /*!
              * Creates a new expression manager with the same set of variables.
              */

src/storm/storage/expressions/Variable.cpp

@@ -3,9 +3,17 @@
 
 namespace storm {
     namespace expressions {
+        Variable::Variable() {
+            // Intentionally left empty.
+        }
+        
         Variable::Variable(std::shared_ptr<ExpressionManager const> const& manager, uint_fast64_t index) : manager(manager), index(index) {
             // Intentionally left empty.
         }
+        
+        Variable::~Variable() {
+            // Intentionally left empty.
+        }
 
         bool Variable::operator==(Variable const& other) const {
             return manager == other.manager && index == other.index;

src/storm/storage/expressions/Variable.h

@@ -17,7 +17,8 @@ namespace storm {
         // This class captures a simple variable.
         class Variable {
         public:
-            Variable() = default;
+            Variable();
+            ~Variable();
             
             /*!
              * Constructs a variable with the given index and type.

src/storm/storage/jani/Automaton.cpp

@@ -50,7 +50,7 @@ namespace storm {
             }
         }
         
-        Automaton::Automaton(std::string const& name) : name(name) {
+        Automaton::Automaton(std::string const& name, storm::expressions::Variable const& locationExpressionVariable) : name(name), locationExpressionVariable(locationExpressionVariable) {
             // Add a sentinel element to the mapping from locations to starting indices.
             locationToStartingIndex.push_back(0);
         }
@@ -166,6 +166,10 @@ namespace storm {
             }
             return mapping;
         }
+        
+        storm::expressions::Variable const& Automaton::getLocationExpressionVariable() const {
+            return locationExpressionVariable;
+        }
 
         Automaton::Edges Automaton::getEdgesFromLocation(std::string const& name) {
             auto it = locationToIndex.find(name);

src/storm/storage/jani/Automaton.h

@@ -95,7 +95,12 @@ namespace storm {
             /*!
              * Creates an empty automaton.
              */
-            Automaton(std::string const& name);
+            Automaton(std::string const& name, storm::expressions::Variable const& locationExpressionVariable);
+            
+            Automaton(Automaton const& other) = default;
+            Automaton& operator=(Automaton const& other) = default;
+            Automaton(Automaton&& other) = default;
+            Automaton& operator=(Automaton&& other) = default;
             
             /*!
              * Retrieves the name of the automaton.
@@ -207,6 +212,11 @@ namespace storm {
              */
             std::map<uint64_t, std::string> buildIdToLocationNameMap() const;
             
+            /*!
+             * Retrieves the expression variable that represents the location of this automaton.
+             */
+            storm::expressions::Variable const& getLocationExpressionVariable() const;
+            
             /*!
              * Retrieves the edges of the location with the given name.
              */
@@ -357,6 +367,9 @@ namespace storm {
         private:
             /// The name of the automaton.
             std::string name;
+            
+            /// The expression variable representing the location of this automaton.
+            storm::expressions::Variable locationExpressionVariable;
 
             /// The set of variables of this automaton.
             VariableSet variables;

src/storm/storage/jani/Model.cpp

@@ -418,7 +418,7 @@ namespace storm {
             ParallelComposition const& parallelComposition = systemComposition.asParallelComposition();
 
             // Create the new automaton that will hold the flattened system.
-            Automaton newAutomaton(this->getName() + "_flattening");
+            Automaton newAutomaton(this->getName() + "_flattened", expressionManager->declareIntegerVariable("_loc_flattened_" + this->getName()));
 
             std::map<Variable const*, std::reference_wrapper<Variable const>> variableRemapping;
             for (auto const& variable : getGlobalVariables()) {

src/storm/storage/prism/ToJaniConverter.cpp

@@ -146,7 +146,7 @@ namespace storm {
                 // Keep track of the action indices contained in this module.
                 std::set<uint_fast64_t> actionIndicesOfModule;
 
-                storm::jani::Automaton automaton(module.getName());
+                storm::jani::Automaton automaton(module.getName(), manager->declareIntegerVariable("_loc_prism2jani_" + module.getName()));
                 for (auto const& variable : module.getIntegerVariables()) {
                     storm::jani::BoundedIntegerVariable newIntegerVariable = *storm::jani::makeBoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression());
                     std::set<uint_fast64_t> const& accessingModuleIndices = variablesToAccessingModuleIndices[variable.getExpressionVariable()];