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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Tue, 4 Oct 2016 00:57:36 -0700 (PDT)*Cc*: belout...@xxxxxxxxx*References*: <CAOcQdOWSEhBPYfOojxpcgOJN9UQi6TE1sL8jTtJbF9hFnVC3kg@mail.gmail.com>

I could not understand Question 1. Are you aware that the formula Init /\ [][Next]_vars is true of a behavior if and only if Init is true in the initial state and EVERY SUCCESSIVE PAIR of states in the behavior satisfies Next or is a stuttering step?

Question 2: The formula Init /\ Next, interpreted as a temporal-logic formula, makes an assertion about the first two states of the behavior. It makes no assertion about the subsequent states, so it allows behaviors that do anything else in subsequent states.

Question 3: Actions are ordinary formulas, so there is no need for special rules to reason about them. More precisely, the only special rules needed are the following ones for the prime operator:

- c’ = c if c is a constant

- Prime distributes
over constant operators—e.g., (x+y)’ = x’ + y’

Leslie

**References**:**Newcomer Questions***From:*kacem belout

- Prev by Date:
**Newcomer Questions** - Next by Date:
**Idiomatically verifying state does not change** - Previous by thread:
**Newcomer Questions** - Next by thread:
**Idiomatically verifying state does not change** - Index(es):