I believe (but I'm not 100% sure) that with the assertion, TLC prints its output once during the generation of the state space and then again when reconstructing the counter-example trace that leads to the assertion violation.
Could someone please explain why the algorithm below prints <<Hello>> twice (unexpected), but when I comment out the assert at the end, it prints <<Hello>> only once (as expected)?
EXTENDS Naturals, TLC
variable a = 0;
L1: while a < 100 do
a := a + 1;
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+u...@xxxxxxxxxxxxxxxx
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx
Visit this group at http://groups.google.com/group/tlaplus
For more options, visit https://groups.google.com/d/optout