[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

meaning of a tla predicate


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,