Local balance does not consider type

[henrikt-ma]

This model is currently considered completely locally balanced:

model LocalImbalanceByType

  model A "Currently locally balanced model"
    Real x;
    Boolean b;
    Boolean c;
  equation
    b = c; // Boolean equation
    x + (if b then 1.0 else 2.0) = 0; // Real equation
    x + (if c then 1.0 else 2.0) = 0; // Real equation
  end A;

  A a;

end LocalImbalanceByType;

However, I would like to be able to reject this with support in the specification to say that it is locally imbalanced for both Boolean and Real types in the component a.

Am I missing something when I think it should be possible to do separate counting for Real and Integer?

[HansOlsson]

No, you are not missing anything.
It's just that specifying the type of an equation is not entirely trivial.

[henrikt-ma]

I thought the most difficult equation would be a record equation, but isn't it enough for the specification to explain that a record equation should be counted (recursively) member by member? Are there other non-trivial equations to associate with a type?

Note that we don't have to formally introduce the concept of the type of an equation, but that it will be sufficient to explain how an equation contributes with local equation count for each of the built-in scalar types.

[HansOlsson]

I thought the most difficult equation would be a record equation, but isn't it enough for the specification to explain that a record equation should be counted (recursively) member by member? Are there other non-trivial equations to associate with a type?

No major issue, but some minor work to get it right (including over-determined connectors with non-Reals).
The important part is that the restrictions for solving Integer/Boolean/String equations eliminates the worst issues.

Note that we don't have to formally introduce the concept of the type of an equation, but that it will be sufficient to explain how an equation contributes with local equation count for each of the built-in scalar types.

[henrikt-ma]

No major issue, but some minor work to get it right (including over-determined connectors with non-Reals).

Oh, is this possible?! Can you given an example?

The important part is that the restrictions for solving Integer/Boolean/String equations eliminates the worst issues.

Right.

[henrikt-ma]

No major issue, but some minor work to get it right (including over-determined connectors with non-Reals).

I am still interested in examples of this, but after letting it sink in, I would expect the counting to be very straightforward, at least with the way we do the counting in System Modeler. The rank of equalityConstraint simply belongs to the balance of Real, both for variables and equations.

In terms of equation solving, this corresponds to the observation that all non-Real members will be determined at the roots, with values that are equivalent across all roots, so that the connections only serve to propagate these values from the roots to all the non-roots.

[henrikt-ma]

I wonder we have sufficient restrictions to allow the equation count for an if-equation to be split by type?

If we can count the non-Real parts, the Real parts of the branches will need to be balanced as a consequence of the total balance of the branches.

Take Boolean for instance. Boolean variables can only be solved from Boolean equations, and Boolean equations can only be solved for Boolean variables. That a Boolean variable shall essentially be solvable from an equation in solved form means that if a Boolean variable is solved from a Boolean equation in of of the if-equation branches, the same variable must also be matched with a Boolean equation in each of the other if-equation branches. It follows that the Boolean equation count must be balanced across the if-equation branches, which then becomes the Boolean equation count for the entire if-equation.

Fortunately, the counting needed for local balance does not require figuring out which set of Boolean variables to match to the if-equation, so I believe we actually already have what is needed to do the local equation count for an if-equation.

For example, the following if-equations which would be a mess to count, could be rejected on the basis of not fulfilling the rule that Integer equations must essentially be in solved form:

model IfMess
  parameter b = false;
  Real x;
  Real y;
  Integer m;
  Integer n;
equation
  if b then
    m + n = 0;
    x = 0.5;
    y = 0.6;
  else
    n = 5;
    m = 6;
    x + y = 0;
  end if;
  if b then
    m = if x < 1 then 0 else 3;
  else
    x = 0.5 * m;
  end if;
end IfMess;

However, the model above raises the question whether the evaluability requirement for an if-equation condition should be strengthened, so that the model above can be accepted (and locally counted) instead of being rejected?

[HansOlsson]

I wonder we have sufficient restrictions to allow the equation count for an if-equation to be split by type?

If we can count equations for local balancing that should work as well.
It may be that we can just add that equation and variable counting can be split according to the different types; and should match for each type (both for local balance and for if-equations); and that we don't have to specify it in detail.

However, before we get too far: it's important to consider that the local balance is quite different from perfect matching.
We could non-normatively add:

Related to globally balanced there is the stronger requirement of perfect matching.
One can consider a similar definition for local perfect matching.
But it requires additions to handle some cases like flow-sources like electrical ideal current sources.
Specifically, it requires considering both flow and non-flow variables in each connector and to balance the new unknowns add a corresponding number of equations relating them.
However, for the same reason a local perfect matching does not imply a global perfect matching.

