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

v0.19.3

v0.19.3 -- 2024-05-07

Added

• Added static analysis checks to ensure proper usage of nondet and oneOf (#1431).

Changed

Deprecated

Removed

Fixed

Security

v0.19.2

v0.19.2 -- 2024-04-09

Added

Changed

Deprecated

Removed

Fixed

• Fix a problem where empty tuples were not parsed as valid types, only as
  values (#1421).

Security

v0.19.1

v0.19.1 -- 2024-04-01

Added

Changed

Deprecated

Removed

Fixed

• Fix a problem where sum types with no parameters were being printed with
  either Quint's unit type () or Apalache's unit type "U_OF_UNIT" (#1416).

Security

v0.19.0

v0.19.0 -- 2024-03-25

Added

• Added polymorphic type declarations, allowing abstracting commonly used data
  types like Option[a] and Result[err, ok]. Note that this is not yet
  supported by verify. (#1298)
• Added compile subcommand, allowing compiling specs to TLA+ (via Apalache)
  and to a JSON format. (#1309, #359)

Changed

• The latest supported node version is now bounded at <= 20, which covers the
  latest LTS. (#1380)
• Shadowing names are now supported, which means that the same name can be redefined
  in nested scopes. (#1394)
• The canonical unit type is now the empty tuple, (), rather than the empty
  record, {}. This should only affect invisible things to do with sum type
  constructors. (#1401)

Deprecated

Removed

Fixed

• Removed a dependency causing deprecation errors messages to be emitted.
  (#1380)
• Fixed a type checker bug causing too general types to be inferred (#1409).
• Fixes serialization of Sets in JSON outputs (#1410).

Security

v0.18.3

v0.18.3 -- 2024-02-08

Added

Changed

Deprecated

Removed

Fixed

• Erroneous effect checking failure resulting from invalid occurs check. This
  error prevented some valid specs from being simulated or verified (#1359).
• Regression on ITF production, where we stopped producing ITF traces on
  successful runs (#1362)

Security

v0.18.2

v0.18.2 -- 2024-01-26

Added

Changed

• Improved error reporting for runtime errors during simulation (#1349).

Deprecated

Removed

Fixed

Security

v0.18.1

v0.18.1 -- 2024-01-16

Added

Changed

Deprecated

Removed

Fixed

• Fixed parsing of qualified type constructors, which were being misinterpreted
  as type variables when the name of the qualifying module started with a
  lowercase letter (#1337).
• Fixed an issue where, sometimes, runtime errors were not reported in
  simulation (#1339)

Security

v0.18.0

v0.18.0 -- 2024-01-03

Added

• Add a run operator A.expect(P) to test the state predicate P in the state resulting from applying action A (#1303)

Changed

• Change in A.then(B): If A returns false, A.then(B) fails (#1304)

Deprecated

Removed

Fixed

• Detect import paths that only differ in capitalization (#1295)

Security