Hello Yuri,
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.
Best, Stephan
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)? Thank you, Yuri
EXTENDS Naturals, TLC (* --algorithm contraints variable a = 0; begin L1: while a < 100 do a := a + 1; end while; print <<"Hello">>; assert FALSE; end algorithm *)
--
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.
|