quint

quint copied to clipboard

After https://github.com/informalsystems/quint/issues/1102, our flattening is no longer done incrementally. We should find a way to make that incrementally with this new procedure.

bugarela

From https://github.com/informalsystems/quint/pull/1109#discussion_r1298194884 I think the solution here is to change the `importedFrom` field to a list, keep track of the path of imports there, get rid of `namespaces`, and then...

bugarela

Flattening does not support all export use cases

1

Examples of unsupported scenarios: ```bluespec module A { const N: int var x: int action aInit = x' = 0 action aStep = x' = x + N } module...

bugarela

```[tasklist] ### Tasks - [ ] [Instancing a module with instances in it](https://github.com/informalsystems/quint/pull/1118/files#r1304797092) ```

bugarela

```bluespec module A { val a = 1 val b = a } module B { val a = 2 import A.b } ``` ``` quint -r ../local/test.qnt::B Quint REPL...

bugarela

How to run tests in deep modules?

2

My spec is this: https://github.com/cosmos/interchain-security/blob/e09968d94a4e5a84bf144e5f0737e1f529494772/tests/difference/core/quint_model/ccv.qnt#L212 When I run ```quint test ccv.qnt --main CCVDefaultStateMachine``` I would expect the tests in the CCV module to be run. They are not; I guess...

p-offtermatt

I haven't investigated the problem yet, but this hash breaks flattening. Seems like the same type constructor is available both with the `execute::` namespace and without it, but only one...

bugarela

The example on this PR results in a invalid flattened module https://github.com/informalsystems/quint/pull/1363. I tried fixing this in the compiler, which is enough for the simulator. But Apalache can't handle multiple...

bugarela

``` /home/gabriela/projects/quint/local/test.qnt:2:13 - error: [QNT000] Couldn't unify set and list Trying to unify Set[_t3] and List[int] Trying to unify (Set[_t3], (_t3) => _t4) => Set[_t4] and (List[int], (int) => int)...

bugarela

Bad error message on record field typo

2

~Somehow, the typechecker doesn't want `submsg` to have fields other than `reply_on` in this case~ https://github.com/informalsystems/security-tooling-incubator/commit/8d8d230e20c26b4736adcbf0d7daf352c164a6c3 ``` quint run donations.qnt --main=state_machine donations.qnt:280:3 - error: [QNT000] Incompatible tails for rows with...

bugarela