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

[tlaplus] Re: Safety Liveness Decomposition and Machine Closure

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"


As explained in Section 4.3 of

   Prophecy Made Simple


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.


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.