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?