v0.30.9

0.30.9 - 2023-05-08

Bug fixes

• Fix conversion of quint records. See #2542.

v0.30.8

0.30.8 - 2023-04-17

Features

• Add support for converting quint record operators. See #2530.

Bug fixes

• Fix conversion of quint setBy operator. See #2531.

v0.30.7

0.30.7 - 2023-04-11

Bug fixes

• Fix conversion of quint binding operators to support operator passed by name. See #2520.

v0.30.6

0.30.6 - 2023-04-01

Features

• Add conversion of quint operators range, foldr, assert, select, and operators over maps (TLA+ functions). See #2439, #2489, #2492, #2493.
• Support conversion of Quin't nondet bindings. See #2499.

Bug fixes

• Fix quint list conversion. See #2495, #2509, #2510.
• Fix conversion of quint let-binding. See #2501.

v0.30.5

0.30.5 - 2023-03-10

Breaking changes

• Updated support for quint input, for compatibility with the (forthcoming) Quint v0.8.0. Output from earlier versions of quint will no longer be supported. See #2473 and informalsystems/quint#689.

Features

• Add support for quint tuples. See #2441.
• Add support for converting (most) quint list operator. See #2440.
• Added support for quint's variadic bindings in forall and exists operators. See #2471.

v0.30.4

0.30.4 - 2023-03-08

Bug fixes

• Fix the typing of quint empty sets during conversion (see #2466)

v0.30.3

0.30.3 - 2023-03-06

Features

• Added support for transpiling quint booleans, integers, and sets (See #2451, #2449, #2445)

Bug fixes

• Add support for first-order CONSTANTS, see #2389.
• Fixed type checking of specs that use Print and PrintT, see #2456.

v0.30.2

0.30.2 - 2023-02-22

Features

• Added support for inputing a spec written in a small fragment of quint (see #2421).

Bug fixes

• Fix parsing of lines longer than 999 characters, see #2430

v0.30.1

0.30.1 - 2022-11-07

Features

• Server port is now configurable via the --port CLI argument or server.port configuration key (see #2264).

v0.30.0

0.30.0 - 2022-10-31

Breaking changes

• The format of parsing error outputs has been changed. Parsing error messages that used to be prefixed with Error by TLA+ parser are now prefixed with Parsing error and error messages that used to begin with Syntax error in annotation: will now also include the Parsing error prefix. This is being recorded as a breaking change since it could break scripts that rely on parsing stdout. (See #2204 and #2242.)

Features

• Return JSON with success or failure data from RPC calls to the CmdExecutor service (see #2186).

Bug fixes

• Write the SMT log also to a custom rundir specified with --run-dir=, see #2208