Jani: Check if a variable is never used as the lvalue of an assignment. If yes, (and if the variable has a known initial value), we replace the variable by a constant.

src/storm/storage/jani/Model.cpp

@@ -18,6 +18,7 @@
 #include "storm/storage/jani/JSONExporter.h"
 #include "storm/storage/jani/ArrayEliminator.h"
 #include "storm/storage/jani/FunctionEliminator.h"
+#include "storm/storage/jani/VariablesToConstantsTransformer.h"
 #include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h"
 
 #include "storm/storage/expressions/LinearityCheckVisitor.h"
@@ -638,7 +639,6 @@ namespace storm {
             return constantToIndex.find(name) != constantToIndex.end();
         }
 
-
         void Model::removeConstant(std::string const& name) {
             auto pos = constantToIndex.find(name);
             if (pos != constantToIndex.end()) {
@@ -1025,12 +1025,16 @@ namespace storm {
             return result;
         }
         
-        Model Model::substituteConstants() const {
-            Model result(*this);
+        Model& Model::replaceUnassignedVariablesWithConstants() {
+            VariablesToConstantsTransformer().transform(*this);
+            return *this;
+        }
+        
+        Model& Model::substituteConstantsInPlace() {
 
             // Gather all defining expressions of constants.
             std::map<storm::expressions::Variable, storm::expressions::Expression> constantSubstitution;
-            for (auto& constant : result.getConstants()) {
+            for (auto& constant : this->getConstants()) {
                 if (constant.hasConstraint()) {
                     constant.setConstraintExpression(substituteJaniExpression(constant.getConstraintExpression(), constantSubstitution));
                 }
@@ -1040,30 +1044,38 @@ namespace storm {
                 }
             }
             
-            for (auto& functionDefinition : result.getGlobalFunctionDefinitions()) {
+            for (auto& functionDefinition : this->getGlobalFunctionDefinitions()) {
                 functionDefinition.second.substitute(constantSubstitution);
             }
             
             // Substitute constants in all global variables.
-            result.getGlobalVariables().substitute(constantSubstitution);
+            this->getGlobalVariables().substitute(constantSubstitution);
             
             // Substitute constants in initial states expression.
-            result.setInitialStatesRestriction(substituteJaniExpression(this->getInitialStatesRestriction(), constantSubstitution));
+            this->setInitialStatesRestriction(substituteJaniExpression(this->getInitialStatesRestriction(), constantSubstitution));
             
-            for (auto& rewMod : result.getNonTrivialRewardExpressions()) {
+            for (auto& rewMod : this->getNonTrivialRewardExpressions()) {
                 rewMod.second = substituteJaniExpression(rewMod.second, constantSubstitution);
             }
             
             // Substitute constants in variables of automata and their edges.
-            for (auto& automaton : result.getAutomata()) {
+            for (auto& automaton : this->getAutomata()) {
                 automaton.substitute(constantSubstitution);
             }
             
+            return *this;
+        }
+        
+        Model Model::substituteConstants() const {
+            Model result(*this);
+            result.substituteConstantsInPlace();
             return result;
         }
         
         Model Model::substituteConstantsFunctions() const {
-            auto result = substituteConstants();
+            Model result(*this);
+            result.replaceUnassignedVariablesWithConstants();
+            result.substituteConstantsInPlace();
             result.substituteFunctions();
             return result;
         }

src/storm/storage/jani/Model.h

@@ -427,6 +427,16 @@ namespace storm {
              */
             std::vector<std::reference_wrapper<Constant const>> getUndefinedConstants() const;
             
+            /*!
+             * Replaces each variable to which we never assign a value with a constant.
+             */
+            Model& replaceUnassignedVariablesWithConstants();
+            
+            /*!
+             * Substitutes all constants in all expressions of the model.
+             */
+            Model& substituteConstantsInPlace();
+            
             /*!
              * Substitutes all constants in all expressions of the model. The original model is not modified, but
              * instead a new model is created.
@@ -453,8 +463,10 @@ namespace storm {
             void substituteFunctions(std::vector<Property>& properties);
             
             /*!
-             * Substitutes all constants in all expressions of the model. The original model is not modified, but
-             * instead a new model is created. Afterwards, all function calls are substituted with the defining expression.
+             * 1. Tries to replace variables by constants (if possible).
+             * 2. Substitutes all constants in all expressions of the model.
+             * 3. Afterwards, all function calls are substituted with the defining expression.
+             * The original model is not modified, but  instead a new model is created.
              */
             Model substituteConstantsFunctions() const;
 

src/storm/storage/jani/VariablesToConstantsTransformer.cpp

@@ -0,0 +1,73 @@
+#include "storm/storage/jani/VariablesToConstantsTransformer.h"
+
+#include "storm/storage/jani/Constant.h"
+#include "storm/storage/jani/Variable.h"
+#include "storm/storage/jani/Model.h"
+#include "storm/storage/jani/traverser/AssignmentsFinder.h"
+
+#include "storm/storage/expressions/Expressions.h"
+#include "storm/storage/jani/expressions/JaniExpressions.h"
+#include "storm/storage/expressions/ExpressionManager.h"
+#include "storm/exceptions/UnexpectedException.h"
+
+namespace storm {
+    
+    
+    
+    namespace jani {
+        namespace detail {
+            storm::jani::Constant createConstantFromVariable(storm::jani::Variable const& variable) {
+                STORM_LOG_ASSERT(variable.hasInitExpression(), "Trying to convert variable " << variable.getName() << " to a constant, but the variable does not have an initial value.");
+                // For the name we use the name of the expression variable to assert uniqueness.
+                return storm::jani::Constant(variable.getExpressionVariable().getName(), variable.getExpressionVariable(), variable.getInitExpression());
+            }
+            
+            template <typename JaniStructureType>
+            bool canTransformVariable(storm::jani::Variable const& variable, JaniStructureType const& janiStructure) {
+                // It does not make sense to do this for transient variables.
+                if (variable.isTransient()) {
+                    return false;
+                }
+                // The variable should have a known initial value.
+                if (!variable.hasInitExpression()) {
+                    return false;
+                }
+                // Finally, there should be no assignment that assignes a value to this variable.
+                auto assignmentTypes = storm::jani::AssignmentsFinder().find(janiStructure, variable);
+                return !assignmentTypes.hasEdgeAssignment && !assignmentTypes.hasEdgeDestinationAssignment && !assignmentTypes.hasLocationAssignment;
+            }
+        } // namespace detail
+        
+        void VariablesToConstantsTransformer::transform(Model& model) {
+            // It is dangerous to erase a variable from a set of variables while iterating over the set.
+            // Therefore, we store the variables and erase them later.
+            std::vector<storm::expressions::Variable> variablesToErase;
+            for (auto const& globalVar : model.getGlobalVariables()) {
+                if (detail::canTransformVariable(globalVar, model)) {
+                    variablesToErase.push_back(globalVar.getExpressionVariable());
+                }
+            }
+            for (auto const& varToErase : variablesToErase) {
+                STORM_LOG_INFO("Transformed Variable " << varToErase.getName() << " to a constant since it is not assigned any value.");
+                auto erasedJaniVariable = model.getGlobalVariables().eraseVariable(varToErase);
+                auto createdConstant = detail::createConstantFromVariable(*erasedJaniVariable);
+                model.addConstant(createdConstant);
+            }
+            for (auto& aut : model.getAutomata()) {
+                variablesToErase.clear();
+                for (auto const& localVar : aut.getVariables()) {
+                    if (detail::canTransformVariable(localVar, aut)) {
+                        variablesToErase.push_back(localVar.getExpressionVariable());
+                    }
+                }
+                for (auto const& varToErase : variablesToErase) {
+                    STORM_LOG_INFO("Transformed Variable " << varToErase.getName() << " to a constant since it is not assigned any value.");
+                    auto erasedJaniVariable = aut.getVariables().eraseVariable(varToErase);
+                    auto createdConstant = detail::createConstantFromVariable(*erasedJaniVariable);
+                    model.addConstant(createdConstant);
+                }
+            }
+        }
+    }
+}
+

src/storm/storage/jani/VariablesToConstantsTransformer.h

@@ -0,0 +1,24 @@
+#pragma once
+
+
+namespace storm {
+    namespace expressions {
+        class Expression;
+    }
+    
+    namespace jani {
+        class Model;
+        
+        class VariablesToConstantsTransformer {
+        public:
+            VariablesToConstantsTransformer() = default;
+            
+            /*!
+             * Replaces each variable to which we never assign a value with a constant.
+             */
+            void transform(Model& model);
+
+        };
+    }
+}
+

src/storm/storage/jani/traverser/AssignmentsFinder.cpp

@@ -9,6 +9,10 @@ namespace storm {
             return find(model, variable.getExpressionVariable());
         }
         
+        AssignmentsFinder::ResultType AssignmentsFinder::find(Automaton const& automaton, storm::jani::Variable const& variable) {
+            return find(automaton, variable.getExpressionVariable());
+        }
+
         AssignmentsFinder::ResultType AssignmentsFinder::find(Model const& model, storm::expressions::Variable const& variable) {
             ResultType res;
             res.hasLocationAssignment = false;
@@ -18,6 +22,15 @@ namespace storm {
             return res;
         }
         
+        AssignmentsFinder::ResultType AssignmentsFinder::find(Automaton const& automaton, storm::expressions::Variable const& variable) {
+            ResultType res;
+            res.hasLocationAssignment = false;
+            res.hasEdgeAssignment = false;
+            res.hasEdgeDestinationAssignment = false;
+            ConstJaniTraverser::traverse(automaton, std::make_pair(&variable, &res));
+            return res;
+        }
+        
         void AssignmentsFinder::traverse(Location const& location, boost::any const& data) {
             auto resVar = boost::any_cast<std::pair<storm::expressions::Variable const*, ResultType*>>(data);
             if (!resVar.second->hasLocationAssignment) {

src/storm/storage/jani/traverser/AssignmentsFinder.h

@@ -22,7 +22,9 @@ namespace storm {
             AssignmentsFinder() = default;
             
             ResultType find(Model const& model, storm::jani::Variable const& variable);
+            ResultType find(Automaton const& automaton, storm::jani::Variable const& variable);
             ResultType find(Model const& model, storm::expressions::Variable const& variable);
+            ResultType find(Automaton const& automaton, storm::expressions::Variable const& variable);
             
             virtual ~AssignmentsFinder() = default;