Semantics of guards

[jakhog]

While working on the Go compiler, I came across two questions that I haven't thought about before, related to events and guards.

1. Is the order of evaluation of guards defined?

E.g. do we evaluate the most specific guard (the guard with the most conditions) first? Is it in the order of appearance in the ThingML source? Or is it just up to the individual compilers to decide?

As an example:

   ...
   internal event m : SomePort?SomeMessage guard (m.A == 1) ...
   transition -> SomeState event m : SomePort?SomeMessage guard (m.A == 1 and m.B == 2) ...
   ...

Is the behaviour of this code defined if SomeMessage(1,2) is received on SomePort ? If so, what happens? The internal transition or the transition to SomeState?

2. Access to the events in guards

From the ThingML grammar, InternalTransitions and Transitions are pretty much the same, with the parts of interest for this question beeing these lines:

Transition returns Transition:
    ...
    ('event' event+=Event)*
    ('guard' guard=Expression)?
    ...
;

According to this rule, I should be able to write:

    ...
    transition -> SomeState
    event SomePort?SomeMessage
    event SomePort?SomeOtherMessage
    guard (SomeProperty == 0)
    ...

But what happens when I use the message parameters in the guard? Surely there will only be one actual message that you can access in the guard, so how do you know which one? E.g.

    ...
    transition -> SomeState
    event m1 : SomePort?SomeMessage
    event m2 : SomePort?SomeOtherMessage
    guard (m1.Parameter1 == 0 or m2.Parameter2 == 0)
    ...

I tried a simple program that did this, and there are no errors in Eclipse, neither does the compiler complain while generating platform code. For Java it fails to build, Arduino fails to compile, and NodeJS fails at runtime.

IMHO, it seems much more reasonable to have one guard per event. I.e. removing the guard from the Transition in the metamodel, and moving it to the Event. So that the grammar becomes something like this:

Transition returns Transition:
    ...
    ('event' event+=Event)*
    ...
;

Event:
    ReceiveMessage  ('guard' guard=Expression)?
;

[jakhog]

Thinking about it a tiny bit more, I see that you can get around the problem by splitting the transition into more definitions, and if you have a long action, put it inside a function.

But either way, the checker should complain about this case...

[brice-morin]

Well, I have never been a big fan of multiple events on a transition. This goes against @ffleurey principle of avoiding to provide two means to do one thing (except if it really simplifies things, like the long awaited >= and <=)... The proper way of doing it is to have two transitions, as you suggest. Of course, it might be that in some cases, we have to duplicate guards or actions, but just but them in a function so that you can factorize them. I vote for removing multiple events on transitions, because, as you pointed out, it makes reference to message's parameters messy. And the same behavior can be achieve in a clearer way by splitting transitions. Here the simplification of factorizing events actually makes thing blurry and harder to manage...

I do no think we impose any order on the evaluation of guards. In principle, we do not really like if two transition can be triggered at runtime, as this is not deterministic. In the general case, it is hard to know if the state machine will be deterministic, though the checker checks some simple cases e.g. one empty transition versus any other transition. But if transition are guarded with non-trivial expression, it will be hard to tell if they can evaluate to true at the same time. But I agree that we would need a common way for all compilers to make such behavior deterministic, i.e. to agree on which transition to trigger in case several can be triggered. In state.js library, I think they raise an exception in this case, which might be a bit extreme to my taste...

I however do not think we should directly guard events. Events are just data flowing around, while guards are more a control structure (basically, if statements). Keep the data "pure" and the control flow in the state machine and actions.

Anyway, good to hear you are working on a go compiler :-)

[jakhog]

Good 😄 I agree, just removing multiple events on transitions makes sense. And that would definitely be the solution that requires the least amount of changes in the compilers.

I would like the ability to do something like:

   transition
   event m : SomePort?SomeMessage guard (m.A == 1)
   event m : SomePort?SomeOtherMessage guard (m.B == 2)
   action ...

That would keep the related parts of code close together, but would require quite a lot of changes I guess. It's not very important either, It's more important to have a compiler that works 😄

Anyway, since we haven't had any problems with it yet, I guess it's quite the edge case. Personally, I don't think I have ever used multiple events before now 😛

Just so that we don't become too good friends, I would argue and say that it's the messages that are the data that is flowing around, and that an event is (possibly) triggered by a message.

[brice-morin]

Well, a message (at least in ThingML) is somehow a type/definition, like a function. The event carries the actual data. A bit like function and function calls. You do not get any data exchange before you "instantiate" the message into an event i.e. send and receive a message. For the same event, some might want to react on it, some might not (depending on guards). It it the same event, which can be of interest or not depending on the context. Anyway, we should not go too philosophical on this topic, I think. Or soon, we'll mention clabjects.....

[brice-morin]

Also in Java and JS compilers (maybe also in C), transitions with multiple events are just generated as multiple transitions. Having proper "atomic" transitions would simplify these compilers.

[jakhog]

Only a single event allowed from 74d44d81df9fa40dcbf4041d18220948aa2bce93