Re: [tlaplus] Question about the order of evaluation.

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

On 28.02.20 15:52, HP wrote:
> 
> VARIABLESx
> 
> 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
> 
> "}"

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

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/895476f6-781b-49c6-8f79-19f9c2a6714e%40lemmster.de.