Currently we only support waits of the form after n units, which require that the model wait exactlyn time units, possibly accepting things permitted by a gap in the interim. The sequence then moves to the next action. (Perhaps confusingly, this may also then take several time units, and so the model may in fact wait at leastn units before doing something observable.)
We might also want to capture the possibility that the model waits some amount of time that is at leastn units, but up tok: after between n and k units. This would be a nondeterministic wait, with CSP semantics that looks something like
-- nondeterministic wait when n=0
nzwait(k) = if k == 0 then Skip else (Skip |~| tock -> nwait(k-1)) end
-- general nondeterministic wait
nwait(n, k) = wait(n); nzwait(k-n)
This mainly captures a corresponding RoboChart feature.
Currently we only support waits of the form
after n units, which require that the model wait exactlyntime units, possibly accepting things permitted by a gap in the interim. The sequence then moves to the next action. (Perhaps confusingly, this may also then take several time units, and so the model may in fact wait at leastnunits before doing something observable.)We might also want to capture the possibility that the model waits some amount of time that is at least
nunits, but up tok:after between n and k units. This would be a nondeterministic wait, with CSP semantics that looks something likeThis mainly captures a corresponding RoboChart feature.