Suspicious reference result for Modelica.Clocked.Examples.Elementary.ClockSignals.LogicalSample

[rfranke]

MSL 4.0.0 and trunk contain the example Modelica.Clocked.Examples.Elementary.ClockSignals.LogicalSample and document the expected result with a screenshot from Dymola. According to this, the variable rotational_clock_2.direction should get the value 1 at initial time, even though there doesn't appear to be an event triggering the respective clock:

The following example might exhibit the same problem. It counts the changes from negative to positive of cosine in two ways:

model EventClockAndClassic
  Real f = cos(5*time*Modelica.Constants.pi);
  Boolean condition = f > 0;
  Integer count1(start = 0);
  Integer count2;
initial equation 
  count2 = 0;
equation 
  when Clock(condition) then
    count1 = previous(count1) + 1;
  end when;
  when condition then
    count2 = pre(count2) + 1;
  end when;
end EventClockAndClassic;

The expected result is that count1 and count2 are identical. Dymola 2021 triggers the clock for count1 additionally at initial time:

[henrikt-ma]

For what it's worth, System Modeler gives the same result as reported here for Dymola 2021. As I cant find support for this behavior in the specification of event clock, I suspect that the behavior seen in System Modeler is merely a consequence of trying to match the MSL reference results.

[christoff-buerger]

I think the reference results are correct. Before investigating them closer, I like to remind first however, that initial conditions etc are not well-defined for clocked partitions (see MCP 0038).

Modelica.Clocked.Examples.Elementary.ClockSignals.LogicalSample

rotational_clock_2 has the cosine as input, which at t=0 is 10; its trigger interval, which defines how much its input angle must have changed for the clock to tick, is 3 at t=0. The initialization will not make the clock tick! Thus, the t=0 tick is not a product of initialization. But right after initialization, at t=0 the clock immediately ticks, because the difference of the last tick's angle (since there is no last the default value 0 is used) and the current one is > the trigger interval.

You may wonder, why initialization does not set 10 as start value for the angle, but instead for the first computation 0 is used as last angle. If you look into the clock you see that the previous angle is modeled by a hold. That very hold has 0.0 as fixed start value. There is no way to do that any better in current Modelica. Clocked partitions -- and in particular holds and samples -- are not subject to normal initialization yet; this means in particular that initial values computed for the inputs of samples are not propagated/pushed inside clocked partitions and that we have no means to compute initial values for holds (only fixed values can be given and whichever fixed value we give here, it might cause an unwanted trigger at t=0 or miss a wanted one). In other words, clocked partitions have no initialization in current Modelica. They just have a first tick, at which time for the first time values for clocked stuff are computed (the only exception is previous and pre -- whereas for pre I think its use is even undefined in clocked partitions). That is what MCP 0038 likes to improve.

EventClockAndClassic

Your event clock example is slightly different. I do not understand why you wouldn't like the clock to tick at t=0? Your condition clearly is satisfied and a rising edge at t=0; it just happens to be satisfied at t=0. I am more surprised for count2. Why is the when not triggered at t=0?

EDIT: The question "I am more surprised for count2. Why is the when not triggered at t=0?" is answered by @henrikt-ma below. The when has no initial().

If you want count1 not to tick at t=0, you have to make sure there is no rising edge. You can do that by giving condition a proper start value:

model EventClockAndClassic
  Real f = cos(5*time*Modelica.Constants.pi);
  Boolean condition(start = true) = f > 0;
  Integer count1(start = 0);
  Integer count2;
initial equation 
  count2 = 0;
equation 
  when Clock(condition) then
    count1 = previous(count1) + 1;
  end when;
  when condition then
    count2 = pre(count2) + 1;
  end when;
end EventClockAndClassic;

Btw., I like to remind that count1 has no value until the first clock tick! Thus, in above modeling with condition(start = true) the count1 variable is never assigned any value until t=0.3.

[henrikt-ma]

Am I right if I think that the essence of your point is captured by this model?

model StartPreEdge
  Boolean b(start = false, fixed = true) = true;
  Boolean y(start = false, fixed = true);
