Skip to content

v0.8.0
Compare
Choose a tag to compare
@shonfeder shonfeder released this 05 Jan 22:12
· 4873 commits to main since this release
v0.8.0
05dfdb8
This commit was created on github.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Learn about vigilant mode.

0.8.0 [RELEASE]

  • use openjdk-9 for deterministic Apalache Docker images, see #318
  • support for advanced syntax in TLC configs, see #208
  • random seed for z3, see docs/tuning.md and #318
  • correct translation of chained substitutions in INSTANCEs, see #143
  • friendly messages for unexpected expressions, see #303
  • better operator inlining, see #283
  • support for standard modules that are instantiated with LOCAL INSTANCE, see #295
  • support for LAMBDAs, see #285 and #289
  • bugfix in treatment of recursive operators, see #273
  • no theories in the model checker due to types, see #22
  • operators and checker caches made Serializable
  • better diagnostics for the recursive operators, see #272
  • verbose output for the config parser, see #266
  • Use a staged docker build, reducing container size ~70%, see #195
  • Use Z3-TurnKey instead of a
    bespoke Z3 build, see #219
  • Use Z3 version 4.8.7.1, see #219
  • Re-stabilized tests on recursive operators, see #344
  • Changed the assignment paradigm; solver now finds assignments without SMT, see #366
Assets 4
Loading