modelica / ModelicaSpecification

Specification of the Modelica Language
https://specification.modelica.org
Creative Commons Attribution Share Alike 4.0 International
102 stars 41 forks source link

8.4 Synchronous Data-flow Principle and Single Assignment Rule #2348

Closed HansOlsson closed 5 years ago

HansOlsson commented 5 years ago

Based on https://github.com/modelica/ModelicaStandardLibrary/issues/2862#issuecomment-486751526 - I believe it is always good to revisit old assumptions.

Looking at https://specification.modelica.org/master/Ch8.html#synchronous-data-flow-principle-and-single-assignment-rule a number of these statements are not that helpful:

  1. " All variables keep their actual values until these values are explicitly changed."

The word "explicit" does not have the usual meaning, as states are integrated (and thus change) and other variables are determined implicitly by solving systems of equations. An important consideration is that since variables are solved numerically they can also vary slightly for no reason at all.

We could make it correct by stating: "Discrete variables keep their actual values until these variables are explicitly changed." and "Differentiated variables have der(x) corresponding to the time-derivative of x, and x is continuous, except when reinit is triggered - see section ....." Note: This is not restricted to states - it should be valid for any differentiated variable. That's also why it doesn't say reinit(x, ...).

  1. "At every time instant, during continuous integration and at event instants, the active equations express relations between variables which have to be fulfilled concurrently (equations are not active if the corresponding if-branch, when-clause or block in which the equation is present is not active)."

That would a complicated definition as the "active equations" would depend on values of variables. The issue is that this requires that we can split satisfying equations in two parts - first finding "active equations" and then satisfying them, but this is not always possible.

It also seems to imply some old definition of when-clauses. Currently this is clearer by mapping when-clauses to if-then-else equations and forbidding if-clauses with different number of equations during simulations.

Thus it could be formulated as: "At every time instant, during continuous integration and at event instants, the equations express relations between variables which have to be fulfilled concurrently. For an if-clause the condition selects the active branch, and the different possible branches must have the same number of equations; see ..."

  1. "The total number of equations is identical to the total “number of unknown variables” (= single assignment rule). "

We have now introduced the concept of "balanced models" (section 4.7) which is basically the same as this "single assignment rule", but the current formulation misses the more important part that could be stated as:

"It must be possible to determine the variables from the equations (with a unique solution close to the trajectory). A necessary requirement is that the model is globally balanced - i.e. that the total number of equations is identical to the total number of unknown variables."

This formulation implies that the equations must be non-singular=>structurally non-singular=>balanced.

The "single assignment rule" is reminiscent of "single definition rule" in C/C++ - but beyond the name I don't see any connection, and "assignment" is also the procedure of matching variables to equations - which requires that the problem is structurally non-singular.

I thus believe that part of "single assignment rule" was to invoke the concept of "structurally non-singular" without stating it. I prefer to explicitly state that it has solution implying "non-singular" instead of introducing "assignment". The reasons are that the assignment-solution is not unique and when you have matrix variables and equations it requires more care in formulating - and assignment is still just an implementation issue.

(Note that previously the solution of the assignment-problem mattered as it would assign a variable to a when-clause causing that variable to keep its value between events; and different assignments would lead to different results.)

(Note that "structurally non-singular" on a component-level is a different topic.)

HansOlsson commented 5 years ago

Language group:

"At every time instant, during continuous integration and at event instants, the equations express relations between variables which have to be fulfilled concurrently. For an if-clause the condition selects the active branch, and the different possible branches must have the same number of equations; see ..."

->

"At every time instant, during continuous integration and at event instants, the equations express relations between variables which have to be fulfilled concurrently. "

"The total number of equations is identical to the total “number of unknown variables” (= single assignment rule). " "It must be possible to determine the variables from the equations (with a unique solution close to the trajectory). A necessary requirement is that the model is globally balanced - i.e. that the total number of equations is identical to the total number of unknown variables."

-> "There must exist a perfect matching of variables to equations after flattening (perfect matching rule - previously called single assignment rule); see also globally balanced ...

Agreement by acclamation. Discussion about the discrete-matching proposed by Henrik.