quint: Tool for the Quint specification language

WARNING: This is a preliminary manual in the style of Working Backwards (opens in a new tab). Some commands are not implemented yet.

quint is a command line interface tool for working with the Quint specification language. It is the primary access point for testing and integration with other tools.

The main commands of quint are as follows:

• repl starts the REPL (Read-Eval-Print loop) for Quint
• compile parses, typechecks, and processes a quint specification into the --target format, writing the results to stdout
• parse parses a Quint specification and resolves names
• typecheck infers types in a Quint specification
• run executes a Quint specification via random simulation similar to stateful property-based testing
• test runs unit tests against a Quint specification
• verify verifies a Quint specification with Apalache
• docs produces documentation
• lint checks a Quint specification for known deficiencies
• indent indents a Quint specification

In the following, we give details about the above commands.

Installation

npm i @informalsystems/quint -g

Command repl

This is the default operation if no other subcommand is given:

$ quint

You can also invoke it directly with quint repl:

$ quint repl --help
quint repl
 
run an interactive Read-Evaluate-Print-Loop
 
Options:
      --help     Show help                                             [boolean]
      --version  Show version number                                   [boolean]
  -r, --require  filename[::module]. Preload the file and, optionally, import
                 the module                                             [string]
      --verbosity  control how much output is produced (0 to 5)
                                                           [number] [default: 2]

quint repl

The REPL is especially useful for learning the language. See the repl documentation for more details.

The verbosity levels 3 and 4 are used to show execution details. They are especially useful for debugging complex specifications.

Command compile

$  quint compile --help
quint compile <input>
 
compile a Quint specification into the target, the output is written to stdout
 
Options:
  --help       Show help                                               [boolean]
  --version    Show version number                                     [boolean]
  --out        output file (suppresses all console output)              [string]
  --main       name of the main module (by default, computed from filename)
                                                                        [string]
  --init       name of the initializer action         [string] [default: "init"]
  --step       name of the step action                [string] [default: "step"]
  --invariant  the invariants to check, separated by commas (e.g.)      [string]
  --temporal   the temporal properties to check, separated by commas    [string]
  --target     the compilation target. Supported values: tlaplus, json
                                                      [string] [default: "json"]
  --verbosity  control how much output is produced (0 to 5)[number] [default: 2]

Given a quint specification as input, this command parses, resolves imports, typechecks, and then "flattens" the specification into on module containing just the needed definitions.

The main module is determined as follows: If a module name is specified by --main, that takes precedence. Otherwise, if there is only one module in the input file, that is the main module. Otherwise, the module with the same name as the file is taken to be the main module.

The main module must specify a state machine. This means it must either define actions named init and step, specifying the initial state and the transition action respectively, or suitable actions defined in the main module must be indicated using the --init and --step options.

The following compilation targets are supported

• json: The default target, this produces a json representation, in the same format which is described under parse and typecheck, below.
• tlaplus: Quint uses its integration with Apalache to compile the specification into TLA+.

Command parse

Warning: The language is still in active development, and breaking changes are to be expected.

$ quint parse --help
quint parse <input>
 
parse a Quint specification
 
Options:
  --help         Show help                                             [boolean]
  --version      Show version number                                   [boolean]
  --out          output file                                            [string]
  --source-map   name of the source map                                 [string]

This command reads a Quint specification from the file <spec>.qnt, parses the specification and resolves the imports relative to the directory of <spec>.qnt. If the command produces errors, these errors are printed on stderr. If there are no errors, nothing is printed.

If the user supplies the flag --out, then the parsing result is written to the file <out>.json. Depending on the outcome, the following is written:

• If the command succeeds, the file contains the parsed and resolved module in Quint IR (opens in a new tab) (JSON):

  {
    "stage": "parsing",
    "module": <IR>,
    "warnings": [ <warnings> ]
  }

  The module contents is the JSON representation of Quint IR (opens in a new tab). The warnings are written in the format of ADR002.

• If the command fails, the file contains an error message in JSON:

  {
    "stage": "parsing",
    "errors": [ <errors> ]
  }

  The errors and warnings are written in the format of ADR002.

