search

UoY-RoboStar / robocert-textual

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

Consider adding mandatory choice (xalt) #52

Closed MattWindsor91 closed 2 years ago

MattWindsor91 commented 3 years ago

I'm currently reading a few papers based on STAIRS, whereby it's discussed that there is a distinction in refinement treatments of sequence diagrams between alt blocks that permit underspecification (eg, |~|) and xalt blocks that require all alternatives to be reachable (eg, []). This is a note to myself that I need to consider this distinction and possibly add something similar to robocert.

One interesting thing that I haven't quite got into yet is how this interacts with guards on the legs of the alt and xalt. Maybe these just legitimately become &-guards at the CSP level, with all the semantic ramifications one would expect.

MattWindsor91 commented 2 years ago

This has been added (with guards to be implemented separately).