search

UoY-RoboStar / robocert-textual

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

Gaps can timestop but nothing else can #65

Closed MattWindsor91 closed 2 years ago

MattWindsor91 commented 3 years ago

An interesting (and perhaps disturbing) consequence of using TCHAOS for gaps (#63) is that anything in {||} until X is not equivalent to X in the tick-tock model, because the former can timestop (ref.tock).

I'm filing an issue here because, if gaps should timestop, there should probably be other ways to introduce timestop into specifications; if they shouldn't, well, they shouldn't.

MattWindsor91 commented 2 years ago

Closing because the semantics of timing in robocert is now fairly stable (if a little rough around the edges). I'll create more specific issues in future if things go wrong.