Question about the order of evaluation.

[HP]

VARIABLES x

Init == /\ x = 1

Next == /\ PrintT("{") /\ PrintT(x) /\ x' = 2 /\ PrintT(x') /\ PrintT("}")

Below is the output for BFS. It makes sense to me. 

"{"

1

2

"}"

"{"

2

2

"}"

But why the output is different with DFS? Why have "{12}" is printed twice? Anyone can explain to me? Thanks.

"{"

1

2

"}"

"{"

1

2

"}"

"{"

2

2

"}"

[Markus Kuppe]

On 28.02.20 15:52, HP wrote:
>
> VARIABLESx

Hi,

it is printed twice because of IDDFS [1]. This thread [2] has some more
info about Print. Note though, that if you care about the inner
workings of TLC, it is probably more effective to run TLC in a debugger.
It won't teach you much about TLA+ though.

M.

[1] https://en.wikipedia.org/wiki/Iterative_deepening_depth-first_search
[2] http://discuss.tlapl.us/msg00707.html