quint
quint copied to clipboard
informalsystems
An executable specification language with delightful tooling based on the temporal logic of actions (TLA)
One of the things I am missing dearly when writing Quint is support to show function signatures for functions I am typing right now. Here is what the thing I...
We found some improvements to be made around what is returned by the simulator and how it is processed in `cliCommands`: https://github.com/informalsystems/quint/pull/1340
Our tuple unpacking in lambdas only works for the top level. ```bluespec module A { // works val foo = Set((1, true), ((2, false)).map((i, b) => if (b) i else...
`iadd` is the builtin for addition: ``` >>> iadd(1,1) 2 ``` But if we try to supply it to a 2nd order operator, name resolution fails: ``` >>> def f(g)...
My current workflow of writing and updating tests is as follows: I write runs/tests in VSCode. They are quite long and complex. I use a prototype of a domain-specific language,...
In the `run` mode, we make some restrictions such as `reps` requiring a pure argument for number of repetitions, while we could be more permissive since these are just tests...
quint test run produces itf traces without the last state ``` module myTest { var x: int action init = x' = 0 run myTest = init.then(x' = 1).then(x' =...
I have been talking to our first users of Quint, who are writing real specs. Here is the summary of the recent feedback: @plafer gave us feedback some time ago...
@andrey-kuprianov had a great suggestion for extending `.clear` with the following logic: > ...it would be nice to have > .clear [def] > i.e. the possibility to provide an optional...
Given ``` module A { var x: int } module B { var x: int } module C { import A import B action step = all { A::x' =...
Metadata
Owner
Metadata
An executable specification language with delightful tooling based on the temporal logic of actions (TLA)