https://homes.cs.washington.edu/~ztatlock/pubs/verdi-wilcox-...
which gives this example for a distributed lock:
mutex(τ ) := τ = τ1 ++ (n1, Grant) ++ τ2 ++ (n2, Grant) ++ τ3 → (n1, Unlock) ∈ τ2
What this safety requirement means is that if the lock is granted in some pending message to host n2 (say delivered or in queue to be delivered) then it must have been proceeded by an unlock message and not on the same host getting the grant --- in fact on the last node who was granted the lock. Here n1, n2 designate hostIds.
What I like about this approach, is that Verdi seems to make it quite easy to model and specify in terms of nodes, processes on nodes, and messages between nodes whether on a reliable or non-reliable network. And safety conditions seem to naturally flow, in part, from how messages are ordered when sent. Of course, in an unreliable network which Verdi can model too, they may come out of order requiring more work to de-dup and/or ensure exactly-once-delivery.