Disabling deadlock checking is standard practice when verifying algorithms whose executions are expected to terminate. Checking for deadlocks is mainly useful for algorithms that are expected to run forever, which is the case for many distributed algorithms.
Also, I suggested adding the fairness condition for verifying the liveness properties that you stated in the original version, in particular for verifying termination, i.e. the property <> done. It won't have an effect on deadlock checking: note that absence of deadlock is a safety property.
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/F1C552A0-0B28-4022-A3BE-EF14664B554F%40gmail.com.