quint
quint copied to clipboard
informalsystems
An executable specification language with delightful tooling based on the temporal logic of actions (TLA)
We have to update the manual with the description of `import ... from`.
Reported by @p-offtermatt ``` quint -r ccv_model.qnt Quint REPL 0.18.0 Type ".exit" to exit, or ".help" for more information >>> (node:39269) [DEP0040] DeprecationWarning: The `punycode` module is deprecated. Please use...
Two different kinds of name errors have been triggered by this exercise in factoring a spec into several modules - ef6a7fb - 65b1883 After investigating, these may be factored out...
Take this spec: ``` module Core { const x: int run CoreTest = 1 == 2 } module Extra { import Core(x = 5).* } ``` When running `quint test...
This case results in `[QNT406] Instantiation error: 'N' is not a constant in 'A'` ```bluespec module A { const N: int val a = N } module B { import...
This follows from discussion in #1062 and discussion with @bugarela and @thpani in person. Currently, type variables must be lower case and type constants must be upper case, but otherwise...
Currently, we have to specify the main module, in order to run tests. This is inconvenient. The command `test` could go over all non-parameterized modules (that is, those that do...
Several of the implemented IR visitors define the same attributes and methods to track nested modules: ```ts private currentModuleName: string = '' private currentTable: DefinitionTable = emptyTable() private moduleStack: string[]...
I just struggled with a problem in a scenario like this: ```bluespec module A { import other.* from "./other" } module B { import other.* from "../wrongPath/other" } ``` Because...
One thing I think could be immensely useful is proper support for . in the VSCode plugin. When I type e.g. ``` currentState. ``` I would like a little box...
Metadata
Owner
Metadata
An executable specification language with delightful tooling based on the temporal logic of actions (TLA)