search

UoY-RoboStar / robocert-textual

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

Resolve semantics oddity with gaps in tick-tock model #31

Closed MattWindsor91 closed 3 years ago

MattWindsor91 commented 3 years ago

At time of writing, the semantics for gapped actions is

anything in X until ->op Y()
=
RUN(union({tock}, diff(X, {Y.out})) /\ Y.out -> SKIP

which is ok in the traces model, but perhaps has an overly strict interpretation in tick-tock: it requires that the module under verification can't refuse any of the events in X. We may need to consider working on a more permissive understanding of gaps that allows refusals (eg using |~|), but need to be wary of preserving time synchronisation across whatever replaces /\.

MattWindsor91 commented 3 years ago

It looks like at some point I put in #63 as a duplicate of this. That's closed now, so I'm closing this.