v0.22.4

v0.22.4 -- 2024-11-19

Added

Changed

Deprecated

Removed

Fixed

• Fixed a problem where traces other than the first one when --n-traces > 1
  and --mbt is true had the incorrect action_taken and nondet_picks values
  (#1553).

Security

v0.22.3

v0.22.3 -- 2024-10-28

Added

• Added a new operator called getOnlyElement() to extract elements out of singleton sets (#1525)

Changed

• Updated grammar rule to allow an optional trailing comma in parameter lists (#1510):
  • Operator calls
  • Constant initialization
  • Operator definitions

Deprecated

Removed

Fixed

• The seed was not being properly printed when the simulator found some runtime errors (#1524).
• Fixed a problem where using --mbt resulted in missing data on nondet_picks
  due to internal caching (#1531)
• Hashbang lines are now properly highlighted as comments in vscode and in highlight.js.

Security

v0.22.2

v0.22.2 -- 2024-10-08

Added

• quint verify has the option --apalache-version to pull a custom version (#1521)
• Grammar updated with support for an optional leading hashbang (#!) line (#1522)

Changed

Deprecated

Removed

Fixed

Security

v0.22.1

v0.22.1 -- 2024-09-25

Added

Changed

Deprecated

Removed

Fixed

• Some error scenarios when importing files on Windows were fixed (#1498)
• quint verify on Windows should now properly start an Apalache server on the
  background (#1499)

Security

v0.22.0

v0.22.0 -- 2024-09-09

Added

• Calling q::test, q::testOnce and q::lastTrace on the REPL now works properly (#1495)

Changed

• Performance of the REPL was drastically improved (#1495)
• Error reporting was improved for many runtime errors (#1495)

Deprecated

Removed

Fixed

• Sending SIGINT (hitting Ctrl+C) to the run and test commands now actually stops the execution (#1495)

Security

v0.21.2

v0.21.2 -- 2024-09-09

Added

• In the verify command, add warning if --out-itf option contains {test} or {seq} as those have no effect since Apalache only produces a single trace (#1485)
• The run and test commands now display a progress bar (#1457)

Changed

• Performance of incrementally checking types (i.e. in REPL) was improved (#1483).
• In the run and test commands, change placeholders from {} to {test} and from {#} to {seq} (#1485)
• In the run command, auto-append trace sequence number to filename if more than one trace is present and {seq} is not specified (#1485)
• In the test command, rename --output to --out-itf

Deprecated

• In the test command, deprecate --output option in favour of --out-itf, add hidden alias for the former (#1485)

Removed

• In the test command, stop enforcing .itf.json extension (#1485)

Fixed

• Bumped GRPC message sizes to 1G (#1480)
• Fix format of ITF trace emitted by verify command (#1448)
• Relax uppercase check for types qualified with a namespace (#1494)

Security

v0.21.1

v0.21.1 -- 2024-07-29

Added

Changed

Deprecated

Removed

Fixed

• Fixed an issue that caused high memory usage on exploration (#1465)

Security

v0.21.0

v0.21.0 -- 2024-06-16

Added

• Added an --n-traces option to the run subcommand so multiple traces can be
  produced in a single CLI call (#1365).

Changed

Deprecated

Removed

Fixed

• Fixed a problem where random numbers were internally produced without being
  used. This affects behavior of randomness, and therefore same seeds will
  behave differently before and after this version (#1453).

Security

v0.20.0

v0.20.0 -- 2024-05-22

Added

• Added an experimental --mbt flag to produce metadata that is useful for
  Model-Based Testing (#1441).
• Added the allListsUpTo, a limited but computable version of allLists (#1442)

Changed

• Shadowing is a bit less agressive. This should improve readability of variable
  names after compilation, i.e. in Apalache and some simulation errors, and in
  TLA+ produced from the compile command (#1444).

Deprecated

Removed

Fixed

Security

v0.19.4

v0.19.4 -- 2024-05-14

Added

Changed

Deprecated

Removed

Fixed

• Fixed a bug introduced in v0.19.3 where the analyzer would crash if there were
  some specific type errors (#1436)

Security