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

*From*: Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>*Date*: Fri, 28 Feb 2020 16:28:27 -0800*References*: <5d834c71-b474-4820-a08c-a0fda7350770@googlegroups.com>

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.

**References**:

- Prev by Date:
**[tlaplus] Question about the order of evaluation.** - Next by Date:
**Re: [tlaplus] Checking Liveness on Windows** - Previous by thread:
**[tlaplus] Question about the order of evaluation.** - Next by thread:
**[tlaplus] Model Checking "Termination" Property** - Index(es):