List view
In order to ensure idiomatic quint specs can be verified in Apalache effectively, we need to be able to rewrite idiomatic quintified-TLA into correct and performant TLA (as the ApalacheIR). However, the current state of our internal rewriting libraries is too burdened by tech debt to make this feasible. Thankfully, a design that will enable us to program these rewrites with greater velocity and correctness has been developed by @kukovec in https://github.com/informalsystems/apalache/pull/2447 . This will have many side benefits to the maintainability and extensibility of Apalache, but the critical need driving this work is the support for idiomatic quint.
Overdue by 1 year(s)•Due by December 31, 2023•9/14 issues closed- No due date•62/63 issues closed
Evaluating ITF traces
No due date•12/16 issues closedWork related to optimizing the core of the model checker
No due date•26/36 issues closedSupport for symbolic simulation
No due date•3/5 issues closedThis milestone captures the worked that was planned in [ADR014](https://github.com/informalsystems/apalache/blob/unstable/docs/src/adr/014adr-precise-records.md).
No due date•27/31 issues closedOur integration test harness is due for another round of refinement. The current approach was an iteration on top of a single bash script. The tests in that script were ported into a single markdown file for use with `mdx`. This provided improved clarity, extensibility, and maintainability, but the single file is growing unwieldy, and the long running times of the integration suite are becoming an increasingly narrow bottleneck on our CI. Some issues have opened with ways on improving the integration tests, and this milestone is to collect those to plan a general revamp.
No due date•2/6 issues closedThis milestone groups issues that are reported by the users. We triage them and collect the issues to be fixed soon in a separate milestone. This is needed to keep track of these issues and observe our progress on fixing them. It also includes maintenance work that is caused by the discovered issues.
No due date•62/63 issues closedScope the work related to safety and liveness properties
No due date•8/17 issues closedWork related to features and refactoring of `a..b`, `Int`, `Nat`, `CHOOSE x \in S: P`, `SUBSET S`, and `[S -> T]`. There is a body of work, where we can improve or fix the encoding.
No due date•8/21 issues closedAlthough we have a pretty good coverage of basic operators with unit tests, we should introduce comprehensive integration tests. The goal is to cover the corner cases and to have as many cases covered from end to end.
No due date•2/6 issues closed- No due date•1/2 issues closed
Implement all the necessary components to support the Simple fragment (mostly collection-free, FO logic with functions).
No due date•6/9 issues closedError messages are one of the most critical forms of user feedback, and recent success of clear, insightful messages in languages like Rust and Elm help show the usability improvements that come from well designed, and consistently implemented, error messaging.
No due date•2/7 issues closed