here is what "Specifying Systems" says about simulation mode (section 14.3.2):
In simulation mode, TLC repeatedly constructs and checks individual behaviors of a fixed maximum length. [...] In simulation mode, TLC runs until you stop it.
Unlike in model checking mode, simulation continues even if all states have already been encountered before.
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/F448AE77-D705-458F-806D-E52341A9AA64%40gmail.com.