Or it might be best to not add it.

If we can count the non-Real parts, the Real parts of the branches will need to be balanced as a consequence of the total balance of the branches.

Take Boolean for instance. Boolean variables can only be solved from Boolean equations, and Boolean equations can only be solved for Boolean variables. That a Boolean variable shall essentially be solvable from an equation in solved form means that if a Boolean variable is solved from a Boolean equation in of of the if-equation branches, the same variable must also be matched with a Boolean equation in each of the other if-equation branches. It follows that the Boolean equation count must be balanced across the if-equation branches, which then becomes the Boolean equation count for the entire if-equation.

Fortunately, the counting needed for local balance does not require figuring out which set of Boolean variables to match to the if-equation, so I believe we actually already have what is needed to do the local equation count for an if-equation.

For example, the following if-equations which would be a mess to count, could be rejected on the basis of not fulfilling the rule that Integer equations must essentially be in solved form:

model IfMess
  parameter Boolean b = false;
  Real x;
  Real y;
  Integer m;
  Integer n;
equation
  if b then
    m + n = 0;
    x = 0.5;
    y = 0.6;
  else
    n = 5;
    m = 6;
    x + y = 0;
  end if;
  if b then
    m = if x < 1 then 0 else 3;
  else
    x = 0.5 * m;
  end if;
end IfMess;

However, the model above raises the question whether the evaluability requirement for an if-equation condition should be strengthened, so that the model above can be accepted (and locally counted) instead of being rejected?

(I corrected a minor issue in the example above.)
As I understand it the intent is to state that https://specification.modelica.org/master/equations.html#if-equations should apply for each type, forcing b to be evaluable. That should work and would give that model is locally balanced for each type (for both values of b).

Trying to strengthen the type-requirement for locally balanced without the corresponding change for if-equations would just be a mess (how would we even count integer equations above?)

[henrikt-ma]

Or it might be best to not add it.

To begin with, I think it sounds like a good idea to not start talking about "local perfect matching". We can always revisit this idea of non-normatively explaining why there is no "local perfect matching rule" later.

As I understand it the intent is to state that https://specification.modelica.org/master/equations.html#if-equations should apply for each type, forcing b to be evaluable. That should work and would give that model is locally balanced for each type (for both values of b).

Yes, and if b wouldn't have been evaluable, the if-equation would have an error with clear support in the specification. (I would have expected the error message to mention all types which are not balanced across the if-equation branches in the motivation for why the condition needs to be evaluable.)

Trying to strengthen the type-requirement for locally balanced without the corresponding change for if-equations would just be a mess (how would we even count integer equations above?)

What I was trying to show with the example is that we might have been able to reject the model on different basis than local imbalance, and that we might have been able to get away with only defining local equation counting for models free of other errors than a potential local imbalance.

If we only add a rule about per-type balance of if-equation branches, it doesn't give us a clear way to deal with this:

  parameter Boolean b = false;
equation
  if b then
    n = 1;
  else
    m = 1;
  end if;

On the other hand, if we add a rule saying that:

• An if-equation with non-evaluable condition must for each discrete-valued type have a unique set of variables solvable in all branches. (A generalization/clarification of the almost solved form mentioned in https://specification.modelica.org/master/modelica-dae-representation.html.)

… then it follows that:

• The equation count for each discrete-valued type must be equal across all branches (equal to the size of the solvable set of variables).
• The equation count for Real must be equal across all branches (since it is what remains after removing all the discrete-type counts from the total branch counts which are already required to be balanced).

So, we could have one rule which adds additional value beside local equation counting, and then describe the two consequences and how they enable defining the per-type local equation count for an if-equation.

[HansOlsson]

I believe that it suffices to just state that the balancing requirement should hold for each primitive type.

The problem with "almost solved form" is that the current one (especially for integers) is a bit of a mix of local (must be possible to solve for the variable) and global requirement (from the given equation based on global sorting) which can create a more complicated situation.

Consider:

model P
  parameter Boolean b=true;
  Integer m,n;
equation 
    if b then
     m+n*2=0;
  else
    n+m*2=0;
  end if;
  m=integer(time);
end P;

Here the if-statement is kind of in "almost solved form", but one branch doesn't work together with the other equation for m; so it isn't in "almost solved form" for the global analysis.

[HansOlsson]

Language group (yesterday): Add this simple type-balancing and then open an issue regarding "almost solved form" for non-Real equations in if-equations, #3779