UoY-RoboStar / robocert-textual

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

Partiality is lost in the tick-tock model #66

Closed MattWindsor91 closed 2 years ago

MattWindsor91 commented 3 years ago

In the traces model, sequences are partial by default (by the sheer nature of traces); in the tick-tock model, we lose this because the final action in pretty much every partial sequence is Skip and this has the effect of requiring the sequence to terminate.

Ideally, we need some way (either implicit or explicit) of marking the end of a sequence as TCHAOS. anything until end was supposed to be this I think, but end is presently itself also Skip. Hmm.