> TLA+ doesn't require simulating anything I was referring to way the Python REPL examples/tree diagrams and sections on execution histories were used to expla

> TLA+ doesn't require simulating anything I was referring to way the Python REPL examples/tree diagrams and sections on execution histories were used to explain things in the article, not to TLA+. I was contrasting how the author explained specifications versus how someone like Dijkstra would, not anything about TLA+. I don’t know enough about TLA+ to say anything interesting, but I appreciate your explanations of its approach!