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