Separate anything and until

[MattWindsor91]

To allow until to be a generalised timeout operator, it makes sense to separate 'anything' and 'until' such that the former is an infinite loop over a message set and the latter is a linearised timeout.

The syntax in robocert-textual would likely flip ('until: X do: anything') or be clarified ('do: anything until: X'), or even be used to reflect the fact that until is similar to strict.

[MattWindsor91]

Draft tock-CSP semantics:

[[ any in X ]] = TCHAOS(X)

[[ until: X do: Y ]] = Y /\ X

This makes clear that each of these is a direct embedding of a CSP construct. It might be worth looking into whether PCTL and Isabelle-UTP will be able to capture these.

[MattWindsor91]

Adding question label as this needs to be discussed.

[MattWindsor91]

A big issue with the above semantics is that it doesn't induces nondeterminism if Y performs any of the initial events in X. Instead, I think we need something like

Do(P, initials) = P [| Universe |] TCHAOS(diff(Universe, initials))

This process ensures that P cannot perform any events in initials.

I would also change the textual semantics to do X until Y.

[MattWindsor91]

Done a while back.