PrintT behaviour

[Werner Grift <sky.c...@xxxxxxxxx>]

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?