first, TLC will not check if your specification is machine-closed. (It is machine-closed if you only state fairness conditions for sub-actions of the next-state relation.)
Second, TLC does not take into account fairness conditions when checking invariants. (This may be interpreted as TLC silently assuming that specifications are machine-closed.) Even when you check `Invariance' as a temporal property rather than checking `Invariance' as an invariant, TLC will detect that your property is in fact an invariant and check it as such. However, if you check the temporal property `<>Invariance', TLC will verify it successfully. (You have to add an appropriate state constraint such as `x < 200' in order to ensure that TLC terminates).
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/0ED5668E-0616-4C2D-BBB6-854B756FD036%40gmail.com.