quint

quint copied to clipboard

As requested in https://github.com/informalsystems/quint/pull/855#discussion_r1179124142

konnov

CLI should produce different error codes

2

Currently, if a test in [cli-tests.md](https://github.com/informalsystems/quint/blob/main/quint/cli-tests.md) returns a non-zero exit code, we do not know, whether it was the expected behavior or not. For instance, if we expect the simulator...

konnov

To gather simple metrics such as the plugin usage. This can be easily done via native VSCode extensions: https://www.npmjs.com/package/@vscode/extension-telemetry We would have to figure out and document which metrics we...

konnov

This is a more useful coverage estimate asked for in #1067. We could store the hashes of the states visited by the simulator and print out the number of visited...

konnov

Improve error messages by antlr

3

The default messages by antlr are hardly readable: ``` examples/ReadersWriters/ReadersWriters.tnt:22:65 - error no viable alternative at input 'NumActorsdefToSet(s)=s.keys().map(i->s[i])defread(s)=s[1]=="read"defwrite(s)=s[1]=="write"valWaitingToRead=ToSet(waitingselectread)map(p->p._2)' examples/ReadersWriters/ReadersWriters.tnt:22:57 - error extraneous input '->' expecting {'module', '{', '}', 'const', 'var',...

konnov

`import... from...` in REPL does not work

3

It looks like we have dismantled support for imports from files in REPL, when we made it incremental. Consider a simple spec: ```bluespec module foo { pure def x =...

konnov

Expose simulator state in the REPL

1

@plafer's excellent feedback in https://github.com/informalsystems/tnt/discussions/435#discussioncomment-4422672 have highlighted some of the pitfalls new comers might hit as they learn to work with actions and state variables in the REPL. One thing...

shonfeder

Require () on actions without parameters?

6

We have the special syntax for the parametereless definitions (`val` and `pure val`). We do not have any special syntax for actions that have zero parameters. I have caught myself...

konnov

This is the `CHOOSE x \in S: TRUE` of TLA+. Most likely, it requires the canonical form, similar to what we do in the conversion `toQuintEx`. This operator is not...

konnov

It should be relatively simple, but we have to find this out.

konnov