Release v0.17.0

[shonfeder]

v0.17.0 -- 2023-12-04

Added

• When an input file only one module, it will be inferred as the main module (Fix the default module in quint run and quint test #1260)
• Sum types are now supported when running verify (Support conversion of sum types in Apalache #1034)

Changed

Deprecated

Removed

Fixed

• Produce proper error messages on invalid module name (Fix the default module in quint run and quint test #1260)
• Fix JSON output when running multiple tests (fix: reset trace recorder at beginning of each test run #1264)
• Topological sorting of modules (Toposort on modules #1268)
• The effect checker will now check for consistency of updates across different
  cases inside match (Fix effect signature for the match operator #1272)
• Fix problems in the integration of sum types in run, test, and verify commands (Two fixes for Paxos simulation #1276)
• Fix some corner cases with the usage of complex expressions inside assume
  and import (...) (Two fixes for Paxos simulation #1276)
• Fix incorrect type checking failure from interference between sum types
  sharing variant labels (Sum type variants with the same label collide in type checking #1275)
• Fix the IDs generated for operator definition bodies (Fix operator declaraion lambda IDs #1280)
• Fixed missing support for sum type variants in ITF traces (Trace generation with quint test does not support sum types #1281)

Security