jani-array fixes

src/storm-parsers/parser/JaniParser.cpp

@@ -24,7 +24,7 @@
 #include <sstream>
 #include <fstream>
 #include <boost/lexical_cast.hpp>
-#include <storm/storage/jani/ArrayVariable.h>
+#include "storm/storage/jani/ArrayVariable.h"
 
 #include "storm/utility/macros.h"
 #include "storm/utility/file.h"
@@ -1299,8 +1299,7 @@ namespace storm {
                         for (auto const& assignmentEntry : destEntry.at("assignments")) {
                             // ref
                             STORM_LOG_THROW(assignmentEntry.count("ref") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "'  must have one ref field");
-                            std::string refstring = getString(assignmentEntry.at("ref"), "assignment in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'");
-                            storm::jani::LValue lValue = parseLValue(refstring, "Assignment variable in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'", globalVars, constants, localVars);
+                            storm::jani::LValue lValue = parseLValue(assignmentEntry.at("ref"), "Assignment variable in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'", globalVars, constants, localVars);
                             // value
                             STORM_LOG_THROW(assignmentEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "'  must have one value field");
                             storm::expressions::Expression assignmentExpr = parseExpression(assignmentEntry.at("value"), "assignment in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'",  globalVars, constants, localVars);

src/storm/storage/jani/Assignment.cpp

@@ -15,7 +15,7 @@ namespace storm  {
         }
         
         bool Assignment::operator==(Assignment const& other) const {
-            return this->isTransient() == other.isTransient() && this->getExpressionVariable() == other.getExpressionVariable() && this->getAssignedExpression().isSyntacticallyEqual(other.getAssignedExpression()) && this->getLevel() == other.getLevel();
+            return this->isTransient() == other.isTransient() && this->getLValue() == other.getLValue() && this->getAssignedExpression().isSyntacticallyEqual(other.getAssignedExpression()) && this->getLevel() == other.getLevel();
         }
         
         bool Assignment::lValueIsVariable() const {

src/storm/storage/jani/Automaton.cpp

@@ -33,6 +33,8 @@ namespace storm {
                 return addVariable(variable.asUnboundedIntegerVariable());
             } else if (variable.isRealVariable()) {
                 return addVariable(variable.asRealVariable());
+            } else if (variable.isArrayVariable()) {
+                return addVariable(variable.asArrayVariable());
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Variable has invalid type.");
             }
@@ -54,6 +56,10 @@ namespace storm {
             return variables.addVariable(variable);
         }
         
+        ArrayVariable const& Automaton::addVariable(ArrayVariable const& variable) {
+            return variables.addVariable(variable);
+        }
+
         bool Automaton::hasVariable(std::string const& name) const {
             return variables.hasVariable(name);
         }

src/storm/storage/jani/Automaton.h

@@ -70,6 +70,11 @@ namespace storm {
              */
             RealVariable const& addVariable(RealVariable const& variable);
 
+            /*!
+             * Adds the given array variable to this automaton.
+             */
+            ArrayVariable const& addVariable(ArrayVariable const& variable);
+
             /*!
              * Retrieves the variables of this automaton.
              */

src/storm/storage/jani/LValue.cpp

@@ -62,9 +62,9 @@ namespace storm {
                     return false;
                 }
                 STORM_LOG_ASSERT(other.isArrayAccess(), "Unhandled LValue.");
-                if (variable->getExpressionVariable() < other.getVariable().getExpressionVariable()) {
+                if (getArray().getExpressionVariable() < other.getArray().getExpressionVariable()) {
                     return true;
-                } else if (other.getVariable().getExpressionVariable() < variable->getExpressionVariable()) {
+                } else if (other.getArray().getExpressionVariable() < getArray().getExpressionVariable()) {
                     return false;
                 } else {
                     return std::less<storm::expressions::Expression>()(arrayIndex, other.getArrayIndex());

src/storm/storage/jani/Model.cpp

@@ -634,6 +634,8 @@ namespace storm {
                 return addVariable(variable.asUnboundedIntegerVariable());
             } else if (variable.isRealVariable()) {
                 return addVariable(variable.asRealVariable());
+            } else if (variable.isArrayVariable()) {
+                return addVariable(variable.asArrayVariable());
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Variable has invalid type.");
             }
@@ -655,6 +657,10 @@ namespace storm {
             return globalVariables.addVariable(variable);
         }
         
+        ArrayVariable const& Model::addVariable(ArrayVariable const& variable) {
+            return globalVariables.addVariable(variable);
+        }
+
         VariableSet& Model::getGlobalVariables() {
             return globalVariables;
         }
@@ -899,6 +905,9 @@ namespace storm {
             for (auto& variable : result.getGlobalVariables().getBoundedIntegerVariables()) {
                 variable.substitute(constantSubstitution);
             }
+            for (auto& variable : result.getGlobalVariables().getArrayVariables()) {
+                variable.substitute(constantSubstitution);
+            }
             
             // Substitute constants in initial states expression.
             result.setInitialStatesRestriction(this->getInitialStatesRestriction().substitute(constantSubstitution));
@@ -993,6 +1002,7 @@ namespace storm {
             for (auto const& variable : this->getGlobalVariables().getBoundedIntegerVariables()) {
                 result.push_back(variable.getRangeExpression());
             }
+            STORM_LOG_ASSERT(this->getGlobalVariables().getArrayVariables().empty(), "This operation is unsupported if array variables are present.");
             
             if (automata.empty()) {
                 for (auto const& automaton : this->getAutomata()) {

src/storm/storage/jani/Model.h

@@ -190,6 +190,11 @@ namespace storm {
              */
             RealVariable const& addVariable(RealVariable const& variable);
 
+            /*!
+             * Adds the given array variable to this model.
+             */
+            ArrayVariable const& addVariable(ArrayVariable const& variable);
+
             /*!
              * Retrieves the variables of this automaton.
              */

src/storm/storage/jani/OrderedAssignments.cpp

@@ -35,8 +35,8 @@ namespace storm {
             auto it = lowerBound(assignment, allAssignments);
             
             // Check if an assignment to this variable is already present
-            if (it != allAssignments.end() && assignment.getExpressionVariable() == (*it)->getExpressionVariable()) {
-                STORM_LOG_THROW(addToExisting && assignment.getExpressionVariable().hasNumericalType(), storm::exceptions::InvalidArgumentException, "Cannot add assignment ('" << assignment.getAssignedExpression() << "') as an assignment ('" << (*it)->getAssignedExpression()  << "') to variable '" <<  (*it)->getVariable().getName() << "' already exists.");
+            if (it != allAssignments.end() && assignment.getLValue() == (*it)->getLValue()) {
+                STORM_LOG_THROW(addToExisting && assignment.getLValue().isVariable() && assignment.getExpressionVariable().hasNumericalType(), storm::exceptions::InvalidArgumentException, "Cannot add assignment ('" << assignment.getAssignedExpression() << "') as an assignment ('" << (*it)->getAssignedExpression()  << "') to LValue '" <<  (*it)->getLValue() << "' already exists.");
                 (*it)->setAssignedExpression((*it)->getAssignedExpression() + assignment.getAssignedExpression());
             } else {
                 // Finally, insert the new element in the correct vectors.
@@ -125,18 +125,19 @@ namespace storm {
             if (first) {
                 std::vector<Assignment> newAssignments;
                 for (uint64_t i = 0; i < allAssignments.size(); ++i) {
-                    if (synchronous && !localVars.hasVariable(allAssignments.at(i)->getVariable())) {
+                    auto const& iLValue = allAssignments.at(i)->getLValue();
+                    if (synchronous && !localVars.hasVariable(iLValue.isVariable() ? iLValue.getVariable() : iLValue.getArray())) {
                         newAssignments.push_back(*(allAssignments.at(i)));
                         continue;
                     }
                     bool readBeforeWrite = true;
                     for (uint64_t j = i + 1; j < allAssignments.size(); ++j) {
                         if (allAssignments.at(j)->getAssignedExpression().containsVariable(
-                                {allAssignments.at(i)->getVariable().getExpressionVariable()})) {
+                                {iLValue.isVariable() ? iLValue.getVariable().getExpressionVariable() : iLValue.getArray().getExpressionVariable()})) {
                             // is read.
                             break;
                         }
-                        if (allAssignments.at(j)->getVariable() == allAssignments.at(i)->getVariable()) {
+                        if (iLValue == allAssignments.at(j)->getLValue()) {
                             // is written, has not been read before
                             readBeforeWrite = false;
                             break;
@@ -158,15 +159,15 @@ namespace storm {
             std::vector<Assignment> newAssignments;
             for (auto const& assignment : allAssignments) {
                 newAssignments.push_back(*assignment);
-                if (synchronous && !localVars.hasVariable(assignment->getVariable())) {
+                if (synchronous && !localVars.hasVariable(assignment->getLValue().isVariable() ? assignment->getLValue().getVariable() : assignment->getLValue().getArray())) {
                     continue;
                 }
                 if (assignment->getLevel() == 0) {
                     continue;
                 }
                 uint64_t assNr = upperBound(assignment->getLevel() - 1);
-                if (assNr == isWrittenBeforeAssignment(assignment->getVariable(), assNr)) {
-                    if (assNr == isReadBeforeAssignment(assignment->getVariable(), assNr)) {
+                if (assNr == isWrittenBeforeAssignment(assignment->getLValue(), assNr)) {
+                    if (assNr == isReadBeforeAssignment(assignment->getLValue(), assNr)) {
                         newAssignments.back().setLevel(0);
                         changed = true;
                     }
@@ -230,7 +231,10 @@ namespace storm {
             return std::lower_bound(assignments.begin(), assignments.end(), assignment, storm::jani::AssignmentPartialOrderByLevelAndLValue());
         }
 
-        uint64_t OrderedAssignments::isReadBeforeAssignment(Variable const& var, uint64_t assignmentNumber, uint64_t start) const {
+        uint64_t OrderedAssignments::isReadBeforeAssignment(LValue const& lValue, uint64_t assignmentNumber, uint64_t start) const {
+            Variable const& var = lValue.isVariable() ? lValue.getVariable() : lValue.getArray();
+            // TODO: do this more carefully
+            STORM_LOG_WARN_COND(lValue.isVariable(), "Called a method that is not optimized for arrays.");
             for (uint64_t i = start; i < assignmentNumber; i++) {
                 if (allAssignments.at(i)->getAssignedExpression().containsVariable({ var.getExpressionVariable() })) {
                     return i;
@@ -239,9 +243,9 @@ namespace storm {
             return assignmentNumber;
         }
 
-        uint64_t OrderedAssignments::isWrittenBeforeAssignment(Variable const& var, uint64_t assignmentNumber, uint64_t start) const {
+        uint64_t OrderedAssignments::isWrittenBeforeAssignment(LValue const& lValue, uint64_t assignmentNumber, uint64_t start) const {
             for (uint64_t i = start; i < assignmentNumber; i++) {
-                if (allAssignments.at(i)->getVariable() == var) {
+                if (allAssignments.at(i)->getLValue() == lValue) {
                     return i;
                 }
             }

src/storm/storage/jani/OrderedAssignments.h

@@ -146,8 +146,8 @@ namespace storm {
             OrderedAssignments clone() const;
 
         private:
-            uint64_t isReadBeforeAssignment(Variable const& var, uint64_t assignmentNumber, uint64_t start = 0) const;
-            uint64_t isWrittenBeforeAssignment(Variable const& var, uint64_t assignmentNumber, uint64_t start = 0) const;
+            uint64_t isReadBeforeAssignment(LValue const& lValue, uint64_t assignmentNumber, uint64_t start = 0) const;
+            uint64_t isWrittenBeforeAssignment(LValue const& LValue, uint64_t assignmentNumber, uint64_t start = 0) const;
 
             /*!
              * Gets the number of  assignments number with an assignment not higher than index.

src/storm/storage/jani/TemplateEdge.cpp

@@ -1,6 +1,7 @@
 #include "storm/storage/jani/TemplateEdge.h"
 
 #include "storm/storage/jani/Model.h"
+#include "storm/storage/jani/LValue.h"
 
 #include "storm/storage/expressions/LinearityCheckVisitor.h"
 
@@ -27,8 +28,9 @@ namespace storm {
         void TemplateEdge::finalize(Model const& containingModel) {
             for (auto const& destination : getDestinations()) {
                 for (auto const& assignment : destination.getOrderedAssignments().getAllAssignments()) {
-                    if (containingModel.getGlobalVariables().hasVariable(assignment.getExpressionVariable())) {
-                        writtenGlobalVariables.insert(assignment.getExpressionVariable());
+                    Variable const& var = assignment.getLValue().isVariable() ? assignment.getLValue().getVariable() : assignment.getLValue().getArray();
+                    if (containingModel.getGlobalVariables().hasVariable(var.getExpressionVariable())) {
+                        writtenGlobalVariables.insert(var.getExpressionVariable());
                     }
                 }
             }

src/storm/storage/jani/VariableSet.cpp

@@ -44,6 +44,14 @@ namespace storm {
             return detail::ConstVariables<RealVariable>(realVariables.begin(), realVariables.end());
         }
         
+        detail::Variables<ArrayVariable> VariableSet::getArrayVariables() {
+            return detail::Variables<ArrayVariable>(arrayVariables.begin(), arrayVariables.end());
+        }
+        
+        detail::ConstVariables<ArrayVariable> VariableSet::getArrayVariables() const {
+            return detail::ConstVariables<ArrayVariable>(arrayVariables.begin(), arrayVariables.end());
+        }
+        
         Variable const& VariableSet::addVariable(Variable const& variable) {
             if (variable.isBooleanVariable()) {
                 return addVariable(variable.asBooleanVariable());
@@ -53,6 +61,8 @@ namespace storm {
                 return addVariable(variable.asUnboundedIntegerVariable());
             } else if (variable.isRealVariable()) {
                 return addVariable(variable.asRealVariable());
+            } else if (variable.isArrayVariable()) {
+                return addVariable(variable.asArrayVariable());
             }
             STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Cannot add variable of unknown type.");
         }
@@ -109,6 +119,19 @@ namespace storm {
             return *newVariable;
         }
         
+        ArrayVariable const& VariableSet::addVariable(ArrayVariable const& variable) {
+            STORM_LOG_THROW(!this->hasVariable(variable.getName()), storm::exceptions::WrongFormatException, "Cannot add variable with name '" << variable.getName() << "', because a variable with that name already exists.");
+            std::shared_ptr<ArrayVariable> newVariable = std::make_shared<ArrayVariable>(variable);
+            variables.push_back(newVariable);
+            arrayVariables.push_back(newVariable);
+            if (variable.isTransient()) {
+                transientVariables.push_back(newVariable);
+            }
+            nameToVariable.emplace(variable.getName(), variable.getExpressionVariable());
+            variableToVariable.emplace(variable.getExpressionVariable(), newVariable);
+            return *newVariable;
+        }
+        
         bool VariableSet::hasVariable(std::string const& name) const {
             return nameToVariable.find(name) != nameToVariable.end();
         }
@@ -174,6 +197,10 @@ namespace storm {
             return !realVariables.empty();
         }
         
+        bool VariableSet::containsArrayVariables() const {
+            return !arrayVariables.empty();
+        }
+        
         bool VariableSet::containsNonTransientRealVariables() const {
             for (auto const& variable : realVariables) {
                 if (!variable->isTransient()) {
@@ -193,7 +220,7 @@ namespace storm {
         }
         
         bool VariableSet::empty() const {
-            return !(containsBooleanVariable() || containsBoundedIntegerVariable() || containsUnboundedIntegerVariables());
+            return !(containsBooleanVariable() || containsBoundedIntegerVariable() || containsUnboundedIntegerVariables() || containsRealVariables() || containsArrayVariables());
         }
         
         uint_fast64_t VariableSet::getNumberOfTransientVariables() const {
@@ -251,6 +278,22 @@ namespace storm {
                     return true;
                 }
             }
+            for (auto const& arrayVariable : this->getArrayVariables()) {
+                if (arrayVariable.hasInitExpression()) {
+                    if (arrayVariable.getInitExpression().containsVariable(variables)) {
+                        return true;
+                    }
+                }
+                if (arrayVariable.hasElementTypeBounds()) {
+                    auto const& bounds = arrayVariable.getElementTypeBounds();
+                    if (bounds.first.containsVariable(variables)) {
+                        return true;
+                    }
+                    if (bounds.second.containsVariable(variables)) {
+                        return true;
+                    }
+                }
+            }
             return false;
         }
         

src/storm/storage/jani/VariableSet.h

@@ -9,6 +9,7 @@
 #include "storm/storage/jani/UnboundedIntegerVariable.h"
 #include "storm/storage/jani/BoundedIntegerVariable.h"
 #include "storm/storage/jani/RealVariable.h"
+#include "storm/storage/jani/ArrayVariable.h"
 
 namespace storm {
     namespace jani {
@@ -68,6 +69,16 @@ namespace storm {
              */
             detail::ConstVariables<RealVariable> getRealVariables() const;
             
+            /*!
+             * Retrieves the Array variables in this set.
+             */
+            detail::Variables<ArrayVariable> getArrayVariables();
+            
+            /*!
+             * Retrieves the Array variables in this set.
+             */
+            detail::ConstVariables<ArrayVariable> getArrayVariables() const;
+
             /*!
              * Adds the given variable to this set.
              */
@@ -93,6 +104,11 @@ namespace storm {
              */
             RealVariable const& addVariable(RealVariable const& variable);
 
+            /*!
+             * Adds the given real variable to this set.
+             */
+            ArrayVariable const& addVariable(ArrayVariable const& variable);
+
             /*!
              * Retrieves whether this variable set contains a variable with the given name.
              */
@@ -162,6 +178,11 @@ namespace storm {
              */
             bool containsRealVariables() const;
 
+            /*!
+             * Retrieves whether the set of variables contains a Array variable.
+             */
+            bool containsArrayVariables() const;
+
             /*!
              * Retrieves whether the set of variables contains a non-transient real variable.
              */
@@ -224,6 +245,9 @@ namespace storm {
             /// The real variables in this set.
             std::vector<std::shared_ptr<RealVariable>> realVariables;
             
+            /// The array variables in this set.
+            std::vector<std::shared_ptr<ArrayVariable>> arrayVariables;
+            
             /// The transient variables in this set.
             std::vector<std::shared_ptr<Variable>> transientVariables;
             

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

@@ -0,0 +1,100 @@
+#include "storm/storage/jani/traverser/ArrayEliminator.h"
+
+
+#include "storm/storage/expressions/ExpressionVisitor.h"
+#include "storm/storage/jani/expressions/JaniExpressionVisitor.h"
+
+namespace storm {
+    namespace jani {
+        namespace detail {
+/*
+        
+
+            class MaxArraySizeVisitor : public ExpressionVisitor, public JaniExpressionVisitor {
+                virtual MaxArraySizeVisitor() = default;
+                virtual ~MaxArraySizeVisitor() = default;
+    
+                std::size_t getMaxSize(Expression const& expression) {
+                    return boost::any_cast<std::size_t> expression.accept(*this);
+                }
+     
+                virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) override {
+                
+                }
+                
+                virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) override {
+                
+                }
+                
+                virtual boost::any visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) override {
+                
+                }
+                
+                virtual boost::any visit(BinaryRelationExpression const& expression, boost::any const& data) override {
+                
+                }
+                
+                virtual boost::any visit(VariableExpression const& expression, boost::any const& data) override {
+                
+                }
+                
+                virtual boost::any visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) override {
+                
+                }
+                
+                virtual boost::any visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) override {
+                
+                }
+                
+                virtual boost::any visit(BooleanLiteralExpression const& expression, boost::any const& data) override {
+                
+                }
+                
+                virtual boost::any visit(IntegerLiteralExpression const& expression, boost::any const& data) override {
+                
+                }
+                
+                virtual boost::any visit(RationalLiteralExpression const& expression, boost::any const& data) override {
+                
+                }
+                
+                
+                virtual boost::any visit(ValueArrayExpression const& expression, boost::any const& data) override {
+                
+                }
+                
+                virtual boost::any visit(ConstructorArrayExpression const& expression, boost::any const& data) override {
+                
+                }
+                
+                virtual boost::any visit(ArrayAccessExpression const& expression, boost::any const& data) override {
+                
+                }
+            };
+        
+            class ArrayVariableReplacer : public JaniTraverser {
+            public:
+
+                ArrayVariableReplacer() = default;
+                virtual ~ArrayVariableReplacer() = default;
+                std::unordered_map<storm::expressions::Variable, std::vector<reference_wrapper<storm::jani::Variable>> replace();
+
+                virtual void traverse(Assignment const& assignment, boost::any const& data) const override;
+                
+            private:
+                void std::unordered_map<storm::expressions::Variable, std::size_t>::getMaxSizes(Model& model);
+                
+            };
+            
+            class ArrayAccessLValueReplacer : public JaniTraverser {
+            }
+           */
+        }
+        
+        ArrayEliminator::eliminate(Model& model) {
+            //auto variableReplacements ArrayVariableReplacer().replace(model)
+        
+        }
+    }
+}
+

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

@@ -8,48 +8,14 @@
 namespace storm {
     namespace jani {
         class ArrayEliminator {
-/*
         public:
+            ArrayEliminator() = default;
+            
             void eliminate(Model& model);
 
         private:
         
-            class ArrayVariableReplacer : public JaniTraverser {
-            public:
-
-                ArrayVariableReplacer() = default;
-                virtual ~ArrayVariableReplacer() = default;
-                std::unordered_map<storm::expressions::Variable, std::vector<reference_wrapper<storm::jani::Variable>> replace();
-
-                virtual void traverse(Assignment const& assignment, boost::any const& data) const override;
-                
-            private:
-                void std::unordered_map<storm::expressions::Variable, std::size_t>::getMaxSizes(Model& model);
-                
-            };
-            
-            
-            
-        };
-        
-        : public JaniTraverser {
-        
-        public:
-            
-            struct ResultType {
-                bool hasLocationAssignment, hasEdgeAssignment, hasEdgeDestinationAssignment;
-            };
-            
-            AssignmentsFinder() = default;
-            
-            ResultType find(Model const& model, Variable const& variable);
-            
-            virtual ~AssignmentsFinder() = default;
         
-            virtual void traverse(Location const& location, boost::any const& data) const override;
-            virtual void traverse(TemplateEdge const& templateEdge, boost::any const& data) const override;
-            virtual void traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) const override;
-        */
         };
     }
 }