Gaps turn into RUNs, which turn into external choices, which have the semantics of 'the model must be able to accept anything from this set until freed by the presence of some other event'. (Which feels almost like linear temporal logic!). This was ok in the traces model, where there is no notion of tracking what the model can refuse to do, but doesn't work well in tick-tock.
What we actually probably mean to say with 80% of gaps is 'the model can do anything it wants, as long as what it does is constrained to this set, etc etc'. This suggests something closer to timed CHAOS, though the exact interaction with deadlock is unclear.
If we change gaps to have the latter implementation, whether we offer a way to get at the current mandatory reading will become an issue (similar to #52).
Gaps turn into
RUNs, which turn into external choices, which have the semantics of 'the model must be able to accept anything from this set until freed by the presence of some other event'. (Which feels almost like linear temporal logic!). This was ok in the traces model, where there is no notion of tracking what the model can refuse to do, but doesn't work well in tick-tock.What we actually probably mean to say with 80% of gaps is 'the model can do anything it wants, as long as what it does is constrained to this set, etc etc'. This suggests something closer to timed
CHAOS, though the exact interaction with deadlock is unclear.If we change gaps to have the latter implementation, whether we offer a way to get at the current mandatory reading will become an issue (similar to #52).