Add infinite loops

[MattWindsor91]

One of the properties I want to formulate in my case study is of the form 'the robot can only call Foo and Bar in an alternating manner, starting with Foo'.

This would translate into a sequence diagram of the form

sequence S for module Mod as M with world as W {
    loop {
        anything except { operation bar() from M to W } until
            operation foo() from M to W
        then anything except { operation foo() from M to W } until
            operation bar() from M to W 
    }
}

These loops don't yet need a method of breaking, but one will need to be added eventually.

I suspect the translation will look something like this (assuming #8):

S = let Loop =
    RUN(diff(Events, {| Mod::fooCall, Mod::barCall |})) /\ mod::fooCall -> Skip;
    RUN(diff(Events, {| Mod::fooCall, Mod::barCall |})) /\ mod::barCall -> Skip;
    Loop
within Loop

which might need some sort of state for tracking which loops are currently inside the sequence to avoid naming clashes, unless CSPM scoping gets us that far.

An interesting point with this construct is that validation should allow the final action in the sequence to be a loop as long as it's infinite.