[NB] Check for compatible variability (#11047)

* [NB] Check for compatible variability

MLS section 3.8 forbids to solve an equation for a variable with
lower variability.

TODO
- alias removal doesn't check and removes eagerly.
- Types are not checked, so `/*Integer*/ n = 3.14` is not found.

Author: phannebohm

OMCompiler/Compiler/NBackEnd/Classes/NBVariable.mo

@@ -135,6 +135,7 @@ public
 
   function fromCref
     input ComponentRef cref;
+    input Attributes attr = NFAttributes.DEFAULT_ATTR;
     input Binding binding = NFBinding.EMPTY_BINDING;
     output Variable variable;
   protected
@@ -144,10 +145,10 @@ public
     SourceInfo info;
   algorithm
     node := ComponentRef.node(cref);
-    ty := ComponentRef.getSubscriptedType(cref, true);
-    vis := InstNode.visibility(node);
+    ty   := ComponentRef.getSubscriptedType(cref, true);
+    vis  := InstNode.visibility(node);
     info := InstNode.info(node);
-    variable := Variable.VARIABLE(cref, ty, binding, vis, NFAttributes.DEFAULT_ATTR, {}, {}, NONE(), info, NFBackendExtension.DUMMY_BACKEND_INFO);
+    variable := Variable.VARIABLE(cref, ty, binding, vis, attr, {}, {}, NONE(), info, NFBackendExtension.DUMMY_BACKEND_INFO);
   end fromCref;
 
   function makeVarPtrCyclic
@@ -533,7 +534,7 @@ public
           state := getVarPointer(cref);
           derNode := InstNode.VAR_NODE(DERIVATIVE_STR, dummy_ptr);
           der_cref := ComponentRef.append(cref, ComponentRef.fromNode(derNode, ComponentRef.scalarType(cref)));
-          var := fromCref(der_cref);
+          var := fromCref(der_cref, Variable.attributes(Pointer.access(state)));
           var.backendinfo := BackendExtension.BackendInfo.setVarKind(var.backendinfo, BackendExtension.STATE_DER(state, NONE()));
           (var_ptr, der_cref) := makeVarPtrCyclic(var, der_cref);
       then ();
@@ -740,7 +741,8 @@ public
   function makePreVar
     "Creates a previous variable pointer from the discrete variable cref.
     e.g. isOpen -> $PRE.isOpen"
-    input output ComponentRef cref    "old component reference to new component reference";
+    input ComponentRef cref           "old component reference";
+    output ComponentRef pre_cref      "new component reference";
     output Pointer<Variable> var_ptr  "pointer to new variable";
   algorithm
     () := match ComponentRef.node(cref)
@@ -752,10 +754,10 @@ public
         algorithm
           disc := BVariable.getVarPointer(cref);
           qual.name := PREVIOUS_STR;
-          cref := ComponentRef.append(cref, ComponentRef.fromNode(qual, ComponentRef.scalarType(cref)));
-          var := fromCref(cref);
+          pre_cref := ComponentRef.append(cref, ComponentRef.fromNode(qual, ComponentRef.scalarType(cref)));
+          var := fromCref(pre_cref, Variable.attributes(Pointer.access(disc)));
           var.backendinfo := BackendExtension.BackendInfo.setVarKind(var.backendinfo, BackendExtension.PREVIOUS(disc));
-          (var_ptr, cref) := makeVarPtrCyclic(var, cref);
+          (var_ptr, pre_cref) := makeVarPtrCyclic(var, pre_cref);
       then ();
 
       else algorithm
@@ -808,7 +810,7 @@ public
           // prepend the seed str and the matrix name and create the new cref
           qual.name := SEED_STR + "_" + name;
           cref := ComponentRef.append(cref, ComponentRef.fromNode(qual, ComponentRef.scalarType(cref)));
-          var := fromCref(cref);
+          var := fromCref(cref, NFAttributes.IMPL_DISCRETE_ATTR);
           // update the variable to be a seed and pass the pointer to the original variable
           var.backendinfo := BackendExtension.BackendInfo.setVarKind(var.backendinfo, BackendExtension.SEED_VAR(old_var_ptr));
           // create the new variable pointer and safe it to the component reference
@@ -825,9 +827,10 @@ public
     "Creates a partial derivative variable pointer from a cref. Used in NBJacobian and NBHessian
     to represent generic gradient equations.
     e.g: (speed, 'Jac') -> $pDer_Jac.speed"
-    input output ComponentRef cref    "old component reference to new component reference";
+    input ComponentRef cref           "old component reference";
     input String name                 "name of the matrix this partial derivative belongs to";
     input Boolean isTmp               "sets variable kind for tmpVar or resultVar accordingly";
+    output ComponentRef pder_cref     "new component reference";
     output Pointer<Variable> var_ptr  "pointer to new variable";
   protected
     VariableKind varKind = if isTmp then BackendExtension.JAC_TMP_VAR() else BackendExtension.JAC_VAR();
@@ -841,12 +844,12 @@ public
       case qual as InstNode.VAR_NODE() algorithm
         // prepend the seed str and the matrix name and create the new cref_DIFF_DIFF
         qual.name := PARTIAL_DERIVATIVE_STR + "_" + name;
-        cref := ComponentRef.append(cref, ComponentRef.fromNode(qual, ComponentRef.scalarType(cref)));
-        var := fromCref(cref);
+        pder_cref := ComponentRef.append(cref, ComponentRef.fromNode(qual, ComponentRef.scalarType(cref)));
+        var := fromCref(pder_cref, Variable.attributes(getVar(cref)));
         // update the variable kind and pass the pointer to the original variable
         var.backendinfo := BackendExtension.BackendInfo.setVarKind(var.backendinfo, varKind);
         // create the new variable pointer and safe it to the component reference
-        (var_ptr, cref) := makeVarPtrCyclic(var, cref);
+        (var_ptr, pder_cref) := makeVarPtrCyclic(var, pder_cref);
       then ();
 
       else algorithm
@@ -880,7 +883,8 @@ public
   function makeStartVar
     "Creates a start variable pointer from a cref. Used in NBInitialization.
     e.g: angle -> $START.angle"
-    input output ComponentRef cref    "old component reference to new component reference";
+    input ComponentRef cref           "old component reference";
+    output ComponentRef start_cref    "new component reference";
     output Pointer<Variable> var_ptr  "pointer to new variable";
   algorithm
     () := match ComponentRef.node(cref)
@@ -894,13 +898,13 @@ public
           old_var_ptr := BVariable.getVarPointer(cref);
           // prepend the seed str and the matrix name and create the new cref
           qual.name := START_STR;
-          cref := ComponentRef.append(cref, ComponentRef.fromNode(qual, ComponentRef.scalarType(cref)));
-          var := fromCref(cref);
+          start_cref := ComponentRef.append(cref, ComponentRef.fromNode(qual, ComponentRef.scalarType(cref)));
+          var := fromCref(start_cref, Variable.attributes(getVar(cref)));
           // update the variable to be a seed and pass the pointer to the original variable
           var.backendinfo := BackendExtension.BackendInfo.setVarKind(var.backendinfo, BackendExtension.START(old_var_ptr));
           // create the new variable pointer and safe it to the component reference
           var_ptr := Pointer.create(var);
-          cref := BackendDAE.lowerComponentReferenceInstNode(cref, var_ptr);
+          start_cref := BackendDAE.lowerComponentReferenceInstNode(start_cref, var_ptr);
       then ();
 
       else algorithm
@@ -966,16 +970,16 @@ public
     cref := ComponentRef.CREF(node, iter_subs, ty, NFComponentRef.Origin.CREF, ComponentRef.EMPTY());
     var_cref := ComponentRef.CREF(node, {}, ty, NFComponentRef.Origin.CREF, ComponentRef.EMPTY());
     // create variable
-    var := fromCref(var_cref);
+    var := fromCref(var_cref, NFAttributes.IMPL_DISCRETE_ATTR);
     // update the variable to be discrete and pass the pointer to the original variable
     var.backendinfo := BackendExtension.BackendInfo.setVarKind(var.backendinfo, BackendExtension.DISCRETE());
     // create the new variable pointer and safe it to the component reference
     (var_ptr, cref) := makeVarPtrCyclic(var, cref);
   end makeEventVar;
 
   function makeAuxStateVar
-    "Creates a generic boolean variable pointer from a unique index and context name.
-    e.g. (\"$WHEN\", 4) --> $WHEN_4"
+    "Creates a auxiliary state variable from an expression.
+    e.g. der(x^2 + y) --> der(aux)"
     input Integer uniqueIndex         "unique identifier index";
     input Option<Expression> binding  "optional binding expression";
     output Pointer<Variable> var_ptr  "pointer to new variable";
@@ -993,7 +997,7 @@ public
     // create variable and add optional binding
     if isSome(binding) then
       bnd := Util.getOption(binding);
-      var := fromCref(cref, Binding.FLAT_BINDING(bnd, Expression.variability(bnd), NFBinding.Source.BINDING));
+      var := fromCref(cref, NFAttributes.DEFAULT_ATTR, Binding.FLAT_BINDING(bnd, Expression.variability(bnd), NFBinding.Source.BINDING));
     else
       var := fromCref(cref);
     end if;

OMCompiler/Compiler/NBackEnd/Modules/1_Main/NBCausalize.mo

@@ -44,6 +44,7 @@ protected
   import Expression = NFExpression;
   import NFFlatten.{FunctionTree, FunctionTreeImpl};
   import InstNode = NFInstNode.InstNode;
+  import Prefixes = NFPrefixes;
   import SBGraphUtil = NFSBGraphUtil;
   import Subscript = NFSubscript;
   import Type = NFType;
@@ -100,7 +101,7 @@ public
 
       case (System.SystemType.ODE, BackendDAE.MAIN(ode = systems, varData = varData, eqData = eqData, funcTree = funcTree))
         algorithm
-          (systems, varData, eqData, funcTree) := applyModule(systems, varData, eqData, funcTree, func);
+          (systems, varData, eqData, funcTree) := applyModule(systems, systemType, varData, eqData, funcTree, func);
           bdae.ode := systems;
           bdae.varData := varData;
           bdae.eqData := eqData;
@@ -112,10 +113,10 @@ public
           if Flags.isSet(Flags.INITIALIZATION) then
             print(StringUtil.headline_1("Balance Initialization") + "\n");
           end if;
-          (systems, varData, eqData, funcTree) := applyModule(systems, varData, eqData, funcTree, func);
+          (systems, varData, eqData, funcTree) := applyModule(systems, systemType, varData, eqData, funcTree, func);
           bdae.init := systems;
           if Util.isSome(bdae.init_0) then
-            (systems, varData, eqData, funcTree) := applyModule(Util.getOption(bdae.init_0), varData, eqData, funcTree, func);
+            (systems, varData, eqData, funcTree) := applyModule(Util.getOption(bdae.init_0), systemType, varData, eqData, funcTree, func);
             bdae.init_0 := SOME(systems);
           end if;
           bdae.varData := varData;
@@ -125,7 +126,7 @@ public
 
       case (System.SystemType.DAE, BackendDAE.MAIN(dae = SOME(systems), varData = varData, eqData = eqData, funcTree = funcTree))
         algorithm
-          (systems, varData, eqData, funcTree) := applyModule(systems, varData, eqData, funcTree, causalizeDAEMode);
+          (systems, varData, eqData, funcTree) := applyModule(systems, systemType, varData, eqData, funcTree, causalizeDAEMode);
           bdae.dae := SOME(systems);
           bdae.varData := varData;
           bdae.eqData := eqData;
@@ -140,21 +141,64 @@ public
 
   function applyModule
     input list<System.System> systems;
+    input System.SystemType systemType;
     output list<System.System> new_systems = {};
     input output VarData varData;
     input output EqData eqData;
     input output FunctionTree funcTree;
     input Module.causalizeInterface func;
   protected
     System.System new_system;
+    Boolean violated = false "true if any system violated variability consistency";
   algorithm
     for system in systems loop
       (new_system, varData, eqData, funcTree) := func(system, varData, eqData, funcTree);
       new_systems := new_system :: new_systems;
     end for;
     new_systems := listReverse(new_systems);
+
+    if systemType <> System.SystemType.INI then
+      for system in new_systems loop
+        violated := checkSystemVariabilities(system) or violated;
+      end for;
+      if violated then fail(); end if;
+    end if;
   end applyModule;
 
+  function checkSystemVariabilities
+    "checks whether variability is valid. Prevents things like `Integer i = time;`"
+    input System.System system;
+    output Boolean violated = false;
+  algorithm
+    if isSome(system.strongComponents) then
+      for scc in Util.getOption(system.strongComponents) loop
+        () := match scc
+          case StrongComponent.SINGLE_COMPONENT() algorithm
+            if Variable.variability(Pointer.access(scc.var)) <
+              Prefixes.variabilityMax(
+                Expression.variability(Equation.getLHS(Pointer.access(scc.eqn))),
+                Expression.variability(Equation.getRHS(Pointer.access(scc.eqn)))
+              )
+            then
+              // The variability of the equation must be greater or equal to that of the variable it solves.
+              // See MLS section 3.8 Variability of Expressions
+              Error.addMessage(Error.COMPILER_ERROR, {"The following strong component has conflicting variabilities: "
+                + Prefixes.variabilityString(Variable.variability(Pointer.access(scc.var))) + " != "
+                + Prefixes.variabilityString(Prefixes.variabilityMax(
+                    Expression.variability(Equation.getLHS(Pointer.access(scc.eqn))),
+                    Expression.variability(Equation.getRHS(Pointer.access(scc.eqn)))
+                  ))
+                + "\n" + StrongComponent.toString(scc)});
+              violated := true;
+            end if;
+          then ();
+          /* TODO case StrongComponent.MULTI_COMPONENT() */
+          else ();
+        end match;
+      end for;
+    end if;
+  end checkSystemVariabilities;
+
   function simple
     input VariablePointers vars;
     input EquationPointers eqs;

OMCompiler/Compiler/NBackEnd/Modules/1_Main/NBPartitioning.mo

@@ -362,7 +362,7 @@ protected
     single_vars := VariablePointers.getMarkedVars(variables, marked_vars);
 
     if not listEmpty(single_vars) then
-      Error.addMessage(Error.INTERNAL_ERROR,{getInstanceName() + " (" + System.System.systemTypeString(systemType)
+      Error.addMessage(Error.INTERNAL_ERROR, {getInstanceName() + " (" + System.System.systemTypeString(systemType)
         + ") failed because the following variables could not be assigned to a partition:\n  {"
         + stringDelimitList(list(BVariable.toString(Pointer.access(var)) for var in single_vars), "\n") + "}"});
       fail();

OMCompiler/Compiler/NFFrontEnd/NFAttributes.mo

@@ -141,7 +141,7 @@ public
               finalPrefix = SCode.Final.NOT_FINAL(),
               innerOuter = Absyn.InnerOuter.NOT_INNER_OUTER(),
               replaceablePrefix = SCode.Replaceable.NOT_REPLACEABLE()))
-        then NFAttributes.DEFAULT_ATTR;
+        then DEFAULT_ATTR;
 
       else
         algorithm
@@ -199,9 +199,9 @@ public
     Boolean fin, redecl;
     Replaceable repl;
   algorithm
-    if referenceEq(outerAttr, NFAttributes.DEFAULT_ATTR) and innerAttr.connectorType == 0 then
+    if referenceEq(outerAttr, DEFAULT_ATTR) and innerAttr.connectorType == 0 then
       attr := innerAttr;
-    elseif referenceEq(innerAttr, NFAttributes.DEFAULT_ATTR) then
+    elseif referenceEq(innerAttr, DEFAULT_ATTR) then
       cty := ConnectorType.merge(outerAttr.connectorType, innerAttr.connectorType, node);
       attr := Attributes.ATTRIBUTES(cty, outerAttr.parallelism,
         outerAttr.variability, outerAttr.direction, innerAttr.innerOuter, outerAttr.isFinal,
@@ -238,9 +238,9 @@ public
     Boolean fin, redecl;
     Replaceable repl;
   algorithm
-    if referenceEq(innerAttr, NFAttributes.DEFAULT_ATTR) and outerAttr.connectorType == 0 then
+    if referenceEq(innerAttr, DEFAULT_ATTR) and outerAttr.connectorType == 0 then
       attr := outerAttr;
-    elseif referenceEq(outerAttr, NFAttributes.DEFAULT_ATTR) and innerAttr.connectorType == 0 then
+    elseif referenceEq(outerAttr, DEFAULT_ATTR) and innerAttr.connectorType == 0 then
       attr := innerAttr;
     else
       Attributes.ATTRIBUTES(cty, par, var, dir, io, fin, redecl, repl) := outerAttr;
@@ -266,9 +266,9 @@ public
     Boolean redecl;
     Replaceable repl;
   algorithm
-    if referenceEq(origAttr, NFAttributes.DEFAULT_ATTR) then
+    if referenceEq(origAttr, DEFAULT_ATTR) then
       attr := redeclAttr;
-    elseif referenceEq(redeclAttr, NFAttributes.DEFAULT_ATTR) then
+    elseif referenceEq(redeclAttr, DEFAULT_ATTR) then
       attr := origAttr;
     else
       Attributes.ATTRIBUTES(cty, par, var, dir, io, _, _, _) := origAttr;
@@ -514,7 +514,7 @@ public
   protected
     Variability var = attr.variability;
   algorithm
-    if referenceEq(attr, NFAttributes.DEFAULT_ATTR) and InstNode.isDiscreteClass(clsNode) then
+    if referenceEq(attr, DEFAULT_ATTR) and InstNode.isDiscreteClass(clsNode) then
       attr := NFAttributes.IMPL_DISCRETE_ATTR;
     elseif var == Variability.CONTINUOUS and InstNode.isDiscreteClass(clsNode) then
       attr.variability := Variability.IMPLICITLY_DISCRETE;

OMCompiler/Compiler/NFFrontEnd/NFComponentRef.mo

@@ -47,6 +47,7 @@ protected
   import Prefixes = NFPrefixes;
   import MetaModelica.Dangerous.*;
   import JSON;
+  import Variable = NFVariable;
 
   import ComponentRef = NFComponentRef;
 
@@ -453,9 +454,12 @@ public
     output Variability var;
   algorithm
     var := match cref
+      local
+        Pointer<Variable> v;
       case CREF(node = InstNode.COMPONENT_NODE())
         then Component.variability(InstNode.component(cref.node));
       case CREF(node = InstNode.CLASS_NODE()) then Variability.CONSTANT;
+      case CREF(node = InstNode.VAR_NODE(varPointer = v)) then Variable.variability(Pointer.access(v));
       else Variability.CONTINUOUS;
     end match;
   end nodeVariability;

OMCompiler/Compiler/NFFrontEnd/NFVariable.mo

@@ -191,6 +191,26 @@ public
       else {var};
   end expandChildren;
 
+  function typeOf
+    input Variable var;
+    output Type ty = var.ty;
+  end typeOf;
+
+  function attributes
+    input Variable variable;
+    output Attributes attributes = variable.attributes;
+  end attributes;
+
+  function variability
+    input Variable variable;
+    output Variability variability = variable.attributes.variability;
+  end variability;
+
+  function visibility
+    input Variable variable;
+    output Visibility visibility = variable.visibility;
+  end visibility;
+
   function isComplex
     input Variable var;
     output Boolean b = Type.isComplex(var.ty);
@@ -207,16 +227,6 @@ public
       variable.attributes.variability <= Variability.STRUCTURAL_PARAMETER;
   end isStructural;
 
-  function variability
-    input Variable variable;
-    output Variability variability = variable.attributes.variability;
-  end variability;
-
-  function visibility
-    input Variable variable;
-    output Visibility visibility = variable.visibility;
-  end visibility;
-
   function isEmptyArray
     input Variable variable;
     output Boolean isEmpty = Type.isEmptyArray(variable.ty);

testsuite/simulation/modelica/NBackend/basics/Makefile

@@ -11,6 +11,7 @@ simpleNonlinearLoop.mos \
 implicitEquation.mos \
 underdetermined_init.mos \
 partitioning.mos \
+variability.mos \
 
 # test that currently fail. Move up when fixed.
 # Run make failingtest