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

*From*: Leslie Lamport <tlaplus.ll@xxxxxxxxx>*Date*: Sun, 9 Aug 2020 10:15:28 -0700 (PDT)*References*: <5df28190-1201-4668-992f-fbd8fa902216n@googlegroups.com>

For safety and liveness properties S and L, machine
closure means that any prefix of a behavior satisfying S can be extended to a
behavior satisfying S /\ L. There is no
reason that should be true for arbitrary S and L. For example take

S == (x \in {1,
2}) /\ [][x' = x + x]_x

L == <>(x
= 17)

Any property can be written as S /\ L where (S, L) is
machine closed.

One of the virtues of TLA is that there's a simple,
practical way to write only machine-closed specs. If you write

S == Init /\
[][Next]_v

Then S, L is machine closed if L is the conjunction of at
most countably many formulas of the form WF_v(A) or SF_v(A), where A => Next is true for all reachable
states of S.

As for the paper "Safety and liveness from a
methodological point of view", I suggest you read this response to it:

Preserving Liveness: Comments on "Safety and Liveness from a Methodological Point of View"

http://lamport.azurewebsites.net/pubs/abadi-preserving.pdf

As explained in Section 4.3 of

Prophecy Made
Simple

http://lamport.azurewebsites.net/pubs/simple.pdf

adding prophecy variables can and often does produce a
spec that is not machine closed. This is
the case for the prophecy variables in the examples in Section 5.

Leslie

You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/38f9cc41-add6-478e-a4ae-060afb3ec421o%40googlegroups.com.

**Follow-Ups**:**[tlaplus] Re: Safety Liveness Decomposition and Machine Closure***From:*Willy Schultz

**References**:**[tlaplus] Safety Liveness Decomposition and Machine Closure***From:*Willy Schultz

- Prev by Date:
**[tlaplus] Safety Liveness Decomposition and Machine Closure** - Next by Date:
**[tlaplus] How do you write a literal function?** - Previous by thread:
**[tlaplus] Safety Liveness Decomposition and Machine Closure** - Next by thread:
**[tlaplus] Re: Safety Liveness Decomposition and Machine Closure** - Index(es):