[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] unexpected print output

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.


On 14 May 2015, at 07:56, Y2i <yur...@xxxxxxxxx> wrote:

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,

--algorithm contraints
variable a = 0;
    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.