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

Re: meaning of a tla predicate

Hi Amira,

You wrote:

   \lnot (Enabled<<A>>_v)' denotes a step that disables  <<A>>_v

A step is a pair of states.  The formula \lnot (Enabled<<A>>_v)' is an
action formula, meaning it is a predicate on steps.  This predicate is
true for a pair of states <<s, t>> iff <<A>>_v is disabled in state t.

"Denotes" means gives a name to or to designate.  The only way to
denote a step is to say what its two states are, which means to say
what values each of them assign to variables.  By "state" we usually
mean the state of a system, which assigns a values to each of the
system's variables.  One can denote a step by an action formula like
the following, which assumes that the system's variables are x, y,
and z:

   /\ x = 7
   /\ y = {"a"}
   /\ z = <<1, 2>>
   /\ x' = 42
   /\ y' = {}
   /\ z' = <<1, 2, 3>>

\lnot (Enabled<<A>>_v)' is not such a formula, and it does not denote
a step. 

If this isn't enough to help you understand the definition of TNext(t),
you may have jumped into Chapter 9 without a proper understanding of
the first few chapters of the book.