equation
  when b then /* Will this trigger in the first turn of initial event iteration? */
    y = true;
  end when;
end StartPreEdge;

As I interpret this model, we'll have pre(b) = false and b = true after the first phase of initialization. In this phase, the when-clause is not triggered simply because it isn't enabled with initial(). We'll now run the initial event iteration to find a fixed point with pre(b) = b. Thus, we set pre(b) := true and evaluate the equations, giving b = true. The when-condition doesn't trigger, and the initial even iteration is complete.

In other words, specifying b.start caused the initial even iteration to make one turn, but didn't affect the triggering of the when-clause. I would have expected the same for condition.start in your example, which would be the reason why count2 doesn't tick at start.

Edit: Added fixed = true to the variables.

[christoff-buerger]

In this phase, the when-clause is not triggered simply because it isn't enabled with initial().

You are right! That's what I missed regarding the when-clause of count2 and explains its behavior. That was a confusion on my side regarding the when-clause of count2.

The argument for count1 still stays the same. For the event clock the condition changes from false to true (is a rising edge) at t=0, except when you say Boolean condition(start = true). Or did I miss that we have initial() also defined for clock whens?

Anyway, Modelica.Clocked.Examples.Elementary.ClockSignals.LogicalSample is a completely different issue. The simulation results are correct due to the hold 0.0 within the rotational clock.

[henrikt-ma]

The argument for count1 still stays the same. For the event clock the condition changes from false to true (is a rising edge) at t=0, except when you say Boolean condition(start = true). Or did I miss that we have initial() also defined for clock whens?

I know I mentioned it first, but I think we should avoid involving initial() too much in this discussion. For me, it seems odd that a condition that doesn't trigger a when-clause would at the same time be able to trigger an event clock. Maybe we need to engage in splitting hairs to resolve this. The spec says (emphasis is mine):

when edge(condition) becomes true

So, can we really say that the condition becomes true at the first phase of initialization? There was no past at this point, so even though edge(condition) is true, one would actually need to clarify whether it should be considered becoming true.

For consistency with when-clauses, it might be advantageous to not define it as becoming true, consistent with the results seen in tools today.

[rfranke]

@christoff-buerger: good that you can explain the result. Still it appears odd that the same condition variable gives two different behaviors. The model EventClockAndClassic says:

  Real f = cos(5*time*Modelica.Constants.pi);
  Boolean condition = f > 0;

Meaning that the first value of condition at time=0 is true during initialization and condition.start should be irrelevant. Start values are more binding for clocked variables. But condition is not clocked and thus the start value just provides a guess.

[henrikt-ma]

Meaning that the first value of condition at time=0 is true during initialization and condition.start should be irrelevant. Start values are more binding for clocked variables. But condition is not clocked and thus the start value just provides a guess.

No, condition.start is not just a guess, at least not when condition.fixed = true. It is also the value of pre(condition) in the initialization problem, since condition is a discrete-time variable. This is what causes the confusion about whether edge(condition) (which is hence true in the initialization problem) is triggering the event clock or not.

