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

# PrintT behaviour

```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? ```