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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Mon, 21 Sep 2015 03:35:10 -0700 (PDT)*References*: <f47ab3b7-9c7d-4a7b-9ec1-fda4020d18d5@googlegroups.com>

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.

Cheers,

Leslie

**References**:**meaning of a tla predicate***From:*Amira Methni

- Prev by Date:
**Re: What should I do next in the Hyperbook?** - Next by Date:
**Re: What should I do next in the Hyperbook?** - Previous by thread:
**meaning of a tla predicate** - Next by thread:
**Error when adding an Invariant** - Index(es):