v0.20.3

0.20.3

Features

• Implemented SetAsFun and use it in counterexamples instead of :> and @@, see #1319, #1327

Bug fixes

• Fixed infinite recursion in consChain, see #1307
• Fixed a bug where some simplified Or expressions were not expected by the rewriting rules, see #1285
• Fixed a bug on broken --view, see #1327

v0.20.2

0.20.2

Bug fixes

• Fix polymorphic types when the type checker is called twice, see #1300

v0.20.1

0.20.1

Breaking changes

• version command only prints the version, see #1279
• tool and jar location no longer output by default, see #1279

Features

• Added support for --output with typecheck, see #1284

Bug fixes

• Fixed JSON decoder failing on inputs with "Untyped", see #1281
• Fixed JSON decoder failing on inputs with "FUN_REC_REF" or "FUN_REC_CTOR"
• Correctly resolve higher-order operators in names instances, see #1289
• Fix ITF output for singleton functions, see #1293

v0.20.0

0.20.0

Breaking changes

• Switched build system from maven to sbt (note, will only cause breakage in
  pipelines that build from source), See #1234.

Features

• Completely remove TlcOper and replace it with a custom TLA+ module, see #1253

Bug fixes

• Fix the semantics of @@ by using the TLC definition, see #1182, #951, #1234
• Fix unexpected polymorphism, see #1262

v0.19.3

0.19.3

Bug fixes

• Fix the ITF writer on empty functions, see #1232

v0.19.2

0.19.2

Design

• ADR-014 on precise type checking for records and variants, see #1151

Features

• Output in the Informal Trace Format, see #1220

Bug fixes

• Add constant simplification rules that may improve performance in specific scenarios, see #1206
• Fix expansion of ~ in configured paths, see #1208
• Fix a bug where an implication with its left side simplified to the TRUE constant was incorrectly translated, see #1206

v0.19.1

0.19.1

Features

• New errors for the following constant simplification scenarios (see #1191):
  1. Division by 0
  2. Mod (%) by 0
  3. Negative expoents
  4. Expoents bigger than an Integer
  5. Expoential operations that would overflow BigInt

v0.19.0

0.19.0

Breaking changes

• The global config file is now named $HOME/.tlaplus/apalache.cfg, see #1160

Features

• Support for a local config file (defaulting to $PWD/.apalache.cfg) see #1160

Bug fixes

• Fix the use of set union in the array encoding, see #1162
• Fix preprocesor's normalization of negated temporal formulas and negated LET .. IN expressions, see #1165

v0.18.1

0.18.1

Bug fixes

• Fix the use of set minus in the array encoding, see #1152

v0.18.0

0.18.0

Features

• Add bug report templates, see #1094

• Improve the format of uninterpreted constants to name_OF_TYPE, see #1130

Bug fixes

• Remove duplicate function indices when decoding symbolic states, fixes #962

• Translate a^b for non-constant a and b, fixes #1136

Refactoring

• Change the format of type exceptions, see #1090

• Remove duplicate function indices when decoding symbolic states, fixes #962

• Improve error messaging for Seq, see #1126 and #1127

Documentation

• Restructure and update the Apalache manual:
  https://apalache.informal.systems/docs/index.html