This also probably explains why so few people manage to pick up symbolic tools (the stability issues aside). It is much harder to build a mental model there, and there are not so many conceptual models around.
Hah, this is true. I can tell you how TLC works very quickly - breadth-first search to check safety properties, graph cycle detection (meaning infinite loops) for liveness counterexamples. I don’t yet have much intuition about symbolic model checking, despite some experience with Z3. I wonder if it has the same issue with invisible performance cliffs where minor restatements of the problem lead to huge differences in execution time.
Instead, we were discussing the syntax of TLA+. There was no single engineer who said that they liked this part. Interestingly, these people did not want to write a specification, they just wanted to read it.
Hah, this is true. I can tell you how TLC works very quickly - breadth-first search to check safety properties, graph cycle detection (meaning infinite loops) for liveness counterexamples. I don’t yet have much intuition about symbolic model checking, despite some experience with Z3. I wonder if it has the same issue with invisible performance cliffs where minor restatements of the problem lead to huge differences in execution time.
Tangentially, thank you for your lovely blog etc. I’ve learned quite a lot from it.
Glad you find it useful!
Why not give them the LaTeX-typeset output then?