jani expression substitution now also works for array expressions

src/storm/storage/SymbolicModelDescription.cpp

@@ -150,9 +150,6 @@ namespace storm {
         SymbolicModelDescription SymbolicModelDescription::preprocess(std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) const {
             if (this->isJaniModel()) {
                 storm::jani::Model preparedModel = this->asJaniModel().defineUndefinedConstants(constantDefinitions).substituteConstants();
-                if (preparedModel.hasArrayVariables()) {
-                    preparedModel = preparedModel.convertArrays();
-                }
                 return SymbolicModelDescription(preparedModel);
             } else if (this->isPrismProgram()) {
                 return SymbolicModelDescription(this->asPrismProgram().defineUndefinedConstants(constantDefinitions).substituteConstants());

src/storm/storage/jani/Assignment.cpp

@@ -1,6 +1,7 @@
 #include "storm/storage/jani/Assignment.h"
 
 #include "storm/storage/jani/LValue.h"
+#include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h"
 
 #include "storm/storage/expressions/LinearityCheckVisitor.h"
 
@@ -51,9 +52,9 @@ namespace storm  {
         }
         
         void Assignment::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
-            this->setAssignedExpression(this->getAssignedExpression().substitute(substitution).simplify());
+            this->setAssignedExpression(substituteJaniExpression(this->getAssignedExpression(), substitution).simplify());
             if (lValue.isArrayAccess()) {
-                lValue = LValue(LValue(lValue.getArray()), lValue.getArrayIndex().substitute(substitution).simplify());
+                lValue = LValue(LValue(lValue.getArray()), substituteJaniExpression(lValue.getArrayIndex(), substitution).simplify());
             }
         }
         

src/storm/storage/jani/Automaton.cpp

@@ -3,6 +3,7 @@
 #include "storm/storage/jani/Edge.h"
 #include "storm/storage/jani/TemplateEdge.h"
 #include "storm/storage/jani/Location.h"
+#include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h"
 
 #include "storm/utility/macros.h"
 #include "storm/exceptions/WrongFormatException.h"
@@ -387,7 +388,7 @@ namespace storm {
                 location.substitute(substitution);
             }
             
-            this->setInitialStatesRestriction(this->getInitialStatesRestriction().substitute(substitution));
+            this->setInitialStatesRestriction(substituteJaniExpression(this->getInitialStatesRestriction(), substitution));
             
             edges.substitute(substitution);
         }

src/storm/storage/jani/BoundedIntegerVariable.cpp

@@ -1,5 +1,6 @@
 #include "storm/storage/jani/BoundedIntegerVariable.h"
 #include "storm/exceptions/NotImplementedException.h"
+#include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h"
 #include "storm/utility/macros.h"
 
 namespace storm {
@@ -47,8 +48,8 @@ namespace storm {
         
         void BoundedIntegerVariable::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
             Variable::substitute(substitution);
-            this->setLowerBound(this->getLowerBound().substitute(substitution));
-            this->setUpperBound(this->getUpperBound().substitute(substitution));
+            this->setLowerBound(substituteJaniExpression(this->getLowerBound(), substitution));
+            this->setUpperBound(substituteJaniExpression(this->getUpperBound(), substitution));
         }
         
         std::shared_ptr<BoundedIntegerVariable> makeBoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, boost::optional<storm::expressions::Expression> initValue, bool transient, boost::optional<storm::expressions::Expression> lowerBound, boost::optional<storm::expressions::Expression> upperBound) {

src/storm/storage/jani/Edge.cpp

@@ -1,6 +1,7 @@
 #include "storm/storage/jani/Edge.h"
 
 #include "storm/storage/jani/Model.h"
+#include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h"
 
 #include "storm/utility/macros.h"
 #include "storm/exceptions/InvalidArgumentException.h"
@@ -76,7 +77,7 @@ namespace storm {
         
         void Edge::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
             if (this->hasRate()) {
-                this->setRate(this->getRate().substitute(substitution));
+                this->setRate(substituteJaniExpression(this->getRate(), substitution));
             }
             for (auto& destination : destinations) {
                 destination.substitute(substitution);

src/storm/storage/jani/EdgeDestination.cpp

@@ -1,6 +1,8 @@
 #include "storm/storage/jani/EdgeDestination.h"
 
 #include "storm/utility/macros.h"
+#include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h"
+
 #include "storm/exceptions/WrongFormatException.h"
 
 namespace storm {
@@ -37,7 +39,7 @@ namespace storm {
         }
         
         void EdgeDestination::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
-            this->setProbability(this->getProbability().substitute(substitution));
+            this->setProbability(substituteJaniExpression(this->getProbability(), substitution));
         }
         
         bool EdgeDestination::hasAssignment(Assignment const& assignment) const {

src/storm/storage/jani/JaniLocationExpander.cpp

@@ -1,5 +1,7 @@
 #include "storm/storage/jani/JaniLocationExpander.h"
 
+#include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h"
+
 #include "storm/storage/expressions/ExpressionManager.h"
 #include "storm/exceptions/NotSupportedException.h"
 #include "storm/exceptions/IllegalArgumentException.h"
@@ -83,7 +85,7 @@ namespace storm {
                     substitutionMap[eliminatedExpressionVariable] = original.getExpressionManager().integer(newValueAndLocation.first);
 
                     uint64_t newSourceIndex = newValueAndLocation.second;
-                    storm::expressions::Expression newGuard = edge.getGuard().substitute(substitutionMap).simplify();
+                    storm::expressions::Expression newGuard = substituteJaniExpression(edge.getGuard(), substitutionMap).simplify();
                     if (!newGuard.containsVariables() && !newGuard.evaluateAsBool()) {
                         continue;
                     }
@@ -105,9 +107,9 @@ namespace storm {
                         }
                         TemplateEdgeDestination ted(oa);
                         templateEdge->addDestination(ted);
-                        destinationLocationsAndProbabilities.emplace_back(locationVariableValueMap[destination.getLocationIndex()][value], destination.getProbability().substitute((substitutionMap)));
+                        destinationLocationsAndProbabilities.emplace_back(locationVariableValueMap[destination.getLocationIndex()][value], substituteJaniExpression(destination.getProbability(), substitutionMap));
                     }
-                    newAutomaton.addEdge(storm::jani::Edge(newSourceIndex, edge.getActionIndex(), edge.hasRate() ? boost::optional<storm::expressions::Expression>(edge.getRate().substitute(substitutionMap)) : boost::none, templateEdge, destinationLocationsAndProbabilities));
+                    newAutomaton.addEdge(storm::jani::Edge(newSourceIndex, edge.getActionIndex(), edge.hasRate() ? boost::optional<storm::expressions::Expression>(substituteJaniExpression(edge.getRate(), substitutionMap)) : boost::none, templateEdge, destinationLocationsAndProbabilities));
 
                 }
             }

src/storm/storage/jani/Model.cpp

@@ -16,6 +16,8 @@
 #include "storm/storage/jani/CompositionInformationVisitor.h"
 #include "storm/storage/jani/Compositions.h"
 #include "storm/storage/jani/JSONExporter.h"
+#include "storm/storage/jani/traverser/ArrayEliminator.h"
+#include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h"
 
 #include "storm/storage/expressions/LinearityCheckVisitor.h"
 
@@ -896,7 +898,7 @@ namespace storm {
             std::map<storm::expressions::Variable, storm::expressions::Expression> constantSubstitution;
             for (auto& constant : result.getConstants()) {
                 if (constant.isDefined()) {
-                    constant.define(constant.getExpression().substitute(constantSubstitution));
+                    constant.define(substituteJaniExpression(constant.getExpression(), constantSubstitution));
                     constantSubstitution[constant.getExpressionVariable()] = constant.getExpression();
                 }
             }
@@ -910,7 +912,7 @@ namespace storm {
             }
             
             // Substitute constants in initial states expression.
-            result.setInitialStatesRestriction(this->getInitialStatesRestriction().substitute(constantSubstitution));
+            result.setInitialStatesRestriction(substituteJaniExpression(this->getInitialStatesRestriction(), constantSubstitution));
             
             // Substitute constants in variables of automata and their edges.
             for (auto& automaton : result.getAutomata()) {
@@ -932,13 +934,21 @@ namespace storm {
             return result;
         }
         
-        bool Model::hasArrayVariables() const {
-            return getExpressionManager().getNumberOfArrayVariables() != 0;
+        bool Model::containsArrayVariables() const {
+            if (getGlobalVariables().containsArrayVariables()) {
+                return true;
+            }
+            for (auto const& a : getAutomata()) {
+                if (a.getVariables().containsArrayVariables()) {
+                    return true;
+                }
+            }
+            return false;
         }
         
-        Model Model::convertArrays() const {
-            std::cout << "TODO";
-            return *this;
+        void Model::eliminateArrays(bool keepNonTrivialArrayAccess) {
+            ArrayEliminator arrayEliminator;
+            arrayEliminator.eliminate(*this);
         }
         
         void Model::setInitialStatesRestriction(storm::expressions::Expression const& initialStatesRestriction) {

src/storm/storage/jani/Model.h

@@ -360,12 +360,13 @@ namespace storm {
             /*!
              * Returns true if at least one array variable occurs in the model.
              */
-            bool hasArrayVariables() const;
+            bool containsArrayVariables() const;
             
             /*!
-             * Converts occurring (fixed size) arrays into multiple variables.
+             * Eliminates occurring array variables and expressions by replacing array variables by multiple basic variables.
+             * @param keepNonTrivialArrayAccess if set, array access expressions in LValues and expressions are only replaced, if the index expression is constant.
              */
-            Model convertArrays() const;
+            void eliminateArrays(bool keepNonTrivialArrayAccess = false);
             
             /*!
              * Retrieves whether there is an expression restricting the legal initial values of the global variables.

src/storm/storage/jani/TemplateEdge.cpp

@@ -4,6 +4,7 @@
 #include "storm/storage/jani/LValue.h"
 
 #include "storm/storage/expressions/LinearityCheckVisitor.h"
+#include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h"
 
 namespace storm {
     namespace jani {
@@ -61,7 +62,7 @@ namespace storm {
         }
         
         void TemplateEdge::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
-            guard = guard.substitute(substitution);
+            guard = substituteJaniExpression(guard, substitution);
 
             for (auto& assignment : assignments) {
                 assignment.substitute(substitution);

src/storm/storage/jani/Variable.cpp

@@ -5,6 +5,7 @@
 #include "storm/storage/jani/UnboundedIntegerVariable.h"
 #include "storm/storage/jani/RealVariable.h"
 #include "storm/storage/jani/ArrayVariable.h"
+#include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h"
 
 namespace storm {
     namespace jani {
@@ -111,7 +112,7 @@ namespace storm {
         
         void Variable::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
             if (this->hasInitExpression()) {
-                this->setInitExpression(this->getInitExpression().substitute(substitution));
+                this->setInitExpression(substituteJaniExpression(this->getInitExpression(), substitution));
             }
         }
 

src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.cpp

@@ -3,6 +3,17 @@
 #include "storm/exceptions/InvalidArgumentException.h"
 
 namespace storm {
+    
+    namespace jani {
+        storm::expressions::Expression substituteJaniExpression(storm::expressions::Expression const& expression, std::map<storm::expressions::Variable, storm::expressions::Expression> const& identifierToExpressionMap) {
+            return JaniExpressionSubstitutionVisitor<std::map<storm::expressions::Variable, storm::expressions::Expression>>(identifierToExpressionMap).substitute(expression);
+        }
+        
+        storm::expressions::Expression substituteJaniExpression(storm::expressions::Expression const& expression, std::unordered_map<storm::expressions::Variable, storm::expressions::Expression> const& identifierToExpressionMap) {
+            return JaniExpressionSubstitutionVisitor<std::unordered_map<storm::expressions::Variable, storm::expressions::Expression>>(identifierToExpressionMap).substitute(expression);
+        }
+    }
+    
     namespace expressions {
         template<typename MapType>
         boost::any JaniExpressionSubstitutionVisitor<MapType>::visit(ValueArrayExpression const& expression, boost::any const& data) {

src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h

@@ -5,6 +5,12 @@
 #include "storm/storage/jani/expressions/JaniExpressionVisitor.h"
 
 namespace storm {
+    
+    namespace jani {
+        storm::expressions::Expression substituteJaniExpression(storm::expressions::Expression const& expression, std::map<storm::expressions::Variable, storm::expressions::Expression> const& identifierToExpressionMap);
+        storm::expressions::Expression substituteJaniExpression(storm::expressions::Expression const& expression, std::unordered_map<storm::expressions::Variable, storm::expressions::Expression> const& identifierToExpressionMap);
+    }
+    
     namespace expressions {
         template<typename MapType>
         class JaniExpressionSubstitutionVisitor : public SubstitutionVisitor<MapType>, public JaniExpressionVisitor {