UoY-RoboStar / robocert-textual

Textual plugin and CSP generator for RoboCert
Eclipse Public License 2.0
2 stars 0 forks source link

Resolve semantics of gaps across n-lifeline sequences #92

Closed MattWindsor91 closed 2 years ago

MattWindsor91 commented 2 years ago

The semantics of a gap in a system diagram is to be a TCHAOS over the allowed set on the single module lifeline interrupted by the action of the action step. This issue is me saying that I need to think about the correct way to generalise this semantics.

Some possible approaches:

It'd be nice to have the second semantics if possible, but maybe it's counterintuitive.

MattWindsor91 commented 2 years ago

Done (we decided to make it affect all actors, but with a heavy synchronisation on both sides).