Add guards

[MattWindsor91]

In my implementation of #14 and #52, I've decided to implement the blocks first and then add guards later (mainly once I fix #12). This issue tracks guards, working out how to express them, etc.

My gut feeling is that guards translate quite transparently into a Step or Action implementing the & operator in CSP, albeit with the appropriate expression elaboration. In fact, we might be able to lift the LSC notion of hot and cold conditions here. It may be that this is overly naive.

[MattWindsor91]

Draft syntax:

require EXP

(Possibly assert EXP or when EXP, but we need to bear in mind that these will be used at least initially to encode the branch conditions of if statements. We may want some syntactic sugar for this eventually.)

I think the translation of a condition will look something like

[[ require EXP ]] = ([[ memory accesses for EXP ]] -> [[ EXP ]] & SKIP)

bearing in mind that, in tock-csp, the semantics of e & P is P when e is true and STOP otherwise. The use of STOP here is appealing in that it closes off branches in hot alternatives, but we might need to think about cold alternatives.

This is closer to a LSC hot condition than a cold condition, as cold conditions break (and we'll probably be adopting the UML break syntax for that).

[MattWindsor91]

I've added something like this, but in discussion with Ana it's become evident that it'll need to be switched to be part of a BranchStep's branches.

I'm thinking we'll have something like this:

• make a Branch class containing a Subsequence and a Guard;
• allow a Guard to be an ImplicitGuard, an ExprGuard with an expression, or an ElseGuard (adding the last one later on);
• have the semantics be [[ body ]] for ImplicitGuard, [[ EXP ]] & [[ body ]] for ExprGuard, and [[ !(conjunction of all parent ExprGuards) ]] & [[ body ]] for ElseGuard.

[MattWindsor91]

This has been done now, just awaiting testing. Will close and reopen if it needs reworking.