quint

quint copied to clipboard

@p-offtermatt pointed out in the co-design meeting today that the simulator lacks the equivalent of apalache's `cinit`. This makes it a bit cumbersome to script instantiation, since it requires writing...

shonfeder

Uninformative error message when using .fail() in tests

2

Take this module: ``` module test { var x: int action init = x' = 1 action inc = x' = x + 1 action failAction = all { false,...

p-offtermatt

Deprecate and remove the ambiguous form of type annotation

4

If I have ``` def condition(f: int => bool): bool = { state.filter(f).size() > 0 } ``` And decide I want to remove the type annotation on `f` and let...

shonfeder

redefining a function gives a "syntax error"

3

In the repl, ``` >>> def farenheit(celsius) = celsius * 9 / 5 + 32 >>> def farenheit(celsius) = celsius * 9 / 5 + 32 syntax error: :4:1 -...

plafer

refactoring the ics23 spec

2

This is a refactoring of the ICS23 spec, which took more effort than I expected (about 8hrs in total): - [x] the spec is now split in multiple files, -...

konnov

Support for "flag-based" invariants

2

@p-offtermatt has shared the view that there is a certain class of invariants which -- while formalizable as trace invariants or temporal properties -- are easiest to communicate to implementation...

shonfeder

### Discussed in https://github.com/informalsystems/quint/discussions/1159 Originally posted by **konnov** September 12, 2023 Champions: @andrey-kuprianov and @angbrav We had a very [long discussion](https://informalsystems.slack.com/archives/C043C01N3SA/p1682666953784399) about native support for rationals in the Quint simulator...

shonfeder

Document the "software specification and development life cycle"

6

We should sketch out our hypothesis on the "specification life cycle", including notes on which parts we've been able to validate. The cycle might go something like: 1. Exploratory modeling...

shonfeder

Closes #1360 This is a quick workaround to meet the need for this functionality, which has been voiced in the last few days. ``` quint run --out-itf=out-itf-example.itf.json --n-traces=5 ../examples/solidity/Coin/coin.qnt ```...

shonfeder

Add the option to specify a number of (counter)examples to generate

3

### Discussed in https://github.com/informalsystems/quint/discussions/1138 Originally posted by **ivan-gavran** September 1, 2023 I would like to start a discussion on a feature that would enable specifying a number of (different) counterexamples...

shonfeder