storm-conv: Added ability to make global variables of a jani model local (or vice versa)

src/storm-conv/api/storm-conv.cpp

@@ -4,6 +4,7 @@
 #include "storm/storage/jani/Property.h"
 #include "storm/storage/jani/Constant.h"
 #include "storm/storage/jani/JaniLocationExpander.h"
+#include "storm/storage/jani/JaniScopeChanger.h"
 #include "storm/storage/jani/JSONExporter.h"
 
 #include "storm/settings/SettingsManager.h"
@@ -18,7 +19,26 @@ namespace storm {
                 janiModel = janiModel.substituteConstants();
             }
             
+            if (options.localVars) {
+                STORM_LOG_WARN_COND(!options.globalVars, "Ignoring 'globalvars' option, since 'localvars' is also set.");
+                storm::jani::JaniScopeChanger().makeVariablesLocal(janiModel, properties);
+            } else if (options.globalVars) {
+                storm::jani::JaniScopeChanger().makeVariablesGlobal(janiModel);
+            }
+            
             if (!options.locationVariables.empty()) {
+                // Make variables local if necessary/possible
+                for (auto const& pair : options.locationVariables) {
+                    if (janiModel.hasGlobalVariable(pair.second)) {
+                        auto var = janiModel.getGlobalVariable(pair.second).getExpressionVariable();
+                        if (storm::jani::JaniScopeChanger().canMakeVariableLocal(var, janiModel, properties, janiModel.getAutomatonIndex(pair.first)).first) {
+                            storm::jani::JaniScopeChanger().makeVariableLocal(var, janiModel, janiModel.getAutomatonIndex(pair.first));
+                        } else {
+                            STORM_LOG_ERROR("Can not transform variable " << pair.second << " into locations since it can not be made local to automaton " << pair.first << ".");
+                        }
+                    }
+                }
+                
                 for (auto const& pair : options.locationVariables) {
                     storm::jani::JaniLocationExpander expander(janiModel);
                     expander.transform(pair.first, pair.second);

src/storm-conv/converter/options/JaniConversionOptions.cpp

@@ -3,11 +3,11 @@
 namespace storm {
     namespace converter {
 
-        JaniConversionOptions::JaniConversionOptions() : edgeAssignments(false), flatten(false), substituteConstants(true), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()), addPropertyConstants(true) {
+        JaniConversionOptions::JaniConversionOptions() : edgeAssignments(false), flatten(false), substituteConstants(true), localVars(false), globalVars(false), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()), addPropertyConstants(true) {
             // Intentionally left empty
         }
 
-        JaniConversionOptions::JaniConversionOptions(storm::settings::modules::JaniExportSettings const& settings) : locationVariables(settings.getLocationVariables()), edgeAssignments(settings.isAllowEdgeAssignmentsSet()), flatten(settings.isExportFlattenedSet()), substituteConstants(true), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()), addPropertyConstants(true) {
+        JaniConversionOptions::JaniConversionOptions(storm::settings::modules::JaniExportSettings const& settings) : locationVariables(settings.getLocationVariables()), edgeAssignments(settings.isAllowEdgeAssignmentsSet()), flatten(settings.isExportFlattenedSet()), substituteConstants(true), localVars(settings.isLocalVarsSet()), globalVars(settings.isGlobalVarsSet()), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()), addPropertyConstants(true) {
             if (settings.isEliminateFunctionsSet()) {
                 allowedModelFeatures.remove(storm::jani::ModelFeature::Functions);
             }

src/storm-conv/converter/options/JaniConversionOptions.h

@@ -27,6 +27,12 @@ namespace storm {
             /// If set, constants in expressions are substituted with their definition
             bool substituteConstants;
             
+            /// If set, variables will be made local wherever possible
+            bool localVars;
+            
+            /// If set, variables will be made global wherever possible
+            bool globalVars;
+            
             /// If given, the model will get this name
             boost::optional<std::string> modelName;
             

src/storm-conv/settings/modules/JaniExportSettings.cpp

@@ -18,6 +18,7 @@ namespace storm {
             const std::string JaniExportSettings::exportFlattenOptionName = "flatten";
             const std::string JaniExportSettings::locationVariablesOptionName = "location-variables";
             const std::string JaniExportSettings::globalVariablesOptionName = "globalvars";
+            const std::string JaniExportSettings::localVariablesOptionName = "localvars";
             const std::string JaniExportSettings::compactJsonOptionName = "compactjson";
             const std::string JaniExportSettings::eliminateArraysOptionName = "remove-arrays";
             const std::string JaniExportSettings::eliminateFunctionsOptionName = "remove-functions";
@@ -27,6 +28,7 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, edgeAssignmentsOptionName, false, "If set, the output model can have transient edge assignments. This can simplify the jani model but is not compliant to the jani standard.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportFlattenOptionName, false, "Flattens the composition of Automata to obtain an equivalent model that contains exactly one automaton").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, globalVariablesOptionName, false, "If set, variables will preferably be made global, e.g., to guarantee the same variable order as in the input file.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, localVariablesOptionName, false, "If set, variables will preferably be made local.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, compactJsonOptionName, false, "If set, the size of the resulting jani file will be reduced at the cost of (human-)readability.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, eliminateArraysOptionName, false, "If set, transforms the model such that array variables/expressions are eliminated.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, eliminateFunctionsOptionName, false, "If set, transforms the model such that functions are eliminated.").build());
@@ -64,6 +66,10 @@ namespace storm {
                 return this->getOption(globalVariablesOptionName).getHasOptionBeenSet();
             }
 
+            bool JaniExportSettings::isLocalVarsSet() const {
+                return this->getOption(localVariablesOptionName).getHasOptionBeenSet();
+            }
+
             bool JaniExportSettings::isCompactJsonSet() const {
                 return this->getOption(compactJsonOptionName).getHasOptionBeenSet();
             }

src/storm-conv/settings/modules/JaniExportSettings.h

@@ -22,6 +22,8 @@ namespace storm {
                 
                 bool isGlobalVarsSet() const;
                 
+                bool isLocalVarsSet() const;
+                
                 bool isCompactJsonSet() const;
                 
                 bool isEliminateArraysSet() const;
@@ -40,6 +42,7 @@ namespace storm {
                 static const std::string exportFlattenOptionName;
                 static const std::string locationVariablesOptionName;
                 static const std::string globalVariablesOptionName;
+                static const std::string localVariablesOptionName;
                 static const std::string compactJsonOptionName;
                 static const std::string eliminateArraysOptionName;
                 static const std::string eliminateFunctionsOptionName;

src/storm/storage/jani/JaniLocationExpander.cpp

@@ -67,10 +67,8 @@ namespace storm {
                 for (int64_t i = variableLowerBound; i <= variableUpperBound; i++) {
                     std::string newLocationName = loc.getName() + "_" + variableName + "_" + std::to_string(i);
                     substitutionMap[eliminatedExpressionVariable] = original.getExpressionManager().integer(i);
-                    std::cout << "eliminate " << eliminatedExpressionVariable.getName() << " with " << i << std::endl;
                     OrderedAssignments newAssignments = loc.getAssignments().clone();
                     newAssignments.substitute(substitutionMap);
-                    std::cout << newAssignments << std::endl;
                     uint64_t newLocationIndex = newAutomaton.addLocation(Location(newLocationName, newAssignments));
 
                     locationVariableValueMap[origIndex][i] = newLocationIndex;

src/storm/storage/jani/JaniScopeChanger.cpp

@@ -0,0 +1,164 @@
+#include "storm/storage/jani/JaniScopeChanger.h"
+
+#include <map>
+#include <set>
+#include <boost/any.hpp>
+
+#include "storm/storage/expressions/Variable.h"
+#include "storm/storage/jani/Model.h"
+#include "storm/storage/jani/Property.h"
+#include "storm/storage/jani/traverser/JaniTraverser.h"
+
+namespace storm {
+    namespace jani {
+        
+        namespace detail {
+            class VariableAccessedTraverser : public ConstJaniTraverser {
+            public:
+                VariableAccessedTraverser(std::set<storm::expressions::Variable> const& varSet) : varSet(varSet) {
+                    // Intentionally left empty
+                }
+                using ConstJaniTraverser::traverse;
+                
+                virtual void traverse(storm::expressions::Expression const& expression, boost::any const& data) override {
+                    bool* result = boost::any_cast<bool *>(data);
+                    if (*result) { return; }
+                    *result = expression.containsVariable(varSet);
+                }
+                
+            private:
+                std::set<storm::expressions::Variable> const& varSet;
+            };
+            
+            std::set<uint64_t> getAutomataAccessingVariable(storm::expressions::Variable const& variable, Model const& model) {
+                std::set<uint64_t> res;
+                for (uint64_t i = 0; i < model.getNumberOfAutomata(); ++i) {
+                    if (model.getAutomaton(i).getVariables().hasVariable(variable)) {
+                        res.insert(i);
+                    } else {
+                        VariableAccessedTraverser vat({variable});
+                        bool varAccessed = false;
+                        vat.traverse(model.getAutomaton(i), &varAccessed);
+                        if (varAccessed) {
+                            res.insert(i);
+                        }
+                    }
+                }
+                return res;
+            }
+        }
+        
+        void JaniScopeChanger::makeVariableGlobal(storm::expressions::Variable const& variable, Model& model) const {
+            uint64_t automatonIndex = 0;
+            for (; automatonIndex < model.getNumberOfAutomata(); ++automatonIndex) {
+                if (model.getAutomaton(automatonIndex).getVariables().hasVariable(variable)) {
+                    break;
+                }
+            }
+            std::map<Variable const*, std::reference_wrapper<Variable const>> remapping;
+            auto oldJaniVar = model.getAutomaton(automatonIndex).getVariables().eraseVariable(variable);
+            remapping.emplace(oldJaniVar.get(), model.addVariable(*oldJaniVar));
+            
+            // Only one automaton accesses this variable
+            model.getAutomaton(automatonIndex).changeAssignmentVariables(remapping);
+        }
+        
+        void JaniScopeChanger::makeVariableLocal(storm::expressions::Variable const& variable, Model& model, uint64_t automatonIndex) const {
+            std::map<Variable const*, std::reference_wrapper<Variable const>> remapping;
+            auto oldJaniVar = model.getGlobalVariables().eraseVariable(variable);
+            remapping.emplace(oldJaniVar.get(), model.getAutomaton(automatonIndex).addVariable(*oldJaniVar));
+            // Only one automaton accesses this variable (otherwise this call would be illegal)
+            model.getAutomaton(automatonIndex).changeAssignmentVariables(remapping);
+        }
+        
+        bool JaniScopeChanger::canMakeVariableGlobal(storm::expressions::Variable const& variable, Model const& model) const {
+            if (model.hasGlobalVariable(variable.getName())) {
+                return false;
+            }
+            // Check whether there are multiple local variables with this name
+            bool foundVar = false;
+            for (auto const& aut : model.getAutomata()) {
+                if (aut.hasVariable(variable.getName())) {
+                    if (foundVar) {
+                        return false;
+                    }
+                    foundVar = true;
+                }
+            }
+            return foundVar;
+        }
+        
+        std::pair<bool, uint64_t> JaniScopeChanger::canMakeVariableLocal(storm::expressions::Variable const& variable, Model const& model, std::vector<Property> const& properties, boost::optional<uint64_t> automatonIndex) const {
+            uint64_t index = model.getNumberOfAutomata();
+            
+            if (!model.getGlobalVariables().hasVariable(variable)) {
+                return {false, index};
+            }
+            
+            auto accessingAutomata = detail::getAutomataAccessingVariable(variable, model);
+            if (accessingAutomata.size() > 1 || (automatonIndex.is_initialized() && accessingAutomata.count(automatonIndex.get()) == 0)) {
+                return {false, index};
+            }
+            if (model.getInitialStatesRestriction().containsVariable({variable})) {
+                return {false, index};
+            }
+            for (auto const& rewExp : model.getNonTrivialRewardExpressions()) {
+                if (rewExp.second.containsVariable({variable})) {
+                    return {false, index};
+                }
+            }
+            for (auto const& funDef : model.getGlobalFunctionDefinitions()) {
+                if (funDef.second.getFunctionBody().containsVariable({variable})) {
+                    return {false, index};
+                }
+            }
+            for (auto const& p : properties) {
+                if (p.getUsedVariablesAndConstants().count(variable) > 0) {
+                    return {false, index};
+                }
+                if (p.getUsedLabels().count(variable.getName()) > 0) {
+                    return {false, index};
+                }
+            }
+            
+            if (accessingAutomata.empty()) {
+                index = automatonIndex.is_initialized() ? automatonIndex.get() : 0;
+            } else {
+                index = *accessingAutomata.begin();
+                assert(!automatonIndex.is_initialized() || index == automatonIndex.get());
+            }
+            return {true, index};
+        }
+        
+        void JaniScopeChanger::makeVariablesGlobal(Model& model) const {
+            for (uint64_t i = 0; i < model.getNumberOfAutomata(); ++i) {
+                // Make sure to not erase from a set while iterating over it...
+                std::set<storm::expressions::Variable> varsToMakeGlobal;
+                for (auto const& v : model.getAutomaton(i).getVariables()) {
+                    if (canMakeVariableGlobal(v.getExpressionVariable(), model)) {
+                        varsToMakeGlobal.insert(v.getExpressionVariable());
+                    }
+                }
+                for (auto const& v : varsToMakeGlobal) {
+                    makeVariableGlobal(v, model);
+                }
+            }
+        }
+        
+        void JaniScopeChanger::makeVariablesLocal(Model& model, std::vector<Property> const& properties) const {
+            // Make sure to not erase from a set while iterating over it...
+            std::map<storm::expressions::Variable, uint64_t> varsToMakeLocal;
+            for (auto const& v : model.getGlobalVariables()) {
+                auto makeLocal = canMakeVariableLocal(v.getExpressionVariable(), model, properties);
+                if (makeLocal.first) {
+                    varsToMakeLocal[v.getExpressionVariable()] = makeLocal.second;
+                }
+            }
+            for (auto const& v : varsToMakeLocal) {
+                makeVariableLocal(v.first, model, v.second);
+            }
+        }
+        
+    }
+
+}

src/storm/storage/jani/JaniScopeChanger.h

@@ -0,0 +1,57 @@
+#pragma once
+
+#include <vector>
+#include <boost/optional.hpp>
+
+namespace storm {
+    
+    namespace expressions {
+        class Variable;
+    }
+    
+    namespace jani {
+        
+        class Model;
+        class Property;
+        
+        class JaniScopeChanger {
+        public:
+            JaniScopeChanger() = default;
+            
+            /*!
+             * Moves the given variable to the global scope.
+             * It is *not* checked whether this introduces name clashes
+             */
+            void makeVariableGlobal(storm::expressions::Variable const& variable, Model& model) const;
+            
+            /*!
+             * Moves the given variable into the local scope of the automaton with the given index.
+             * It is *not* checked whether this introduces out-of-scope accesses.
+             */
+            void makeVariableLocal(storm::expressions::Variable const& variable, Model& model, uint64_t automatonIndex) const;
+            
+            /*!
+             * Checks whether this variable can be made global without introducing name clashes.
+             */
+             bool canMakeVariableGlobal(storm::expressions::Variable const& variable, Model const& model) const;
+             
+            /*!
+             * Checks whether this variable can be made local without introducing out-of-scope accesses.
+             * Returns true if this is a case as well as an automaton index where to pout the variable
+             */
+             std::pair<bool, uint64_t> canMakeVariableLocal(storm::expressions::Variable const& variable, Model const& model, std::vector<Property> const& properties = {}, boost::optional<uint64_t> automatonIndex = boost::none) const;
+             
+            /*!
+             * Moves as many variables to the global scope as possible
+             */
+             void makeVariablesGlobal(Model& model) const;
+             
+            /*!
+             * Moves as many variables to a local scope as possible
+             */
+             void makeVariablesLocal(Model& model, std::vector<Property> const& properties = {}) const;
+             
+        };
+    }
+
+}

src/storm/storage/jani/LValue.cpp

@@ -50,14 +50,23 @@ namespace storm {
         
         LValue LValue::changeAssignmentVariables(std::map<Variable const*, std::reference_wrapper<Variable const>> const& remapping) const {
             if (isVariable()) {
-                return LValue(remapping.at(variable));
+                auto it = remapping.find(variable);
+                if (it == remapping.end()) {
+                    return *this;
+                } else {
+                    return LValue(it->second);
+                }
             } else {
                 STORM_LOG_ASSERT(isArrayAccess(), "Unhandled LValue.");
-                return LValue(LValue(remapping.at(variable)), arrayIndex);
+                auto it = remapping.find(variable);
+                if (it == remapping.end()) {
+                    return *this;
+                } else {
+                    return LValue(LValue(it->second), arrayIndex);
+                }
             }
         }
 
-        
         bool LValue::operator<(LValue const& other) const {
             if (isVariable()) {
                 return !other.isVariable() || variable->getExpressionVariable() < other.getVariable().getExpressionVariable();

src/storm/storage/jani/Property.cpp

@@ -70,6 +70,26 @@ namespace storm {
         bool Property::containsUndefinedConstants() const {
             return !undefinedConstants.empty();
         }
+ 
+        std::set<storm::expressions::Variable> Property::getUsedVariablesAndConstants() const {
+            auto res = getUndefinedConstants();
+            getFilter().getFormula()->gatherUsedVariables(res);
+            getFilter().getStatesFormula()->gatherUsedVariables(res);
+            return res;
+        }
+ 
+        std::set<std::string> Property::getUsedLabels() const {
+            std::set<std::string> res;
+            auto labFormSet = getFilter().getFormula()->getAtomicLabelFormulas();
+            for (auto const& f : labFormSet) {
+                res.insert(f->getLabel());
+            }
+            labFormSet = getFilter().getStatesFormula()->getAtomicLabelFormulas();
+            for (auto const& f : labFormSet) {
+                res.insert(f->getLabel());
+            }
+            return res;
+        }
         
         std::ostream& operator<<(std::ostream& os, Property const& p) {
             return os << "(" << p.getName() << "): " << p.getFilter();

src/storm/storage/jani/Property.h

@@ -129,8 +129,11 @@ namespace storm {
             
             std::set<storm::expressions::Variable> const& getUndefinedConstants() const;
             bool containsUndefinedConstants() const;
+            std::set<storm::expressions::Variable> getUsedVariablesAndConstants() const;
+            std::set<std::string> getUsedLabels() const;
             
             std::shared_ptr<storm::logic::Formula const> getRawFormula() const;
+            
         private:
             std::string name;
             std::string comment;

src/storm/storage/jani/VariableSet.cpp

@@ -196,6 +196,51 @@ namespace storm {
             return getVariable(it->second);
         }
 
+        template <typename VarType>
+        void eraseFromVariableVector(std::vector<std::shared_ptr<VarType>>& varVec, storm::expressions::Variable const& variable) {
+            for (auto vIt = varVec.begin(); vIt != varVec.end(); ++vIt) {
+                if ((*vIt)->getExpressionVariable() == variable) {
+                    varVec.erase(vIt);
+                    break;
+                }
+            }
+        }
+        
+        std::shared_ptr<Variable> VariableSet::eraseVariable(storm::expressions::Variable const& variable) {
+            auto vToVIt = variableToVariable.find(variable);
+            STORM_LOG_THROW(vToVIt != variableToVariable.end(), storm::exceptions::InvalidArgumentException, "Unable to erase unknown variable '" << variable.getName() << "'.");
+            std::shared_ptr<Variable> janiVar = std::move(vToVIt->second);
+            variableToVariable.erase(vToVIt);
+            
+            nameToVariable.erase(variable.getName());
+            eraseFromVariableVector(variables, variable);
+            if (janiVar->isBooleanVariable()) {
+                eraseFromVariableVector(booleanVariables, variable);
+            }
+            if (janiVar->isBooleanVariable()) {
+                eraseFromVariableVector(booleanVariables, variable);
+            }
+            if (janiVar->isBoundedIntegerVariable()) {
+                eraseFromVariableVector(boundedIntegerVariables, variable);
+            }
+            if (janiVar->isUnboundedIntegerVariable()) {
+                eraseFromVariableVector(unboundedIntegerVariables, variable);
+            }
+            if (janiVar->isRealVariable()) {
+                eraseFromVariableVector(realVariables, variable);
+            }
+            if (janiVar->isArrayVariable()) {
+                eraseFromVariableVector(arrayVariables, variable);
+            }
+            if (janiVar->isClockVariable()) {
+                eraseFromVariableVector(clockVariables, variable);
+            }
+            if (janiVar->isTransient()) {
+                eraseFromVariableVector(transientVariables, variable);
+            }
+            return janiVar;
+        }
+
         typename detail::Variables<Variable>::iterator VariableSet::begin() {
             return detail::Variables<Variable>::make_iterator(variables.begin());
         }

src/storm/storage/jani/VariableSet.h

@@ -153,6 +153,11 @@ namespace storm {
              * Retrieves the variable object associated with the given expression variable (if any).
              */
             Variable const& getVariable(storm::expressions::Variable const& variable) const;
+            
+            /*!
+             * Erases the given variable from this set.
+             */
+             std::shared_ptr<Variable> eraseVariable(storm::expressions::Variable const& variable);
 
             /*!
              * Retrieves whether this variable set contains a transient variable.