Prism: ToJaniConverters now enforces variables occurring in properties to become global. This fixes GitHub issue #40

src/storm/storage/prism/Program.cpp

@@ -1843,7 +1843,7 @@ namespace storm {
         
         storm::jani::Model Program::toJani(bool allVariablesGlobal, std::string suffix) const {
             ToJaniConverter converter;
-            auto janiModel = converter.convert(*this, allVariablesGlobal, suffix);
+            auto janiModel = converter.convert(*this, allVariablesGlobal, {}, suffix);
             STORM_LOG_WARN_COND(!converter.labelsWereRenamed(), "Labels were renamed in PRISM-to-JANI conversion, but the mapping is not stored.");
             STORM_LOG_WARN_COND(!converter.rewardModelsWereRenamed(), "Rewardmodels were renamed in PRISM-to-JANI conversion, but the mapping is not stored.");
             return janiModel;
@@ -1851,7 +1851,14 @@ namespace storm {
 
         std::pair<storm::jani::Model, std::vector<storm::jani::Property>> Program::toJani(std::vector<storm::jani::Property> const& properties, bool allVariablesGlobal, std::string suffix) const {
             ToJaniConverter converter;
-            auto janiModel = converter.convert(*this, allVariablesGlobal, suffix);
+            std::set<storm::expressions::Variable> variablesToMakeGlobal;
+            if (!allVariablesGlobal) {
+                for (auto const& prop : properties) {
+                    auto vars = prop.getUsedVariablesAndConstants();
+                    variablesToMakeGlobal.insert(vars.begin(), vars.end());
+                }
+            }
+            auto janiModel = converter.convert(*this, allVariablesGlobal, variablesToMakeGlobal, suffix);
             std::vector<storm::jani::Property> newProperties;
             if (converter.labelsWereRenamed() || converter.rewardModelsWereRenamed()) {
                 newProperties = converter.applyRenaming(properties);

src/storm/storage/prism/ToJaniConverter.cpp

@@ -18,7 +18,7 @@
 namespace storm {
     namespace prism {
         
-        storm::jani::Model ToJaniConverter::convert(storm::prism::Program const& program, bool allVariablesGlobal, std::string suffix) {
+        storm::jani::Model ToJaniConverter::convert(storm::prism::Program const& program, bool allVariablesGlobal, std::set<storm::expressions::Variable> const& givenVariablesToMakeGlobal, std::string suffix) {
             labelRenaming.clear();
             rewardModelRenaming.clear();
             formulaToFunctionCallMap.clear();
@@ -53,6 +53,9 @@ namespace storm {
             
             // Maintain a mapping of each variable to a flag that is true if the variable will be made global.
             std::map<storm::expressions::Variable, bool> variablesToMakeGlobal;
+            for (auto const& var : givenVariablesToMakeGlobal) {
+                variablesToMakeGlobal.emplace(var, true);
+            }
             
             // Get the set of variables that appeare in a renaimng of a renamed module
             if (program.getNumberOfFormulas() > 0) {

src/storm/storage/prism/ToJaniConverter.h

@@ -18,7 +18,7 @@ namespace storm {
         
         class ToJaniConverter {
         public:
-            storm::jani::Model convert(storm::prism::Program const& program, bool allVariablesGlobal = true, std::string suffix = "");
+            storm::jani::Model convert(storm::prism::Program const& program, bool allVariablesGlobal = true, std::set<storm::expressions::Variable> const& variablesToMakeGlobal = {}, std::string suffix = "");
             
             bool labelsWereRenamed() const;
             bool rewardModelsWereRenamed() const;