Hi,
In module RealTime, the definition of TNext (as given on page 123 of Specifying Systems book) is as follows:
TNext(t) == t' = IF <<A>>_v \/ \lnot (Enabled<<A>>_v)' THEN 0 ELSE ...
As described in the book, the predicate \lnot (Enabled<<A>>_v)' denotes a step that disables <<A>>_v. I do not understand the meaning of this predicate. Could you give me an example to more understand what this predicate does ?
Thank you,
Amira