Skip to content

Dear Developers,

On https://www.eclipse.org/escet/cif/language-tutorial/data/state-evt-excl-invariants.html is written:

It is therefore not possible to give a name to a combined invariant that applies to multiple events.

Imho it is (fundamentally) possible. E.g. with syntax like

invariant no_emergency : {motor.turn_on, door.close} needs emergency_button.released; 

So would a slightly weaker statement like

It is not supported to give a name to a combined invariant that applies to multiple events.

not be better?

Greetings, Pierre