Skip to content

Milestones

List view

  • Our (more or less arbitrary) goal for this is to have compilation of all specs in our examples directory to be under 1 second. I believe we achieved this!

    Due by September 30, 2023
  • Now that we have integration plumbing to convert the [quint IR](https://github.com/informalsystems/quint/milestone/8) into the [apalache IR](https://github.com/informalsystems/apalache/milestone/74), we want to expose this functionality vial quint's CLI interface. This milestone will be completed once we have a satisfactory implementation of some subcommand(s) that let us modelcheck Apalche specs relatively transparently.

    No due date
    13/14 issues closed
  • This milestone collects the issues that capture the accumulated technical debt

    No due date
    1/1 issues closed
  • The work on simulator that is postponed until after Q1

    No due date
    9/9 issues closed
  • No due date
    1/1 issues closed
  • No due date
    18/18 issues closed
  • No due date
    1/1 issues closed
  • The MVP and first public release of Quint

    Due by January 1, 2023
    13/13 issues closed
  • We want to inform our next iteration of language design with inputs from potential users. I aim to establish two groups of users: - Potential users, interested, willing to spend up to 3 hours in interviews or giving feedback on designs or documentation. - Design partners, who will participate with us on a long-term basis to evolve a language and tooling to meet their needs. From the first group, we will gather user research through interviews and questionnaires. From the second group, we will establish long-term relationships and enlist them into [participatory design](https://en.wikipedia.org/wiki/Participatory_design).

    No due date
    9/9 issues closed
  • To run TNT specs in the model checker, we'll need to convert the TNT AST into the ApalacheIR and serialize it into JSON. For the Apalache side, see https://github.com/informalsystems/apalache/milestone/74

    No due date
    34/34 issues closed
  • Here we group issues that go beyond the MVP

    No due date
    18/18 issues closed
  • We have to update the language from time to time. This work is collected in this milestone.

    No due date
    33/33 issues closed
  • Implement a type system for Quint

    No due date
    20/20 issues closed
  • User stories, features, and bugs related to the interpreter/simulator

    Due by December 31, 2022
    41/41 issues closed
  • No due date
    18/18 issues closed
  • Implement IR manipulation with the visitor pattern according to [ADR 03](https://github.com/informalsystems/tnt/blob/main/doc/adr003-visiting-ir-components.md)

    Due by April 27, 2022
    7/7 issues closed
  • During parsing, `tntc` should check that all names and types are defined, raising meaningful errors otherwise.

    No due date
    14/15 issues closed