Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Well-formed or illegal mutual dependency between discrete-valued variables? #2639

Open
henrikt-ma opened this issue Aug 26, 2020 · 18 comments
Open

Comments

@henrikt-ma
Copy link
Collaborator

In appendix C, equation (C.1b), it is said that the discrete-valued variables m should be possible to determine by evaluation of fm(v, c). Even though this is some sort of high level informal description, the fact that this equation is given in the form of an assignment seems to suggest that given the other variables, one should be able to determine m in a straight-forward manner.

Does this mean that the following model does not fit this description, and therefore is invalid?

model MutualDiscreteValued
  Integer x;
  Integer y;
algorithm /* Use of algorithm instead of equation will become clear below. */
  x := y;
equation
  y = x;
end MutualDiscreteValued;

(SystemModeler currently rejects this model.)

If the model above is invalid, then what about this one?

model MutualDiscreteValuedUnused
  Integer x;
  Integer y;
algorithm
  x := y; /* Use of 'y' has no impact on the algorithm outputs. */
  x := 1;
equation
  y = x;
end MutualDiscreteValuedUnused;

The reason I ended up wondering is because of this model, where pre(x) takes the role of y during initialization:

model AlgorithmWithUnusedPre
  Integer x;
initial algorithm
  x := 1; /* Overwrites the value pre(x) formally assigned at the start of the algorithm. */
equation
  /* When-equation for x, resulting in
   *   x = pre(x)
   * during initialization, expected to be solved for pre(x).
   */
  when false then
    x = pre(x);
  end when;
end AlgorithmWithUnusedPre;

Of course, one of the assumptions in this last example was that the default equation for the inactive when-equation is really allowed to be solved for pre(x), which would actually need clarification in the specification considering that x is a discrete-time variable. Perhaps a clarification would be good either way?

@henrikt-ma
Copy link
Collaborator Author

For background, the problem I was trying to solve using the structure of AlgorithmWithUnusedPre was to use a variable to enforce an order between algorithm sections in the initialization problem. Maybe the correct way of doing this would be to use a parameter instead of a discrete-time variable? Like so:

model InitialAlgorithmOrdering
protected
  parameter Boolean initialAlgorithmComplete(fixed = false, start = false);
initial algorithm
  initializeExternalStuff();
  initialAlgorithmComplete := true;
algorithm
  assert(initialAlgorithmComplete, "Algorithms evaluated in the wrong order!");
  doStuffAssumingInitialized();
end InitialAlgorithmOrdering;

@HansOlsson
Copy link
Collaborator

