Fixed issues related to allowing local variables when converting from prism to jani

src/storm/storage/prism/ToJaniConverter.cpp

@@ -99,6 +99,14 @@ namespace storm {
                 }
             }
             
+            // Create a mapping from variables to a flag indicating whether it should be made global
+            std::map<storm::expressions::Variable, bool> variablesToMakeGlobal;
+            for (auto const& varMods : variablesToAccessingModuleIndices) {
+                assert(!varMods.second.empty());
+                // If there is exactly one module reading and writing the variable, we can make the variable local to this module.
+                variablesToMakeGlobal[varMods.first] = allVariablesGlobal || (varMods.second.size() > 1);
+            }
+            
             // Go through the labels and construct assignments to transient variables that are added to the locations.
             std::vector<storm::jani::Assignment> transientLocationAssignments;
             for (auto const& label : program.getLabels()) {
@@ -111,6 +119,24 @@ namespace storm {
                 auto newExpressionVariable = manager->declareBooleanVariable(finalLabelName);
                 storm::jani::BooleanVariable const& newTransientVariable = janiModel.addVariable(storm::jani::BooleanVariable(newExpressionVariable.getName(), newExpressionVariable, manager->boolean(false), true));
                 transientLocationAssignments.emplace_back(newTransientVariable, label.getStatePredicateExpression());
+
+                // Variables that are accessed in the label predicate expression should be made global.
+                std::set<storm::expressions::Variable> variables = label.getStatePredicateExpression().getVariables();
+                for (auto const& variable : variables) {
+                    variablesToMakeGlobal[variable] = true;
+                }
+            }
+            
+            // Create an initial state restriction if there was an initial construct in the program.
+            if (program.hasInitialConstruct()) {
+                janiModel.setInitialStatesRestriction(program.getInitialConstruct().getInitialStatesExpression());
+                // Variables in the initial state expression should be made global
+                std::set<storm::expressions::Variable> variables = program.getInitialConstruct().getInitialStatesExpression().getVariables();
+                for (auto const& variable : variables) {
+                    variablesToMakeGlobal[variable] = true;
+                }
+            } else {
+                janiModel.setInitialStatesRestriction(manager->boolean(true));
             }
             
             // Go through the reward models and construct assignments to the transient variables that are to be added to
@@ -131,6 +157,11 @@ namespace storm {
                         }
                     }
                     transientLocationAssignments.emplace_back(newTransientVariable, transientLocationExpression);
+                    // Variables that are accessed in a reward term should be made global.
+                    std::set<storm::expressions::Variable> variables = transientLocationExpression.getVariables();
+                    for (auto const& variable : variables) {
+                        variablesToMakeGlobal[variable] = true;
+                    }
                 }
                 
                 std::map<uint_fast64_t, storm::expressions::Expression> actionIndexToExpression;
@@ -152,6 +183,11 @@ namespace storm {
                         std::vector<storm::jani::Assignment> assignments = {storm::jani::Assignment(newTransientVariable, entry.second)};
                         transientEdgeAssignments.emplace(entry.first, assignments);
                     }
+                    // Variables that are accessed in a reward term should be made global.
+                    std::set<storm::expressions::Variable> variables = entry.second.getVariables();
+                    for (auto const& variable : variables) {
+                        variablesToMakeGlobal[variable] = true;
+                    }
                 }
                 STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotImplementedException, "Transition reward translation currently not implemented.");
             }
@@ -182,28 +218,24 @@ namespace storm {
                 storm::jani::Automaton automaton(module.getName(), manager->declareIntegerVariable("_loc_prism2jani_" + module.getName() + "_" + suffix));
                 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()];
-                    // If there is exactly one module reading and writing the variable, we can make the variable local to this module.
-                    if (!allVariablesGlobal && accessingModuleIndices.size() == 1) {
-                        storm::jani::BoundedIntegerVariable const& createdVariable = automaton.addVariable(newIntegerVariable);
-                        variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
-                    } else if (!accessingModuleIndices.empty()) {
-                        // Otherwise, we need to make it global.
-                        storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addVariable(newIntegerVariable);
+                    auto findRes = variablesToMakeGlobal.find(variable.getExpressionVariable());
+                    if (findRes != variablesToMakeGlobal.end()) {
+                        bool makeVarGlobal = findRes->second;
+                        storm::jani::BoundedIntegerVariable const& createdVariable = makeVarGlobal ? janiModel.addVariable(newIntegerVariable) : automaton.addVariable(newIntegerVariable);
                         variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
+                    } else {
+                        STORM_LOG_INFO("Variable " << variable.getName() << " is declared but never used.");
                     }
                 }
                 for (auto const& variable : module.getBooleanVariables()) {
                     storm::jani::BooleanVariable newBooleanVariable = *storm::jani::makeBooleanVariable(variable.getName(), variable.getExpressionVariable(), variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, false);
-                    std::set<uint_fast64_t> const& accessingModuleIndices = variablesToAccessingModuleIndices[variable.getExpressionVariable()];
-                    // If there is exactly one module reading and writing the variable, we can make the variable local to this module.
-                    if (!allVariablesGlobal && accessingModuleIndices.size() == 1) {
-                        storm::jani::BooleanVariable const& createdVariable = automaton.addVariable(newBooleanVariable);
-                        variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
-                    } else if (!accessingModuleIndices.empty()) {
-                        // Otherwise, we need to make it global.
-                        storm::jani::BooleanVariable const& createdVariable = janiModel.addVariable(newBooleanVariable);
+                    auto findRes = variablesToMakeGlobal.find(variable.getExpressionVariable());
+                    if (findRes != variablesToMakeGlobal.end()) {
+                        bool makeVarGlobal = findRes->second;
+                        storm::jani::BooleanVariable const& createdVariable = makeVarGlobal ? janiModel.addVariable(newBooleanVariable) : automaton.addVariable(newBooleanVariable);
                         variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
+                    } else {
+                        STORM_LOG_INFO("Variable " << variable.getName() << " is declared but never used.");
                     }
                 }
                 automaton.setInitialStatesRestriction(manager->boolean(true));
@@ -303,13 +335,6 @@ namespace storm {
                 firstModule = false;
             }
             
-            // Create an initial state restriction if there was an initial construct in the program.
-            if (program.hasInitialConstruct()) {
-                janiModel.setInitialStatesRestriction(program.getInitialConstruct().getInitialStatesExpression());
-            } else {
-                janiModel.setInitialStatesRestriction(manager->boolean(true));
-            }
-            
             // Set the standard system composition. This is possible, because we reject non-standard compositions anyway.
             if (program.specifiesSystemComposition()) {
                 CompositionToJaniVisitor visitor;