The current temporal operators are always, eventually, and next. Some properties need the until operator, like if you want to say that a spinner is shown until a success or error message is shown.
Note: p.until(q) does not imply always(not(p.and(q))), i.e. there's no "mutual exclusion" going in until. If you'd like to say the spinner is shown until, but not together with the success or error message, you'd have to combine the two formulas, or do p.until(q.and(not(p))).
Also note: always and eventually can be defined in terms of until, but we probably don't want to do that in order to have clear error messages and not lose information.
The current temporal operators are
always,eventually, andnext. Some properties need theuntiloperator, like if you want to say that a spinner is shown until a success or error message is shown.Note:
p.until(q)does not implyalways(not(p.and(q))), i.e. there's no "mutual exclusion" going inuntil. If you'd like to say the spinner is shown until, but not together with the success or error message, you'd have to combine the two formulas, or dop.until(q.and(not(p))).Also note:
alwaysandeventuallycan be defined in terms ofuntil, but we probably don't want to do that in order to have clear error messages and not lose information.