Skip to content

v0.6.0
Compare
Choose a tag to compare
@konnov konnov released this 14 Feb 16:16
· 5212 commits to main since this release
v0.6.0
a104ca2

0.6.0

  • Using z3 version 4.8.7

  • A 2-8x speedup for 5 out 16
    benchmarks,
    due to the optimizations and maybe switching to z3 4.8.x.

  • Distributing the releases with docker as apalache/mc

  • The results of intermediate passes are printed in TLA+ files
    in the x/* directory: out-analysis.tla, out-config.tla,
    out-inline.tla, out-opt.tla, out-parser.tla,
    out-prepro.tla, out-priming.tla, out-transition.tla,
    out-vcgen.tla

  • The model checker is translating only KerA+ expressions,
    which are produced by Keramelizer

  • Multiple optimizations that were previously done by rewriting
    rules were move to the preprocessing phase, produced by
    ExprOptimizer

  • Introducing Skolem constants for \E x \in S: P, such
    expressions are decorated with Skolem

  • Introducing Expand for SUBSET S and [S -> T], when
    they must be expanded

  • Translating e \in a..b to a <= e /\ e <= b, whenever possible

  • Supporting sequence concatenation: <<1, 2>> \o <<4, 5>>

  • Short-circuiting and lazy-circuiting of a /\ b and a \/ b
    are disabled by default (see docs/tuning.md on how to enable them)

  • Introduced PrettyWriter to nicely print TLA+ expressions
    with proper indentation

  • The preprocessing steps -- which were scattered across the code
    -- are extracted in the module tla-pp,
    which contains: ConstAndDefRewriter, ConstSimplifier,
    Desugarer, Normalizer, see preprocessing

  • Bounded variables are uniquely renamed by Renaming
    and IncrementalRenaming

  • Massive refactoring of the TLA intermediate representation

  • TLA+ importer stopped chocking on the rare TLA+ syntax, e.g.,
    ASSUME and THEOREM

  • Backtracking expressions to their source location in a TLA+ spec

  • LET-IN is translated into LetInEx in tlair

  • Nullary LET-IN expressions (without arguments) are processed by
    the model checker directly, no expansion needed

  • The assignment solver has been refactored. The assignments are
    now translated to BMC!<-, for instance, x' <- S

  • Constant assignments in ConstInit are now preprocessed correctly

  • User operators are not translated to TlaUserOper anymore,
    but are called with TlaOper.apply

  • Importing tla2tools.jar from Maven Central

Assets 4
Loading