State machine example incorrectly produces overdetermined system

[jwharington@…]

Two equivalent codes, simulating the startup sequence of a state machine.

This first code does not compile (overdetermined system):

class stateinit

  class StateMachine
    Boolean active;
    Boolean init;
  algorithm

    when init then
      init := false;
      // do something, next state
    end when;

  end StateMachine;

  StateMachine statemachine;

algorithm
  when time > 0.1 then
    // activate state machine, initial state
    statemachine.init := true;
    statemachine.active := true;
  end when;

end stateinit;

But this code does compile fine:

class stateinit2

  class StateMachine
    Boolean active;
    Boolean init;
  algorithm

    when active then
      init := true;
      // activate initial state
    end when;

    when init then
      init := false;
      // do something, next state
    end when;

  end StateMachine;

  StateMachine statemachine;

algorithm
  when time > 0.1 then
    // activate state machine
    statemachine.active := true;
  end when;

end stateinit2;

Now, here's a weird thing. When I take the flattened code of the first example (stateinit), replace '.' with '_' and compile it, it compiles and works fine.

class stateinit3
  Boolean statemachine_active;
  Boolean statemachine_init;
algorithm
  when statemachine_init then
    statemachine_init := false;
  end when;
  when time > 0.1 then
    statemachine_init := true;
    statemachine_active := true;
  end when;
end stateinit3;

How is it the first example fails, yet the same flattened code compiles fine on its own?

[Martin Sjölund]

All of the examples should fail according to the language specification (8.3.5.3
Application of the Single-assignment Rule to When-Equations). Someone who works on the backend should probably enforce this restriction. If you want to set the same variable on two different conditions, you have to use elsewhen.

[Lennart Ochel]

Sure, that code is invalid because of the single assignment rule. But I guess this kind of language check should be done in the frontend, or not?

[Martin Sjölund]

No, this is a check for the backend. OpenModelica frontend doesn't even do equation counting. Many checks have to be done in the backend (like making sure reinit is called on a variable selected as a state).

The single-assignment rule is already handled in the backend anyway (for normal equations). Consider:

model M
  Real x,y;
equation
  x = 2*time;
  x = 3*time;
end M;

[Lennart Ochel]

Sure, then you are right. I thought that was already done when any model pass my implementations inside the compiler… so from now on I will take care if it :)

[jwharington@…]

For what it's worth, here's a little more information about the problem as it occurred for me.
We had code produced by the ModelicaML/eclipse system from a few years ago, then hand edited. This implemented a state machine. In recent (later than around r13600) builds of openmodelica, the code now refuses to compile. It's quite possible the code generation templates, or our hand-edits, did something illegal that nevertheless worked in earlier versions of the compiler. Recently, I've tried to simplify down the code to bare minimum to try to find the culprit.

In this case, what's very strange is that the first example fails to compile, yet the third code, being what is essentially the flattened code from the first example, does compile.

I don't quite understand why the first/third code is perhaps more illegal than the second, because the only change there is to make the init=true activation indirect. The code produced by ModelicaML was more like the first example, if I recall correctly.

[Willi Braun]

As far as I see we just count wrong and the models are valid, the single assignment rule is only applicable on when equations, but in this case we have algorithms, so the rule doesn't matter, since an algorithm may have as many assignment to one variable as it's wanted.

The following model is correct and works fine.

model A
 Real x;
algorithm
 when time > 0.1 then
   x := 3;
 end when;
 when time > 0.5 then
  x := 5;
 end when;
end A;

[Willi Braun]

Ups, this model "stateinit" isn't really valid, since two different algorithm section
have the same variable "statemachine.init" and "init" as output. So the counting is correct.
Replying to jwharington@…:

class stateinit

  class StateMachine
    Boolean active;
    Boolean init;
  algorithm

    when init then
      init := false;
      // do something, next state
    end when;

  end StateMachine;

  StateMachine statemachine;

algorithm
  when time > 0.1 then
    // activate state machine, initial state
    statemachine.init := true;
    statemachine.active := true;
  end when;

end stateinit;

This model "stateinit2" is valid and compiles correct.
Replying to jwharington@…:

class stateinit2

  class StateMachine
    Boolean active;
    Boolean init;
  algorithm

    when active then
      init := true;
      // activate initial state
    end when;

    when init then
      init := false;
      // do something, next state
    end when;

  end StateMachine;

  StateMachine statemachine;

algorithm
  when time > 0.1 then
    // activate state machine
    statemachine.active := true;
  end when;

end stateinit2;

Now, here's a weird thing. When I take the flattened code of the first example (stateinit), replace '.' with '_' and compile it, it compiles and works fine.

class stateinit3
  Boolean statemachine_active;
  Boolean statemachine_init;
algorithm
  when statemachine_init then
    statemachine_init := false;
  end when;
  when time > 0.1 then
    statemachine_init := true;
    statemachine_active := true;
  end when;
end stateinit3;

How is it the first example fails, yet the same flattened code compiles fine on its own?

No, it's not wired. Since in the flatten output doesn't distinguish between different algorithm sections and outputs them together this yields in an valid model.

[jwharington@…]

wbraun, thanks for the input. I also believed that for algorithms and discrete variables, that the limit of single assignment wouldn't apply. So your comment6 made me feel better.
Your comment7 helps clarify why I thought the behaviour was weird, so that's good. But if single assignment doesn't apply to algorithms, why does it matter if the algorithms are in separate algorithm sections?

[Martin Sjölund]

That's easy to answer: each algorithm section counts as one equation with the outputs considered to be the variables you assign to.

So the following is ok (one equation that assigns to a)

algorithm
  a := 1;
  a := a+1;

But this is not (two equations that assign to a)

algorithm
  a := 1;
algorithm
  a := a+1;

[jwharington@…]

sjoelund.se: thanks for the explanation, that helps.

[Martin Sjölund]

Postponed until 1.9.1

[Martin Sjölund]

This ticket was not closed for 1.9.1, which has now been released. It was batch modified for milestone 1.9.2 (but maybe an empty milestone was more appropriate; feel free to change it).

[Martin Sjölund]

Milestone changed to 1.9.3 since 1.9.2 was released.

[Martin Sjölund]

Moved to new milestone 1.9.4

[Martin Sjölund]

Milestone pushed to 1.9.5

[Martin Sjölund]

Milestone renamed

[Martin Sjölund]

Ticket retargeted after milestone closed

[Martin Sjölund]

Milestone moved to 1.12.0 due to 1.11.0 already being released.

[Francesco Casella]

I guess the issues were clarified by the various comments. If not, please reopen.