I would say that the first two models are illegal. The fact that y has no impact in the algorithm in the 2nd example isn't something we would expect a tool to find.
Algorithms and equations for discrete variables can be sorted, but the algorithm-part rules out cycles. (Would be good if this was specified in more detail - similarly to https://specification.modelica.org/master/class-predefined-types-and-declarations.html#acyclic-bindings-of-constants-and-parameters

The InitialAlgorithmOrdering is on the other hand correct, as parameters with fixed=false are just unknowns for the initialization.

The AlgorithmWithUnusedPre should also be legal. The initialization problem becomes:

algorithm x:=1;
equation  x=pre(x);

where pre(x) has guess-value x.start. I admit that it's a bit weird to determine pre(x) in this backwards way, but at least it's consistent.

@henrikt-ma
Copy link
Collaborator Author

I would say that the first two models are illegal. The fact that y has no impact in the algorithm in the 2nd example isn't something we would expect a tool to find.
Algorithms and equations for discrete variables can be sorted, but the algorithm-part rules out cycles. (Would be good if this was specified in more detail - similarly to https://specification.modelica.org/master/class-predefined-types-and-declarations.html#acyclic-bindings-of-constants-and-parameters

Yes, that's the point of this issue. I can see how writing it nicely will be tricky, however, as one probably still want some kinds of simplifications to happen before analyzing the algorithm for dependencies, such as evaluation of if-equations and if-expressions with constant conditions, when-statement simplification for the initialization problem, etc…

@henrikt-ma
Copy link
Collaborator Author

The AlgorithmWithUnusedPre should also be legal. The initialization problem becomes:

algorithm x:=1;
equation  x=pre(x);

where pre(x) has guess-value x.start. I admit that it's a bit weird to determine pre(x) in this backwards way, but at least it's consistent.

Does this mean solving for a discrete-valued variable on the right hand side of an equation is OK in general? I've had the impression that all discrete-valued variables should have their own equation in solved form (with the variable on the left hand side of an equation or statement), but I'm not aware of this being explicitly stated anywhere…

@HansOlsson
Copy link
Collaborator

Does this mean solving for a discrete-valued variable on the right hand side of an equation is OK in general? I've had the impression that all discrete-valued variables should have their own equation in solved form (with the variable on the left hand side of an equation or statement), but I'm not aware of this being explicitly stated anywhere…

Good point. The restriction is not explicitly stated, but since we want to handle alias equations x=y due to connections without specifying alias-handling in detail it would make sense to allow it in solved form with the variable either on the left or the right hand side. I also noticed that the support in Dymola is somewhat inconsistent.

@eshmoylova
Copy link
Member

By the way, in appendix C Henrik linked above I see some strange \cref@addtoreset...:
image
Is it just my browser or can somebody else see it? Is that a known issue or do we need to file it?

@HansOlsson
Copy link
Collaborator

By the way, in appendix C Henrik linked above I see some strange \cref@addtoreset...:
image
Is it just my browser or can somebody else see it? Is that a known issue or do we need to file it?

Known issue #2629

@HansOlsson
Copy link
Collaborator

Something like the following:

It shall be possible to compute m without any cycles, provided that the rest of v is known (thus there might be cyclic dependencies between m and y that require the solution of systems of equations). The variables in m need to occur explicitly solved on one of the sides of an equation, or assigned in an algorithm.

@henrikt-ma
Copy link
Collaborator Author

Something like the following:

It shall be possible to compute m without any cycles, provided that the rest of v is known (thus there might be cyclic dependencies between m and y that require the solution of systems of equations). The variables in m need to occur explicitly solved on one of the sides of an equation, or assigned in an algorithm.

Almost. I'd like to split m into its continuous-valued (discrete-time Real) and discrete-valued parts (all the rest), and then apply the above to just the discrete-valued part. (While I see no reason to have this sort of constraint on discrete-time Real variables in general, it is of course a given for any discrete Real variable due to the current requirement of being assigned in a when-clause.)

@HansOlsson
Copy link
Collaborator

Something like the following:
It shall be possible to compute m without any cycles, provided that the rest of v is known (thus there might be cyclic dependencies between m and y that require the solution of systems of equations). The variables in m need to occur explicitly solved on one of the sides of an equation, or assigned in an algorithm.

Almost. I'd like to split m into its continuous-valued (discrete-time Real) and discrete-valued parts (all the rest), and then apply the above to just the discrete-valued part. (While I see no reason to have this sort of constraint on discrete-time Real variables in general, it is of course a given for any discrete Real variable due to the current requirement of being assigned in a when-clause.)

Being assigned in a when-clause does not prevent loops:

  when sample(2, 2) then
     x=A*pre(x)+B*u+time;
  end when;
  when sample(3, 3) then
     u=A*pre(u)+B*x; 
  end when;

@HansOlsson HansOlsson added this to the Phone2020-5 milestone Oct 26, 2020
@henrikt-ma
Copy link
Collaborator Author

Being assigned in a when-clause does not prevent loops:

  when sample(2, 2) then
     x=A*pre(x)+B*u+time;
  end when;
  when sample(3, 3) then
     u=A*pre(u)+B*x; 
  end when;

Right, being assigned in a when-clause just means that there is no point requiring that the variable appears "explicitly solved on one side of the sides of an equation". I don't think we need to forbid loops like this, at least not for the same reasons why we don't want mutually dependent discrete-valued variables?

@HansOlsson
Copy link
Collaborator

Being assigned in a when-clause does not prevent loops:

  when sample(2, 2) then
     x=A*pre(x)+B*u+time;
  end when;
  when sample(3, 3) then
     u=A*pre(u)+B*x; 
  end when;

Right, being assigned in a when-clause just means that there is no point requiring that the variable appears "explicitly solved on one side of the sides of an equation". I don't think we need to forbid loops like this, at least not for the same reasons why we don't want mutually dependent discrete-valued variables?

I agree that part is automatically true for when-clauses, but the proposed text:

It shall be possible to compute m without any cycles, provided that the rest of v is known (thus there might be cyclic dependencies between m and y that require the solution of systems of equations). The variables in m need to occur explicitly solved on one of the sides of an equation, or assigned in an algorithm.

have two parts: solvable without cycles (which this examples fail), and they need to be explicitly solvable from an equation (which when-clauses must satisfy).

Boolean equations can fail the first and/or the second part:

It could be that it is not in one of the allowed forms (this example could actually be solved):
(b == (x>2)) = time>=1;
Or it just form a boolean system of equations:

   b1=if b2 then time>=1 else time>=2;
   b2=if b1 then x>2 else false;

Note that the restriction to allowed forms says that the variables should occur explicitly, which is stronger than saying that discrete-valued equations must be on this form, consider:

   b1=if b2 then time>=1 else time>=2;
   b1=(b2==(x>=2);

Here b2 cannot be solved from any equation, and thus we don't have to figure out whether there is a cycle or not.

I don't see the point of making an exception for the second part for when-clauses merely because when-clauses automatically fulfill that.

@henrikt-ma
Copy link
Collaborator Author

It shall be possible to compute m without any cycles, provided that the rest of v is known (thus there might be cyclic dependencies between m and y that require the solution of systems of equations). The variables in m need to occur explicitly solved on one of the sides of an equation, or assigned in an algorithm.

have two parts: solvable without cycles (which this examples fail), and they need to be explicitly solvable from an equation (which when-clauses must satisfy).

Yes, and of the two parts, it's the cycles part that I don't find relevant for the discrete-time Real variables. (It was probably wrong to bring up that variables assigned in when-clauses already fulfill the other part.)

Boolean equations can fail the first and/or the second part:

Sure.

Here b2 cannot be solved from any equation, and thus we don't have to figure out whether there is a cycle or not.

Right.

I don't see the point of making an exception for the second part for when-clauses merely because when-clauses automatically fulfill that.

Agreed, there would be no point to make an exception for that reason. The reason for making an exception would be to not mix up the requirements needed for discrete-valued variables with any requirements needed for discrete-time variables. To me, the explicitly solvable and not-in-a-cycle has only to do with being discrete-valued, as it is the foundation for the "standard" fixed-point iteration method for solving systems of equations involving both discrete-valued and continuous-valued variables.

@HansOlsson
Copy link
Collaborator

Henrik: Start with discrete-valued ones. Requires splitting discrete-time variables in description.
Hans: Can delay discrete-Real restrictions later.
Agreement.

henrikt-ma added a commit to henrikt-ma/ModelicaSpecification that referenced this issue Nov 2, 2020
@HansOlsson
Copy link
Collaborator

Even if #2702 didn't fully solve this one I would propose to close this issue and if necessary (at some point) open a new cleaner issue for the remaining part.

@henrikt-ma
Copy link
Collaborator Author

Whether a discrete-valued variable could be solved on the right side of an equality was never the big question here, so I don't think having resolved #2702 is much of a reason to close this one. (But it is true that there are some parts that could be cleaned up as a result.)

@HansOlsson
Copy link
Collaborator

To me #2702 implicitly cleared up more than just right side of equality, so I'm unclear what remains of this one.

@henrikt-ma
Copy link
Collaborator Author

Things remaining:

  • Clearly state it's not OK to just throw away start expressions because the tool cannot find a way to evaluate them before they are needed. (The specification cannot prevent a tool from breaking the rules, but it would be madness to do so – in this case and in general – without at least warning the user about taking illegal action.)
  • Clarify that tools are not required to evaluate start expressions (just like pure expressions in general) if it can be proven that the result of the initialization does not depend on this start-value.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants