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

v0.17.1

v0.17.1 -- 2023-12-05

Added

• Add a q::debug built-in function for printing values to stdout (#1266)

Changed

Deprecated

Removed

Fixed

• The effect checker now distinguishes variables from different instances (#1290)

Security

v0.17.0

v0.17.0 -- 2023-12-04

Added

• When an input file only one module, it will be inferred as the main module (#1260)
• Sum types are now supported when running verify (#1034)

Changed

Deprecated

Removed

Fixed

• Produce proper error messages on invalid module name (#1260)
• Fix JSON output when running multiple tests (#1264)
• Topological sorting of modules (#1268)
• The effect checker will now check for consistency of updates across different
  cases inside match (#1272)
• Fix problems in the integration of sum types in run, test, and verify commands (#1276)
• Fix some corner cases with the usage of complex expressions inside assume
  and import (...) (#1276)
• Fix incorrect type checking failure from interference between sum types
  sharing variant labels (#1275)
• Fix the IDs generated for operator definition bodies (#1280)
• Fixed missing support for sum type variants in ITF traces (#1281)

Security