Assertions in the model

[jakhog]

As discussed, we should introduce assertions in the metamodel, that is, checks that are evaluated at run-time.

The first concrete example of this is to assert that messages are handled within a state. This would be a very usefull feature, both for making sure that you don't forget to handle messages in your own code, and also if you write a framework for someone else to implement (like in the courses using ThingML for teaching). The current way to do this is to manually create internal transitions and print actions for each message you want to make sure is handled.

Proposed syntax:

   message A
   message B
   message C

   port P1 { receives A, B, C }
   port P2 { receives A, B, C }

   (state | composite state | session | region) State {
     assert handles P1?A, P1?B
   }

The semantics behind this, would be that if the statemacine is currently in State and messages A or B is received on port P1, and is not handled by either State itself, or any substate of State. An error will be automatically printed on the output (using the same mechanism as an error action), and the message will be considered as handled. In other words, it will not be handled by superstates of State.

Sidenote 1:

This is a place where it might make sense to allow wildcards in ports/messages to ease assertions of multiple messages. E.g. P1?* for all messages on port P1, or *?* for all messages on all ports.

Sidenote 2:

I don't know if the default behaviour should be printing an error or crashing. But it might be good to have an annotation that allows the other behaviour in any case.

@ffleurey @brice-morin any comments on the syntax or the behaviour?

[jakhog]

Sidenote 3:

IMO, it would be good to keep the syntax when it comes to assertions somewhat general. I guess there are other assertions that also could be interesting to have a look at. E.g. invariants.

[jakhog]

Sidenote 4:

Another thing that we also discussed in the same session, is about defers. Where the meaning would be that a deferred message is considered handled, but put back into the receive queue, to allow handling in a coming state.

This is really a separate issue, but since we have not decided on anything yet. I just leave it here (at least until we close this issue, or someone makes a new one).

[brice-morin]

Note that it seems we could implement it as a ThingML tool, a bit like we do for the logging (where we actually report on events that are not handled).