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

*From*: Werner Grift <sky.c...@xxxxxxxxx>*Date*: Thu, 15 Sep 2016 07:37:19 -0700 (PDT)

Why does PrintT always print when TLC evaluates or permutates it, instead of only on the permutation that resulted in a valid next state. PrintT is currently basically useless for debugging purpose and just spams printouts that don't make any sense at all. Does anyone find this or is it just me? For example: N1 == /\ a' = a + 1 /\ PrintT("N1") /\ UNCHANGED b N2 == /\ b' = b + 1 /\ PrintT("N2") /\ UNCHANGED a N == /\ \/ N1 \/ N2 /\ t' = t + 1 /\ t' < 3 /\ PrintT([t|->t', a|->a, b|->b]) ...yields the output "N1" [t |-> 1, a |-> 0, b |-> 0] "N2" [t |-> 1, a |-> 0, b |-> 0] "N1" [t |-> 2, a |-> 1, b |-> 0] "N2" [t |-> 2, a |-> 1, b |-> 0] "N1" [t |-> 2, a |-> 0, b |-> 1] "N2" [t |-> 2, a |-> 0, b |-> 1] "N1" "N2" "N1" "N1" "N2" "N1" "N2" [t |-> 1, a |-> 0, b |-> 0] "N2" [t |-> 1, a |-> 0, b |-> 0] "N1" [t |-> 2, a |-> 1, b |-> 0] "N2" [t |-> 2, a |-> 1, b |-> 0] How can PrintT be useful if it does this when the state only changed 3 times? What don't I get?

- Prev by Date:
**Re: RandomElement fails with TLC bug** - Next by Date:
**Re: RandomElement fails with TLC bug** - Previous by thread:
**Re: [tlaplus] Re: RandomElement fails with TLC bug** - Next by thread:
**[Dr. TLA+ Series] Global Snapshot - Rustan Leino** - Index(es):