|TLC is not checking these fairness conditions, since they are part of the specification and therefore assumed. Also, as long as you are only checking invariants it doesn't matter if you add the fairness assumptions to the spec or not as they do not influence whether a state is reachable or not.|
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/82FB71A1-D76D-4E05-A500-5956026ADEC7%40gmail.com.