Ideas for interaction

[shonfeder]

Thought I'd open a thread to share and discuss ideas from a broad UI/UX angle, but that are too roughed in to be issues or discussion in their own right.

[shonfeder]

Interactive configuration of checking parameters, and execution of checks.

I imagine a TUI interface akin to magit or ProofGeneral. Some functionality would includeL

• On click/selection of operator names, set them as invariants, as init, or as next. This could be indicated by an icon, overlay, or font face change to the operators.
• Interact with step-wise simulation to show the current value (or perhaps just constraints) of a state variable on hover.
• Enable live reloading and checking of spec, giving feedback inline, akin to type checking, of whether set invariants/next are holding given the current spec or not.

[konnov]

I like this idea a lot. Do we have to make a prototype to discuss that? As far as I know, UX can be designed without having an MVP. Do we like to do that in advance @tesnimab?

[shonfeder]

The new ability to set all application configuration via a single config file should help with lots of parts of this this once we're connected with Apalache: reading and updating the config can just be a matter of reading/writing to a json file that holds the apalache config, and if we run the checker in "watch mode", it can just rerun whenever the source files change (including the config file).

[bugarela]

For clarification: are we imagining this as part of the VSCode plugin or as a TUI?
I personally love TUIs but I think the VSCode plugin is much more accessible atm. However, I'd like us to keep in mind the possibility of other frontends to find some nice abstractions in the implementation as we are doing with LSP.

[shonfeder]

I meant “text user interface” in a vague and inaccurate sense, I guess, and expect that the implementation would be in or at least aimed to support VSCode.

[shonfeder]

Oh, but also this discussion item was meant to be a place where you ideas of all sorts can be shared discussed :)

[tesnimab]

I am happy that you are opening this discussion.
For Atomkraft, we have to ease the writing of test assertions by users given a TLA+ spec.
Here are more details about the feature in this issue: https://github.com/informalsystems/mbt/issues/226
In terms of UI/UX it's a priority for us.

[shonfeder]

One quick note on the intent of this discussion: it was meant as a place to record and have open-ended discussion on UI ideas, as they arise. Which might later be broken out into concrete work items and prioritized etc.

If the https://github.com/informalsystems/mbt/issues/226 reflects planned work that we should prioritize, and that needs support from Quint, we should be sure to record this in an issue in the Quint repository! In that case, I think we'll probably need some clarification on what the expected ask is from Quint development.

If, however, we're just exploring/kicking around ideas on this: iiuc, is possible that the Quint support suggested there, w/r/t auto-complete etc. could come just from extending the base module specifying the SDK and adding some additional invariants? Or is something else needed?

[andrey-kuprianov]

On the MBT side, we've started to experiment with TUI ideas before the Vienna meeting. Some info in this direction can be found here:

• Modelator API & Shell
• Modelator & Atomkraft Shell diagram

We've had the prototype version of Modelator Shell working for the Vienna meeting, but because later we have moved fast forward with Atomkraft, the Shell idea has been put on the shelf for now; the current version of modelator doesn't support interactive shell. You can still play with the previous prototype by checking out the repo at approximately this commit.

I've also had many ideas wrt. using overlays in TUI to show the status of parsing/typechecking/checking the model, a la Pytest-TUI, but have not found time to implement them yet... To summarize, it seems that quite a lot of what you have in mind wrt. TUI we were also thinking about at some point. So we should probably do a joint meeting and discuss all that.

[konnov]

Just revisiting this idea. In principle, I like the interactivity of Coq and Isabelle. However, having observed protocol designers and auditors a bit, they tend to use quint repl more, at least for now. Where some form of interactivity would definitely help is replaying of runs. Currently, one has to do it by hand and print the states. While this is possible, it is not a very productive activity.

[jbibla]

Where some form of interactivity would definitely help is replaying of runs. Currently, one has to do it by hand and print the states.

can you elaborate on this, Igor?

[konnov]

For instance, see the trace produced in this example. Currently, the users have to copy&paste states one by one to REPL. It's not hard, but we could introduce the trace in REPL itself and let the users replay it interactively. Also, see this PR: https://github.com/informalsystems/quint/pull/866/files