quint

quint copied to clipboard

Apalache rewritter error on poly types

6

After solving #1393, I'm hitting another problem with the `option.qnt` (full) example: ``` error: : rewriter error: Unexpected type a when generating a default value ``` https://github.com/informalsystems/apalache/blob/dd1fef9323863b49e623337fe4cba167c63f2c8d/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/DefaultValueFactory.scala#L113

bugarela

Two examples. First: https://github.com/informalsystems/quint/issues/1389 The "Error: 1 CANCELLED: Call cancelled" is not helpful at all. Even if we are not able to identify the problem on quint side, we should...

bugarela

Quint allows let-bindings where operators are expected, breaking integration with Apalache

2

Apalache is version 0.44.7 Quint version 0.18.3 Spec: https://github.com/cosmos/interchain-security/blob/8184c49ab6f6edb3e53cd7b6a70c127d5b65eb24/tests/mbt/model/ccv_model.qnt#L178 ``` % quint verify ccv_model.qnt --verbosity 5 error: internal error: while parsing in Apalache: 'Input was not a valid representation of...

p-offtermatt

The language spec describes "anonymous" instances as follows https://github.com/informalsystems/quint/blob/393ec51329429ce8d99016921fea777b53ea357d/doc/lang.md#L2025-L2058 This makes it clear that the current intended semantics of instances of the form ``` import Foo(...).* ``` is that the...

shonfeder

Trailing comma in const initialization

2

Hi, take this example: ``` module a { const A: int const B: int } module b { import a( A = 5, B = 5 ).* } ``` Here,...

p-offtermatt

Minimizing counterexample traces

1

I think one thing that could be very useful to have in the simulator would be an option to have it attempt to minimize invariant violations. When I get counterexample...

p-offtermatt

My spec is here: https://github.com/cosmos/interchain-security/blob/c69977414782ed604f53cf555e342bb177163123/tests/mbt/model/ccv_model.qnt#L523 When I run ``` quint test ccv_model.qnt --verbosity=3 ``` I get this error: ``` TypeError: Cannot read properties of undefined (reading 'subframes') at TraceRecorderImpl.onNextState (/opt/homebrew/lib/node_modules/@informalsystems/quint/dist/src/runtime/trace.js:147:32)...

p-offtermatt

It would be very useful to have an option to automatically convert a counterexample trace into a test inside your module. A suggestion for the workflow could be like this:...

p-offtermatt

Related to #446 @p-offtermatt has recently revived discussion of how useful it would be to be able to save the state of a simulation, and then load up a simulation...

shonfeder

Simulator should produce a minimal violated invariant

1

When the simulator finds a violation to `and { A_1, ..., A_n }`, it should report one of `A_i` that was violated.

konnov