Command typecheck

quint typecheck [--out=<out>.json] <spec>.qnt

This command infers types in the Quint specification, which is provided in the input file <spec>.qnt. Before doing that, it performs the same steps as the command parse. If the command produces errors, these errors are printed on stderr. If there are no errors, nothing is printed.

Option --out. If the user supplies the flag --out, then the parsing result is written to the file <out>.json. Depending on the outcome, the following is written:

• If the command succeeds, the file contains the parsed and resolved module in Quint IR (opens in a new tab) (JSON):

  {
    "stage": "typechecking",
    "module": <IR>,
    "types": { <typemap> }
    "effects": { <effectmap> }
  }

  The module contents is the JSON representation of Quint IR (opens in a new tab), the types and effects map source IDs of entities in the module to their inferred type or effect.

• If the command fails, the file contains an error message in JSON:

  {
    "stage": "typechecking",
    "errors": [ <errors> ]
  }

  The errors and warnings are written in the format of ADR002.

Command run

$ quint run --help
quint run <input>
 
Simulate a Quint specification and (optionally) check invariants
 
Options:
  --help         Show help                                             [boolean]
  --version      Show version number                                   [boolean]
  --main         name of the main module (by default, computed from filename)
                                                                        [string]
  --out          output file (suppresses all console output)            [string]
  --out-itf      output the trace in the Informal Trace Format to file
                 (suppresses all console output)                         [string]
  --max-samples  the maximum on the number of traces to try
                                                       [number] [default: 10000]
  --n-traces     how many traces to generate (only affects output to out-itf)
                                                           [number] [default: 1]                                                       
  --max-steps    the maximum on the number of steps in every trace
                                                          [number] [default: 20]
  --init         name of the initializer action       [string] [default: "init"]
  --step         name of the step action              [string] [default: "step"]
  --invariant    invariant to check: a definition name or an expression
                                                    [string] [default: ["true"]]
  --seed         random seed to use for non-deterministic choice        [string]
  --mbt          (experimental) whether to produce metadata to be used by
                 model-based testing                  [boolean] [default: false]

• If there are no critical errors (e.g., in parsing, typechecking, etc.), the simulator tries to find the shortest trace that violates the invariant. If it finds one, it prints the trace on the standard output. If it does not find a violating trace, it prints the longest sample trace that the simulator has found during the execution. When the parameter --out is supplied, the trace is written as a JSON representation of Quint IR in the output file. When the parameter --out-itf is supplied, the traces are written in the Informal Trace Format (opens in a new tab). This output can be conviently displayed with the ITF Trace Viewer (opens in a new tab), or just with jq (opens in a new tab).

• If the specification cannot be run (e.g., due to a parsing error), the file contains an error message in JSON:

  {
    "stage": "running",
    "errors": [ <errors> ]
  }

  The errors and warnings are written in the format of ADR002.

The --mbt flag

When this flag is given, the Quint simulator will keep track of two additional variables on the traces it produces:

• action_taken: The first action executed by the simulator on each step, reset at every any evaluation. That is, if the spec has nested any statements, action_taken will correspond to the action picked in the innermost any.
• nondet_picks: A record with all nondet values that were picked since the last any was called (or since the start, if there were no any calls in the step).

Keep in mind that this is an experimental flag and it is specially subject to changes in its behavior.

Command test

$ quint test --help
quint test <input>
 
Run tests against a Quint specification
 
Options:
  --help       Show help                                               [boolean]
  --version    Show version number                                     [boolean]
  --main       name of the main module (by default, computed from filename)
                                                                        [string]
  --out        output file (suppresses all console output)              [string]
  --max-samples  the maximum number of successful runs to try for every
                 randomized test                       [number] [default: 10000]
  --seed       random seed to use for non-deterministic choice          [string]
  --verbosity  control how much output is produced (0 to 5)[number] [default: 2]
  --match      a string or regex that selects names to use as tests     [string]

