Semantics of the strict operator, given a cursory glance of COMPASS D22.4, looks like we introduce a channel strict.x.y for every strict step x and nested element y, and use them to synchronise after every y. So the pseudo-RoboCert
strict:
always:
op foo from A to W
always:
op bar from B to W
always:
op baz from C to W
becomes something like
A = fooCall -> strict.0.0 -> strict.0.1 -> strict.0.2
B = strict.0.0 -> barCall -> strict.0.1 -> strict.0.2
C = strict.0.0 -> strict.0.1 -> bazCall -> strict.0.2
We have the parallel, alt, and loop operators already, but at least one example in the testbed requires the strict operator.
Semantics of the strict operator, given a cursory glance of COMPASS D22.4, looks like we introduce a channel
strict.x.y
for every strict stepx
and nested elementy
, and use them to synchronise after everyy
. So the pseudo-RoboCertbecomes something like