finalized location variable for JANI automata

src/storm/builder/DdJaniModelBuilder.cpp

@@ -159,7 +159,6 @@ namespace storm {
             std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> rowColumnMetaVariablePairs;
             
             // A mapping from automata to the meta variables encoding their location.
-            std::map<std::string, storm::expressions::Variable> automatonToLocationVariableMap;
             std::map<std::string, std::pair<storm::expressions::Variable, storm::expressions::Variable>> automatonToLocationDdVariableMap;
             
             // A mapping from action indices to the meta variables used to encode these actions.
@@ -264,10 +263,11 @@ namespace storm {
                     result.allNondeterminismVariables.insert(result.markovNondeterminismVariable);
                 }
                 
-                for (auto const& automaton : this->model.getAutomata()) {
+                for (auto const& automatonName : this->automata) {
+                    storm::jani::Automaton const& automaton =  this->model.getAutomaton(automatonName);
+                    
                     // Start by creating a meta variable for the location of the automaton.
-                    storm::expressions::Variable locationExpressionVariable = model.getManager().declareFreshIntegerVariable(false, "loc");
-                    result.automatonToLocationVariableMap[automaton.getName()] = locationExpressionVariable;
+                    storm::expressions::Variable locationExpressionVariable = automaton.getLocationExpressionVariable();
                     std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable("l_" + automaton.getName(), 0, automaton.getNumberOfLocations() - 1);
                     result.automatonToLocationDdVariableMap[automaton.getName()] = variablePair;
                     result.rowColumnMetaVariablePairs.push_back(variablePair);
@@ -1785,10 +1785,16 @@ namespace storm {
         std::map<std::string, storm::expressions::Expression> buildLabelExpressions(storm::jani::Model const& model, CompositionVariables<Type, ValueType> const& variables, typename DdJaniModelBuilder<Type, ValueType>::Options const& options) {
             std::map<std::string, storm::expressions::Expression> result;
             
+            // Create a list of composed automata to restrict the labels to locations of these automata.
+            std::vector<std::reference_wrapper<storm::jani::Automaton const>> composedAutomata;
+            for (auto const& entry : variables.automatonToIdentityMap) {
+                composedAutomata.emplace_back(model.getAutomaton(entry.first));
+            }
+            
             for (auto const& variable : model.getGlobalVariables().getTransientVariables()) {
                 if (variable.isBooleanVariable()) {
                     if (options.buildAllLabels || options.labelNames.find(variable.getName()) != options.labelNames.end()) {
-                        result[variable.getName()] = model.getLabelExpression(variable.asBooleanVariable(), variables.automatonToLocationVariableMap);
+                        result[variable.getName()] = model.getLabelExpression(variable.asBooleanVariable(), composedAutomata);
                     }
                 }
             }

src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp

@@ -97,11 +97,6 @@ namespace storm {
                     }
                 }
                 
-                // Create location variables for all the automata that we put in parallel.
-                for (auto const& automaton : parallelAutomata) {
-                    automatonToLocationVariable.emplace(automaton.get().getName(), this->model.getManager().declareFreshIntegerVariable(false, automaton.get().getName() + "_"));
-                }
-                
                 // If the program still contains undefined constants and we are not in a parametric setting, assemble an appropriate error message.
 #ifdef STORM_HAVE_CARL
                 if (!std::is_same<ValueType, storm::RationalFunction>::value && this->model.hasUndefinedConstants()) {
@@ -1514,7 +1509,7 @@ namespace storm {
                         if (this->options.isBuildAllLabelsSet() || this->options.getLabelNames().find(variable.getName()) != this->options.getLabelNames().end()) {
                             cpptempl::data_map label;
                             label["name"] = variable.getName();
-                            label["predicate"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(model.getLabelExpression(variable.asBooleanVariable(), automatonToLocationVariable)), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName));
+                            label["predicate"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(model.getLabelExpression(variable.asBooleanVariable(), parallelAutomata)), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName));
                             labels.push_back(label);
                         }
                     }
@@ -1542,7 +1537,7 @@ namespace storm {
                         auto const& variable = variables.getVariable(labelOrExpression.getLabel());
                         STORM_LOG_THROW(variable.isBooleanVariable(), storm::exceptions::WrongFormatException, "Terminal label refers to non-boolean variable '" << variable.getName() << ".");
                         STORM_LOG_THROW(variable.isTransient(), storm::exceptions::WrongFormatException, "Terminal label refers to non-transient variable '" << variable.getName() << ".");
-                        auto labelExpression = model.getLabelExpression(variable.asBooleanVariable(), automatonToLocationVariable);
+                        auto labelExpression = model.getLabelExpression(variable.asBooleanVariable(), parallelAutomata);
                         if (terminalEntry.second) {
                             labelExpression = !labelExpression;
                         }
@@ -1590,7 +1585,7 @@ namespace storm {
                 
             template <typename ValueType, typename RewardModelType>
             storm::expressions::Variable const& ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::getLocationVariable(storm::jani::Automaton const& automaton) const {
-                return automatonToLocationVariable.at(automaton.getName());
+                return automaton.getLocationExpressionVariable();
             }
             
             template <typename ValueType, typename RewardModelType>

src/storm/builder/jit/ExplicitJitJaniModelBuilder.h

@@ -161,7 +161,6 @@ namespace storm {
                 // Members that store information about the model. They are used in the process of assembling the model
                 // data that is used in the skeleton.
                 std::unordered_map<storm::expressions::Variable, std::string> variableToName;
-                std::map<std::string, storm::expressions::Variable> automatonToLocationVariable;
                 storm::expressions::ToCppVisitor expressionTranslator;
                 std::map<storm::expressions::Variable, storm::expressions::Expression> lowerBoundShiftSubstitution;
                 std::map<storm::expressions::Variable, int_fast64_t> lowerBounds;

src/storm/generator/JaniNextStateGenerator.cpp

@@ -80,11 +80,9 @@ namespace storm {
             
             // If there are terminal states we need to handle, we now need to translate all labels to expressions.
             if (this->options.hasTerminalStates()) {
-                std::map<std::string, storm::expressions::Variable> locationVariables;
-                auto locationVariableIt = this->variableInformation.locationVariables.begin();
+                std::vector<std::reference_wrapper<storm::jani::Automaton const>> composedAutomata;
                 for (auto const& automaton : this->model.getAutomata()) {
-                    locationVariables[automaton.getName()] = locationVariableIt->variable;
-                    ++locationVariableIt;
+                    composedAutomata.emplace_back(automaton);
                 }
                 
                 for (auto const& expressionOrLabelAndBool : this->options.getTerminalStates()) {
@@ -100,7 +98,7 @@ namespace storm {
                             STORM_LOG_THROW(variable.isBooleanVariable(), storm::exceptions::InvalidSettingsException, "Terminal states refer to non-boolean variable '" << expressionOrLabelAndBool.first.getLabel() << "'.");
                             STORM_LOG_THROW(variable.isTransient(), storm::exceptions::InvalidSettingsException, "Terminal states refer to non-transient variable '" << expressionOrLabelAndBool.first.getLabel() << "'.");
                             
-                            this->terminalStates.push_back(std::make_pair(this->model.getLabelExpression(variable.asBooleanVariable(), locationVariables), expressionOrLabelAndBool.second));
+                            this->terminalStates.push_back(std::make_pair(this->model.getLabelExpression(variable.asBooleanVariable(), composedAutomata), expressionOrLabelAndBool.second));
                         }
                     }
                 }
@@ -618,11 +616,9 @@ namespace storm {
         storm::models::sparse::StateLabeling JaniNextStateGenerator<ValueType, StateType>::label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices) {
             
             // Prepare a mapping from automata names to the location variables.
-            std::map<std::string, storm::expressions::Variable> locationVariables;
-            auto locationVariableIt = this->variableInformation.locationVariables.begin();
+            std::vector<std::reference_wrapper<storm::jani::Automaton const>> composedAutomata;
             for (auto const& automaton : model.getAutomata()) {
-                locationVariables[automaton.getName()] = locationVariableIt->variable;
-                ++locationVariableIt;
+                composedAutomata.emplace_back(automaton);
             }
             
             // As in JANI we can use transient boolean variable assignments in locations to identify states, we need to
@@ -631,7 +627,7 @@ namespace storm {
             for (auto const& variable : model.getGlobalVariables().getTransientVariables()) {
                 if (variable.isBooleanVariable()) {
                     if (this->options.isBuildAllLabelsSet() || this->options.getLabelNames().find(variable.getName()) != this->options.getLabelNames().end()) {
-                        transientVariableToExpressionMap[variable.getExpressionVariable()] = model.getLabelExpression(variable.asBooleanVariable(), locationVariables);
+                        transientVariableToExpressionMap[variable.getExpressionVariable()] = model.getLabelExpression(variable.asBooleanVariable(), composedAutomata);
                     }
                 }
             }

src/storm/storage/jani/Model.cpp

@@ -969,18 +969,19 @@ namespace storm {
             STORM_LOG_ASSERT(composition != nullptr, "Composition is not set");
         }
         
-        storm::expressions::Expression Model::getLabelExpression(BooleanVariable const& transientVariable, std::map<std::string, storm::expressions::Variable> const& automatonToLocationVariableMap) const {
+        storm::expressions::Expression Model::getLabelExpression(BooleanVariable const& transientVariable, std::vector<std::reference_wrapper<Automaton const>> const& automata) const {
             STORM_LOG_THROW(transientVariable.isTransient(), storm::exceptions::InvalidArgumentException, "Expected transient variable.");
             
             storm::expressions::Expression result;
             bool negate = transientVariable.getInitExpression().isTrue();
             
-            for (auto const& automaton : this->getAutomata()) {
-                storm::expressions::Variable const& locationVariable = automatonToLocationVariableMap.at(automaton.getName());
-                for (auto const& location : automaton.getLocations()) {
+            for (auto const& automaton : automata) {
+                storm::expressions::Variable const& locationVariable = automaton.get().getLocationExpressionVariable();
+                
+                for (auto const& location : automaton.get().getLocations()) {
                     for (auto const& assignment : location.getAssignments().getTransientAssignments()) {
                         if (assignment.getExpressionVariable() == transientVariable.getExpressionVariable()) {
-                            auto newExpression = (locationVariable == this->getManager().integer(automaton.getLocationIndex(location.getName()))) && (negate ? !assignment.getAssignedExpression() : assignment.getAssignedExpression());
+                            auto newExpression = (locationVariable == this->getManager().integer(automaton.get().getLocationIndex(location.getName()))) && (negate ? !assignment.getAssignedExpression() : assignment.getAssignedExpression());
                             if (result.isInitialized()) {
                                 result = result || newExpression;
                             } else {

src/storm/storage/jani/Model.h

@@ -379,7 +379,7 @@ namespace storm {
              * Creates the expression that characterizes all states in which the provided transient boolean variable is
              * true. The provided location variables are used to encode the location of the automata.
              */
-            storm::expressions::Expression getLabelExpression(BooleanVariable const& transientVariable, std::map<std::string, storm::expressions::Variable> const& automatonToLocationVariableMap) const;
+            storm::expressions::Expression getLabelExpression(BooleanVariable const& transientVariable, std::vector<std::reference_wrapper<Automaton const>> const& automata) const;
             
             /*!
              * Checks that undefined constants (parameters) of the model preserve the graph of the underlying model.