• If there are no critical errors (e.g., in parsing, typechecking, etc.), the command succeeds. The output file contains the parsed and resolved module in Quint IR (opens in a new tab) (JSON):

  {
    "stage": "testing",
    "passed": [ <names of the successful tests> ],
    "failed": [ <names of the failed tests> ],
    "ignored": [ <names of the ignored tests> ],
    "errors": [ <errors and warnings> ]
  }

• If the tests cannot be run (e.g., due to a parsing error), the file contains an error message in JSON:

  {
    "stage": "testing",
    "errors": [ <errors and warnings> ]
  }

  The errors and warnings are written in the format of ADR002.

Command verify

$  quint verify --help
quint verify <input>
 
Verify a Quint specification via Apalache
 
Options:
  --help                Show help                                      [boolean]
  --version             Show version number                            [boolean]
  --out                 output file (suppresses all console output)     [string]
  --main                name of the main module (by default, computed from
                        filename)                                       [string]
  --init                name of the initializer action[string] [default: "init"]
  --step                name of the step action       [string] [default: "step"]
  --invariant           the invariants to check, separated by commas (e.g.)
                                                                        [string]
  --temporal            the temporal properties to check, separated by commas
                                                                        [string]
  --out-itf             output the trace in the Informal Trace Format to file
                        (suppresses all console output)                 [string]
  --max-steps           the maximum number of steps in every trace
                                                          [number] [default: 10]
  --random-transitions  choose transitions at random (= use symbolic simulation)
                                                      [boolean] [default: false]
  --apalache-config     path to an additional Apalache configuration file (in
                        JSON)                                           [string]
  --verbosity           control how much output is produced (0 to 5)
                                                           [number] [default: 2]

By default, this command will automatically obtain and run Apalache. The only prerequisite is a compatible installation of OpenJDK.

You may also manually obtain and run a distribution of Apalache, following these steps:

1. Install a distribution of Apalache (opens in a new tab).
2. Start the Apalache server apalache-mc server and ensure that it is running.

Apalache uses bounded model checking. This technique checks all runs up to --max-steps steps via z3 (opens in a new tab). Apalache is highly configurable. See Apalache configuration (opens in a new tab) for guidance.

• If there are no critical errors (e.g., in parsing, typechecking, etc.), this command sends the Quint specification to the Apalache (opens in a new tab) model checker, which will try to find an invariant violation. If it finds one, it prints the trace on the standard output. When the parameter --out is supplied, the trace is written as a JSON representation of Quint IR in the output file. When the parameter --out-itf is supplied, the trace is written in the Informal Trace Format (opens in a new tab). This output can be conveniently displayed with the ITF Trace Viewer (opens in a new tab), or just with jq (opens in a new tab).

• If the specification cannot be run (e.g., due to a parsing error), the file contains an error message in JSON:

  {
    "stage": "verifying",
    "errors": [ <errors> ]
  }

  The errors and warnings are written in the format of ADR002.

Command lint

This command is not implemented yet.

quint lint [--config=config.json] [--out=<out>.json] <spec>.qnt

This command checks an input specification <spec>.qnt against a set of rules. If no errors or warnings are found, this command outputs nothing. When errors or warning are found, this command outputs them to stderr, unless the command --out is specified.

Option --config. This parameter specifies a configuration file in the JSON format. This configuration files specifies linting rules. The exact format is to be specified in the future.

Option --out. If the user supplies the flag --out, then the result is written to the file <out>.json. Depending on the outcome, the following is written:

• If the command succeeds, the file contains the success data structure:

  {
    "status": "linted"
  }

• If the command fails, the file contains error messages and warnings in JSON:

  {
    "result": "error",
    "messages": [ <errors and warnings> ]
  }

  The errors and warnings are written in the format of ADR002.

Command indent

This command is not implemented yet.

quint indent [--config=config.json] [--out=<out>.qnt] <spec>.qnt

This rule formats the input specification according to the default indentation rules. Unless the option --out is specified, the formatted specification is written on the standard output.

Option --out. The optional parameter --out specifies the name of an output file in the Quint format.

Option --config. This parameter specifies a configuration file in the JSON format. This configuration files specifies the indentation rules. The exact format is to be specified in the future.