(When condition.fixed = false, I'm not sure whether a tool should add the equation pre(condition) = condition or pre(condition) = condition.start to balance the initialization problem.)

[christoff-buerger]

It seems we are getting stuck on the EventClockAndClassic example. I would like to pick up again the original issue of Suspicious reference result for Modelica.Clocked.Examples.Elementary.ClockSignals.LogicalSample.

Regarding the LogicalSample, I think:

1. The reference result documented in the MSL is correct.
2. It is correct regardless of the interpretation of initialization.
3. Its modeling, and result, is not similar to the EventClockAndClassic example. Thus, I think the original claim of @rfranke is incorrect, that

   The following example might exhibit the same problem.

My rationale:

• The used rotational clocks work as follows: They compare the old angle with the current angle. The current angle is a continuous value; the old is stored by means of a clocked partition triggered by the clock itself. The hold, holding the old value has a fixed start value 0.0.
• At t=0, the continuous angle is 10; the old angle is the fixed start value of the hold, holding the old angle, which is 0.0. The absolute difference between old angle and new is 10, which is greater than the required interval to trigger the clock. Hence the clock ticks at t=0.

We can argue if the modelling is nice. As author of it, I am aware that it can not yield satisfying clock behaviour at t=0 for every possible application context; in some applications, one would like a rotational clock to start ticking right from the beginning at t=0, in others not. But to my defense, I like to add, that I am also not aware of any universal modelling that can adjust to the application context automatically; this would require to leverage on initialization knowledge derived from the continuous parts in combination with the clocked. Such means are not given in the current Modelica specification. Quiet contrary, the current Modelica specification explicitly excludes clocked partitions from normal initialization. And I think that any more clever modelling would for now actually run into the issue of undefined behaviour. The current modelling has at least the advantage to be well-defined and clear specification-wise.

The only improvement I can see is to add a parameter to define the fixed start value of the hold; this would give users a means to adjust the starting behaviour, but also puts the burden on them to actually guess a good start value. A better approach might be to combine such parametrization in some way so a user can say "if the clock can tick at t=0 or not" (big emphasizes on can); still a user would have to select statically if it can tick at t=0 or not.

I will investigate to add these improvements.

With respect to EventClockAndClassic, I have to say: I am not sure what we want and what it should be according to the current specification. I have to think more about it. But I am sure it is irrelevant for the Modelica.Clocked.Examples.Elementary.ClockSignals.LogicalSample example of the MSL.

@rfranke and @henrikt-ma: Can you follow this rationale? If yes, I would propose to open a separate issue for EventClockAndClassic and close this one.

[henrikt-ma]

I've yet to be convinced that EventClockAndClassic isn't related to LogicalSample, and it's related to my inability to follow the rationale above. The problem for me is the conclusion Hence the clock ticks a t=0. I can see that rotational_clock_2.y_clock.u is true during initialization, but I don't see that edge(rotational_clock_2.y_clock.u) becomes true at initialization. Beside the question of how to interpret becomes (which is what we were discussing in the context of EventClockAndClassic), I'd even expect edge(rotational_clock_2.y_clock.u) to be false. I come to this conclusion as there is no equation given for pre(rotational_clock_2.y_clock.u) in the initialization problem, and I'd expect a tool to choose to add the equation pre(rotational_clock_2.y_clock.u) = rotational_clock_2.y_clock.u to balance the initialization problem, hence making edge(rotational_clock_2.y_clock.u) false.

We can argue if the modelling is nice.

I can see that not triggering the event clock at initialization would be a real issue for the model, as it would allow the angle to grow indefinitely without triggering comparison, but I'll try to avoid getting involved in this part. For me it seems more important right now to sort out what the correct result is, and for what reasons.

[rfranke]

I get from the explanation by @christoff-buerger above that cosine_angle_input.y shall be zero during initialization at time == 0 and jump to 10 immediately afterwards, triggering rotational_clock_2.y_clock.u. It is defined like:

model C
  Real y = if time < 0 then 0 else 10;
end C;

I don't see a big difference to

model B
  Boolean condition = cos(time) > 0;
end B;

[henrikt-ma]

I get from the explanation by @christoff-buerger above that cosine_angle_input.y shall be zero during initialization at time == 0 and jump to 10 immediately afterwards

I don't think he said that. The cosine_angle_input.y is a continuous-time variable given by an expression which simplifies to 10 * cos(2 * pi * time) with given parameter values and a simulation starting at time = 0. It is a non-discrete-time Real variable, so at initialization pre(cosine_angle_input.y) = cosine_angle_input.y = 10.

The variable that might jump from 0 to 10 is rotational_clock_2.angular_offset.y, but only if the event clock actually triggers during initialization. This jump is needed to bring the absolute difference down below the abs(rotational_clock_2.trigger_interval) = 3, so that a new event will be triggered when the angle crosses 7 or 13 (disregarding the fact that rotational_clock_2.trigger_interval alters between 3 and 1). If the jump doesn't happen because the event clock doesn't trigger at initialization (discussion of this issue), the hold will in a bad state, and the rotational_clock_2.angle would need to enter the (-3, 3) range to get out of the bad state, and only after that could the event clock tick for the first time.

[christoff-buerger]

I can see that rotational_clock_2.y_clock.u is true during initialization, but I don't see that edge(rotational_clock_2.y_clock.u) becomes true at initialization.

Yes, that is the question!

It is late and I have to rant a bit now; I am sorry for that! Here we go...

I can see that rotational_clock_2.y_clock.u is true during initialization, but I don't see that edge(rotational_clock_2.y_clock.u) becomes true at initialization.

I am not sure if that is related to the clocked partition at all according to the current Modelica specification, since clocks are not permitted to tick throughout initialization if I am not mistaken (I am aware that this may be an arguable requirement).

The question then is: What do we do if a clock condition becomes true during initialization? I think, this is undefined and cannot be handled by the current spec because it is a hard contradiction to the requirement that clocks don't tick throughout initialization. This will lead to initialization contradictions, I don't think any tooling detects yet and respectively fails with an error.

For the given examples we have to ask the question:

• Are we on undefined/inconsistent territory in that throughout initialization we see a rising edge for the clock's condition?
• Are we on troublesome territory in that initialization finally yields/settles with falsefor the condition (maybe to avoid a rising edge...) which at t=0 is immediately evaluated to true?
• Or is the current Dymola result just wrong, in that the condition was always true, and stays true at t=0? Related to that question we can ask if there is some freedom in the initialization to settle with that conclusion if other possible initial selections would be possible?

Honestly, the whole issue is a bottomless pit. The answers I heard so far are always that Modelica synchronous is well-defined, because it is build on top of well-defined formal semantics of synchronous languages like Estrel or Lustre. But these languages are purely synchronous; they avoid the issues of integrating the continuous and synchronous paradigms! But this are the really hard issues. Initialization for example is really tricky now, because on the one hand clocks shouldn't tick (for example because of side-effects like counters in them) and on the other hand initialization of a continuous + synchronous mixed system easily becomes contradicting if clocks must not tick through initialization (for example if we encounter a rising edge for an event clock throughout initialization). A purely synchronous language is trivial compared to the issues we see in Modelica; very, very simple and the (sorry for the wording) shit is blowing up slowly.

[christoff-buerger]

I get from the explanation by @christoff-buerger above that cosine_angle_input.y shall be zero during initialization at time == 0 and jump to 10 immediately afterwards

I don't think he said that. The cosine_angle_input.y is a continuous-time variable given by an expression which simplifies to 10 cos(2 pi * time) with given parameter values and a simulation starting at time = 0. It is a non-discrete-time Real variable, so at initialization pre(cosine_angle_input.y) = cosine_angle_input.y = 10.

The variable that might jump from 0 to 10 is rotational_clock_2.angular_offset.y, but only if the event clock actually triggers during initialization. This jump is needed to bring the absolute difference down below the abs(rotational_clock_2.trigger_interval) = 3, so that a new event will be triggered when the angle crosses 7 or 13 (disregarding the fact that rotational_clock_2.trigger_interval alters between 3 and 1). If the jump doesn't happen because the event clock doesn't trigger at initialization (discussion of this issue), the hold will in a bad state, and the rotational_clock_2.angle would need to enter the (-3, 3) range to get out of the bad state, and only after that could the event clock tick for the first time.

Yes @henrikt-ma, you understood me right. cosine_angle_input.y should be initialized to 10.

The variable that might jump from 0 to 10 is rotational_clock_2.angular_offset.y, but only if the event clock actually triggers during initialization.

...or triggers at t=0, immediately after initialization because initialization sets the condition of the clock to false, but it will evaluate to true at t=0 triggering the event clock.

And that might be the actual thing Dymola does. It keeps the condition false, in the try to avoid any change of the Boolean from false to true throughout initialization. The reason I can see for such a hack is that the default starting value for a Boolean is false; thus, if its start value is not fixed true, we might indeed see a false->true change throughout initialization which for clock conditions is troublesome (violation of Modelica synchronous semantics). In other words, we might not conclude that "having true as condition value to start with, keep it like that throughout the whole initialization and start integration at t=0 with the condition true would avoid any clock tick".

This surely would be wrong in this case. But due to possible negations the strategy Boolean values = true at initialization might be wrong in other scenarios.

I played a bit with setting fixed start values for the less.y output, but it changes nothing. This hints in my opinion to some bug. Because for fixed less.y.start=true, combined with the clock not ticking, the clock should also not tick at t=0. But it does... arghhh -- at least it should fail with "doesn't work due to contradicting initializations".

How does that scenario look in System Modeler (setting fixed start values for the condition)?

Important edit

Instead of setting less.y.start=true I played with setting fixed y_clock.u.start=true. Now Dymola correctly concludes that the clock does not tick at t=0 (its condition is true since ever, and now after initialization when integration starts at t=0, still is true).

I conclude from that, that we have some hack of the form clock.u.start=false throughout initialization for event clocks. And thinking about it (requirement that event clocks must not tick throughout initialization according to Modelica specification) I think this hack is a requirement. What we could improve is that we conclude: It would become true, but must not, thus we have an initialization contradiction => fail". But that is also troublesome.

[rfranke]

OK, I was referring to: "But right after initialization, at t=0 the clock immediately ticks, because the difference of the last tick's angle (since there is no last the default value 0 is used) and the current one is > the trigger interval." So, "0" is meant for the difference not for the angle.

[henrikt-ma]

I'm not sure where to start, but commenting on this is easy:

How does that scenario look in System Modeler (setting fixed start values for the condition)? … Instead of setting less.y.start=true I played with setting fixed y_clock.u.start=true. Now Dymola correctly concludes that the clock does not tick at t=0 (its condition is true since ever, and now after initialization when integration starts at t=0, still is true).

I conclude from that, that we have some hack of the form clock.u.start=false throughout initialization for event clocks. And thinking about it (requirement that event clocks must not tick throughout initialization according to Modelica specification) I think this hack is a requirement. What we could improve is that we conclude: It would become true, but must not, thus we have an initialization contradiction => fail". But that is also troublesome.

The System Modeler hack is different and doesn't care about y_clock.u.start. Basically, System Modeler checks for the edge of the condition becoming true, and then has some special logic that additionally allows the clock to trigger if the condition is true on first encounter. My guess is that the special is simply there to match the MSL reference results.

In this hackery territory System Modeler has an inconsistency which forces me to use the expression time > -1 instead of true to avoid extrapolating the truth to the behavior of the ideal System Modeler. That said, the following example shows the System Modeler behavior very concretely. In this model, the clock ticks at the initial time 0 regardless of cond.start:

model StartPreEdgeEventClock
  Boolean cond(start = false, fixed = true) = time > -1;
  Boolean ticked(start = false, fixed = true);
equation
  when Clock(cond) then
    ticked = true;
  end when;
end StartPreEdgeEventClock;

If the expression for cond is changed to true, the hack is bypassed, and the clock doesn't tick at all.

[henrikt-ma]

Honestly, the whole issue is a bottomless pit. …

I don't know about the bigger picture, but in this particular case I'm not sure there's no bottom.

The issues it would cause for models like LogicalSample aside, I don't see why the solution isn't simply that an event clock only ticks when edge(cond) becomes true, meaning that it cannot tick during the first phase of initialization. This seems consistent with clocks not ticking during initialization, which could actually be an observation rather than a rule. Instead of getting an event clock tick during initialization, the model needs to be set up for the event to happen during the initial event iteration instead.

This is how one should be able to control whether the clock ticks during initial event iteration or not (but the hack added to System Modeler makes it not work as expected):

model InitialTickControl
  parameter Boolean enableInitialTick = false;
  Boolean cond(start = not enableInitialTick , fixed = true);
  Clock clk = Clock(cond); /* Give the clock a name just to facilitate investigation. */
  Boolean ticked(start = false, fixed = true);
equation
  when not initial() then
    cond = true;
  end when;
  when clk then
    ticked = true;
  end when;
end InitialTickControl;