UoY-RoboStar / robocert-textual

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

Capture distinction between provisional and mandatory arrows #67

Closed MattWindsor91 closed 2 years ago

MattWindsor91 commented 3 years ago

Targeting the tick-tock model has pushed the issue of whether arrow actions are provisional (eg, we don't require the model to actually accept them when the environment offers them, at least not initially) or mandatory (eg. we do) onto the forefront of the sequences semantics. My feeling is that we should:

Some possible dichotomies which would appear as keywords:

I'm unsure what the graphical distinction would be, but probably the same as LSC. LSC temperature semantics might be the best initial way of representing this in the textual one, too.

Note that this dichotomy doesn't appear in other actions, as they have no initial events other than tock, and actions are defined as things that can take an arbitrary amount of time to occur (and so, they always accept tock, #65 notwithstanding).

MattWindsor91 commented 2 years ago

We use hot/cold at the moment, but the name may change later.