search

UoY-RoboStar / robocert-textual

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

Add alt blocks (if statements) #14

Closed MattWindsor91 closed 3 years ago

MattWindsor91 commented 3 years ago

Per #12, we have at least one property that, at its most low-level formulation, would require an if statement.

MattWindsor91 commented 3 years ago

Quoting UML2.5.1:

'The interactionOperator alt designates that the CombinedFragment represents a choice of behavior. At most one of the operands will be chosen. The chosen operand must have an explicit or implicit guard expression that evaluates to true at this point in the interaction. An implicit true guard is implied if the operand has no guard.'

So, this is not an if statement, this is (as STAIRS suggests) more like a guarded nondeterministic choice. (Or at least it makes sense for it to be so under trace semantics; under tick-tock, maybe not so?)

See #52 for the analogue of STAIRS's xalt.

MattWindsor91 commented 3 years ago

Available now, but see #72.