support for transient assignments in locations, changed assignment to jani::variable, notice that (already broken) prism-to-jani is disabled as long as we reshape jani code

Former-commit-id: 9bf2f68c7c [formerly 2a1181a603]
Former-commit-id: d487b0fc74

src/parser/JaniParser.cpp

@@ -321,6 +321,15 @@ namespace storm {
             STORM_LOG_THROW(expr.hasNumericalType(), storm::exceptions::InvalidJaniException, "Operator " << opstring << " expects argument " + std::to_string(argNr) + " to be numerical in " << errorInfo << ".");
         }
 
+        storm::jani::Variable getLValue(std::string const& ident, storm::jani::VariableSet const& globalVars, storm::jani::VariableSet const& localVars, std::string const& scopeDescription) {
+            if(localVars.hasVariable(ident)) {
+                return globalVars.getVariable(ident);
+            } else if(globalVars.hasVariable(ident)) {
+                return globalVars.getVariable(ident);
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown identifier '" << ident << "' occurs in  " << scopeDescription);
+            }
+        }
 
         storm::expressions::Variable JaniParser::getVariableOrConstantExpression(std::string const &ident,std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars) {
             if(localVars.count(ident) == 1) {
@@ -552,10 +561,21 @@ namespace storm {
             STORM_LOG_THROW(automatonStructure.count("locations") > 0, storm::exceptions::InvalidJaniException, "Automaton '" << name << "' does not have locations.");
             std::unordered_map<std::string, uint64_t> locIds;
             for(auto const& locEntry : automatonStructure.at("locations")) {
-                STORM_LOG_THROW(locEntry.count("name"), storm::exceptions::InvalidJaniException, "Locations for automaton '" << name << "' must have exactly one name");
+                STORM_LOG_THROW(locEntry.count("name") == 1, storm::exceptions::InvalidJaniException, "Locations for automaton '" << name << "' must have exactly one name");
                 std::string locName = getString(locEntry.at("name"), "location of automaton " + name);
                 STORM_LOG_THROW(locIds.count(locName) == 0, storm::exceptions::InvalidJaniException, "Location with name '" + locName + "' already exists in automaton '" + name + "'");
-                uint64_t id = automaton.addLocation(storm::jani::Location(locName));
+                
+                //STORM_LOG_THROW(locEntry.count("invariant") > 0 && !supportsInvariants(parentModel.getModelType()), storm::exceptions::InvalidJaniException, "Invariants are not supported in the model type " + to_string(parentModel.getModelType()));
+                std::vector<storm::jani::Assignment> transientAssignments;
+                for(auto const& transientValueEntry : locEntry.at("transient-values")) {
+                    STORM_LOG_THROW(transientValueEntry.count("ref") == 1, storm::exceptions::InvalidJaniException, "Transient values in location " << locName << " need exactly one ref that is assigned to");
+                    STORM_LOG_THROW(transientValueEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Transient values in location " << locName << " need exactly one assigned value");
+                    storm::jani::Variable lhs = getLValue(transientValueEntry.at("ref"), parentModel.getGlobalVariables(), automaton.getVariables(), "LHS of assignment in location " + locName + " (automaton '" + name + "')");
+                    STORM_LOG_THROW(lhs.isTransientVariable(), storm::exceptions::InvalidJaniException, "Assigned non-transient variable " + lhs.getName() + " in location " + locName + " (automaton: '" + name + "')");
+                    storm::expressions::Expression rhs = parseExpression(transientValueEntry.at("value"), "Assignment of variable " + lhs.getName() + " in location " + locName + " (automaton: '" + name + "')");
+                    transientAssignments.emplace_back(lhs, rhs);
+                }
+                uint64_t id = automaton.addLocation(storm::jani::Location(locName, transientAssignments));
                 locIds.emplace(locName, id);
             }
             STORM_LOG_THROW(automatonStructure.count("initial-locations") == 1, storm::exceptions::InvalidJaniException, "Automaton '" << name << "' does not have initial locations.");
@@ -639,7 +659,7 @@ namespace storm {
                         // 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 + "'");
-                        assignments.emplace_back(getVariableOrConstantExpression(refstring, "Assignment variable in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'", localVars), assignmentExpr);
+                        assignments.emplace_back(getLValue(refstring, parentModel.getGlobalVariables(), automaton.getVariables(), "Assignment variable in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'"), assignmentExpr);
                     }
                     edgeDestinations.emplace_back(locIds.at(targetLoc), probExpr, assignments);
                 }

src/storage/jani/Assignment.cpp

@@ -3,12 +3,16 @@
 namespace storm  {
     namespace jani {
         
-        Assignment::Assignment(storm::expressions::Variable const& variable, storm::expressions::Expression const& expression) : variable(variable), expression(expression) {
+        Assignment::Assignment(storm::jani::Variable const& variable, storm::expressions::Expression const& expression) : variable(variable), expression(expression) {
             // Intentionally left empty.
         }
         
+        storm::jani::Variable const& Assignment::getVariable() const {
+            return variable.get();
+        }
+        
         storm::expressions::Variable const& Assignment::getExpressionVariable() const {
-            return variable;
+            return variable.get().getExpressionVariable();
         }
         
         storm::expressions::Expression const& Assignment::getAssignedExpression() const {
@@ -19,8 +23,12 @@ namespace storm  {
             this->expression = expression;
         }
         
+        bool Assignment::isTransientAssignment() const {
+            return this->variable.get().isTransientVariable();
+        }
+        
         std::ostream& operator<<(std::ostream& stream, Assignment const& assignment) {
-            stream << assignment.getExpressionVariable().getName() << " := " << assignment.getAssignedExpression();
+            stream << assignment.getVariable().getName() << " := " << assignment.getAssignedExpression();
             return stream;
         }
         

src/storage/jani/Assignment.h

@@ -1,6 +1,8 @@
 #pragma once
 
-#include "src/storage/expressions/Variable.h"
+#include <functional>
+
+#include "src/storage/jani/Variable.h"
 #include "src/storage/expressions/Expression.h"
 
 namespace storm {
@@ -11,8 +13,13 @@ namespace storm {
             /*!
              * Creates an assignment of the given expression to the given variable.
              */
-            Assignment(storm::expressions::Variable const& variable, storm::expressions::Expression const& expression);
+            Assignment(storm::jani::Variable const& variable, storm::expressions::Expression const& expression);
             
+            /*!
+             * Retrieves the expression variable that is written in this assignment.
+             */
+            storm::jani::Variable const& getVariable() const;
+                
             /*!
              * Retrieves the expression variable that is written in this assignment.
              */
@@ -28,11 +35,16 @@ namespace storm {
              */
             void setAssignedExpression(storm::expressions::Expression const& expression);
 
+            /**
+             * Retrieves whether the assignment assigns to a transient variable.
+             */
+            bool isTransientAssignment() const;
+            
             friend std::ostream& operator<<(std::ostream& stream, Assignment const& assignment);
             
         private:
             // The variable being assigned.
-            storm::expressions::Variable variable;
+            std::reference_wrapper<storm::jani::Variable const> variable;
             
             // The expression that is being assigned to the variable.
             storm::expressions::Expression expression;

src/storage/jani/Location.cpp

@@ -1,9 +1,12 @@
 #include "src/storage/jani/Location.h"
+#include "src/storage/jani/Assignment.h"
+#include "src/exceptions/InvalidJaniException.h"
+#include "src/utility/macros.h"
 
 namespace storm {
     namespace jani {
         
-        Location::Location(std::string const& name) : name(name) {
+        Location::Location(std::string const& name, std::vector<Assignment> const& transientAssignments) : name(name), transientAssignments(transientAssignments) {
             // Intentionally left empty.
         }
         
@@ -11,5 +14,15 @@ namespace storm {
             return name;
         }
         
+        std::vector<Assignment> const& Location::getTransientAssignments() const {
+            return transientAssignments;
+        }
+        
+        void Location::checkValid() const {
+            for(auto const& assignment : transientAssignments) {
+                STORM_LOG_THROW(assignment.isTransientAssignment(), storm::exceptions::InvalidJaniException, "Only transient assignments are allowed in locations.");
+            }
+        }
+        
     }
 }

src/storage/jani/Location.h

@@ -1,25 +1,42 @@
 #pragma once
 
 #include <string>
+#include <vector>
+#include "src/storage/jani/Assignment.h"
 
 namespace storm {
     namespace jani {
         
+        /**
+         * Jani Location:
+         * 
+         * Whereas Jani Locations also support invariants, we do not have support for them (as we do not support any of the allowed model types)
+         */
         class Location {
         public:
             /*!
              * Creates a new location.
              */
-            Location(std::string const& name);
+            Location(std::string const& name, std::vector<Assignment> const& transientAssignments = {});
             
             /*!
              * Retrieves the name of the location.
              */
             std::string const& getName() const;
             
+            /*!
+             *
+             */
+            std::vector<Assignment> const& getTransientAssignments() const;
+            
+            /*!
+             * Checks whether the location is valid, that is, whether the assignments are indeed all transient assignments.
+             */
+            void checkValid() const;
         private:
             // The name of the location.
             std::string name;
+            std::vector<Assignment> transientAssignments;
         };
         
     }

src/storage/prism/Program.cpp

@@ -1511,6 +1511,7 @@ namespace storm {
         }
         
         storm::jani::Model Program::toJani(bool allVariablesGlobal) const {
+#if 0
             // Start by creating an empty JANI model.
             storm::jani::ModelType modelType;
             switch (this->getModelType()) {
@@ -1639,7 +1640,7 @@ namespace storm {
                     for (auto const& update : command.getUpdates()) {
                         std::vector<storm::jani::Assignment> assignments;
                         for (auto const& assignment : update.getAssignments()) {
-                            assignments.push_back(storm::jani::Assignment(assignment.getVariable(), assignment.getExpression()));
+                            assignments.push_back(storm::jani::Assignment(assignment.getVariable().getName(), assignment.getExpression()));
                         }
                         
                         if (rateExpression) {
@@ -1668,6 +1669,7 @@ namespace storm {
             janiModel.finalize();
             
             return janiModel;
+#endif
         }
         
         std::ostream& operator<<(std::ostream& out, Program::ModelType const& type) {