That’s the great advantage of interacting with a system instead of just reasoning about it. We had to think about it for a second, and it felt like a discovery, something we didn’t know we didn’t know. (The REPL preloads some standard modules like Bags and Sequences.) (tla+) SetToBag() is a tuple. Let’s say you wanted to understand Bags better. Download a recent TLC build (the latest release is December 2020 and doesn’t have it) and invoke the REPL thus: $ java -cp tla2tools.jar tlc2.REPL Samy and I think it’s especially helpful for beginners, but it’ll be occasionally valuable for any TLA+ user. ![]() Our former colleague Will Schultz contributed it last year (before he left MongoDB for grad school). If you want to experiment and see what some constant TLA+ expression evaluates to, the new REPL is useful. We think that “export to HTML” would be a nice feature for the Toolbox. And unlike the Toolbox or VS Code GUIs, you can publish this on the web and share it with colleagues to communicate about spec behaviors. It’s obviously easier to read than the plain-text output from TLC. ![]() This is a nice HTML version of a TLA+ trace. Samy’s and my colleague at MongoDB, Siyuan Zhou, made an alternative called tla-trace-formatter: out file, or a GUI trace in the TLA+ Toolbox or VS Code. What precisely is the mismatch between your hypothesis and reality? How can the tools help you find it? Specifying Systems § 14.5.2 “Debugging a Specification” is a particularly good section about this, so we won’t repeat it, but we’ll try to add a bit.Įrror traces are the main technique for answering this question. You ask this question when you have a wrong hypothesis about your spec: you either didn’t write the spec you thought you did, or the spec doesn’t behave as you think. The tools are only prototypes or don’t exist at all. TLC and TLAPS are production-quality, and there are new tools like Apalache.Īs we go down the list there are vaguer questions like “Is the spec generally behaving as intended?” or “How do I use TLA+ to communicate behaviors to other people?” These are decreasingly well-supported. It’s the main purpose of model-checking and proofs, and it’s where most of the research seems to go. The first question, “Does my spec imply my invariants / properties”, is the most thoroughly supported.
0 Comments
Leave a Reply. |
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |