quint

quint copied to clipboard

Simulator crashes with invalid `init` action

4

If the init action refers to vars, the simulator breaks. Instead, we should properly report/explain the error. MWE: ```bluespec module test { var x: int action init = x' =...

bugarela

It complains about a record. We should figure out that there is an operator with that name and complain about missing parenthesis instead. ``` quint typecheck test.qnt test.qnt:2:28 - error:...

bugarela

Add option to verify inductive invariants

3

I'm exploring inductive invariants in Quint with Apalache, and it seems to be achieavable with some tweaks to the interface and mode verification for Init. See this example (from the...

bugarela

For now, the REPL only supports parsing multiline things when there is some sort of open braces that still need to be closed when a newline appears. We should take...

bugarela

Bad error message for missing parenthesis in the `if` condition

2

If the `if` statement is inside an operator call (or probably anything), the parser loses track of the missing parenthesis error, and the reported error is almost meaningless: ```bluespec module...

bugarela

Integration with TLC

5

I've been thinking about and trying to use Quint with TLC for a while now, so here's an issue to track these thoughts/experiments. First of all, we need to translate...

bugarela

Improve our tests that use fixtures

1

Ideas: 1. Format test fixture json file as suggested by @p-offtermatt in https://github.com/informalsystems/quint/pull/1421#pullrequestreview-1985582480, this would make the diffs much easier to read (currently impossible to read) 2. Use a proper...

bugarela

Formatter for Quint source code

3

It would be nice to have a `quint format` command that would format any source file given to it, much like `rustfmt` for Rust or `prettier` for JavaScript/TypesScript. As far...

romac

Internal error while flattening [QNT404] Name 'Listed' not found

1

Trying to verify the accompanying model results in error ``` Error: Internal error while flattening [QNT404] Name 'Listed' not found at resolveNamesOrThrow (/home/user/.npm-packages/lib/node_modules/@informalsystems/quint/dist/src/flattening/fullFlattener.js:91:15) at flattenModules (/home/user/.npm-packages/lib/node_modules/@informalsystems/quint/dist/src/flattening/fullFlattener.js:62:35) at compile (/home/user/.npm-packages/lib/node_modules/@informalsystems/quint/dist/src/cliCommands.js:493:104) at...

eras

We currently download apalache and spawn a bash script to run the server. On windows, we can't simply run a bash script. I tried adding a `.bat` file to the...

bugarela