On Friday, November 21, 2014 7:22:46 PM UTC-5, Leslie Lamport wrote:
I don't know what kind of REPL for TLA+ you (and Chris) would like.
Please describe explicit scenarios that you would like to have
supported. Be as fanciful as you like. The only constraint is that
the E(valuate) has to be performed by the TLC model checker, so forget
about anything that involves instantly reporting all errors in a spec
with 10^27 reachable states.
What I expect from the REPL is effortless and always-on evaluation of expressions. This can be in the form of a console-style interface that's typical of the REPL's out there, but I'm more fond of the notebook-style interfaces that Mathematica or more dynamic variants of this UI style, such as Light Table (http://lighttable.com), exemplify.
For example, if I have three expressions on my notebook using various definitions from the specification this notebook is based on, I would expect their results to be updated without any explicit action by me when I change the specification. The notebook itself would have an editor-like UI, with expressions and the results of the their evaluation presented inline. I would want to use the REPL notebook in a two-column layout with the specification editor within the toolbox.
It should be possible to define and redefine operators, variables, constants and model values within the notebook. If a symbol is redefined, the new definition's effects should be immediately visible on all usages of that symbol transitively.
I expect to have three major ways to launch the REPL notebook:
- Based on a specification: This is perhaps the simplest way; right-clicking on a specification (or using a menu item) should open a REPL notebook where all definitions and declarations made in the specification are in scope. This is where I expect to spend most of my time, using it as a sandbox and building up parts of a specification incrementally. This alternative also fits the "logic calculator" use case, assuming the specification can be optional, with an empty one (suitably importing a default set of useful standard modules) substituted at runtime in a notebook that's not based on an existing specification.
- Based on a state in the error trace: Right-clicking on a state in the error trace should provide an UI action to create a REPL notebook with the initial state set to and all definitions/declarations in scope at that point. I should be able to write expressions in the notebook and see their result as they would be evaluated in those exact conditions. It would be nice if this included ENABLED expressions too. I suspect more interesting ways to push this style of interaction are possible if one were to consider interactively guiding the model checker along a particular behavior, but this encroaches on debugger territory (which is interesting for a runtime such as TLC).
- Based on a model of the spec: Right clicking on a model should give me the ability to create a REPL notebook based on the initial state and all other overrides/settings/declarations in that model.
In all of these alternatives, it should be possible to create a model out of a notebook, with all the redefinitions, constants and other details outside of the specification the notebook is based on being reproduced in the new model. Among making it simple to move parts between notebooks and models, this allows a nice workflow during debugging; I could start a notebook from a particular error state, make changes, create a new model out of the notebook that reproduced my changes (including the variable state as the new initial state), and see their effect. Of course, I would only observe the effect on the small subset of the state space as pruned by the given initial state, which I think is fine in order to check the effects of a change on a specific set of behaviors. This sort of incremental checking is too cumbersome to use today.
There are of course a lot more details to figure out about the user interaction, but I think what I describe above would be a significant factor to ease the learning curve of TLA; my main motivation is to shorten the feedback loop between making a change and seeing its effects, which makes the interaction between my thinking and the reality as shown by TLA/TLC more frictionless, and that is a boost to how fast I can learn.