Before translating a specification into SMT,
apalache performs a number of
- replaces every call to a user-defined operator with the operator's body
- replaces every call to a let-in defined operator of arity at least 1 with the operator's body
PrimingPass: adds primes to variables in
VCGen: extracts verification conditions from the invariant candidate.
Desugarer: removes syntactic sugar like short-hand expressions in
Normalizer: rewrites all expressions in negation-normal form.
Keramelizer: translates TLA+ expressions into the kernel language KerA.
ExprOptimizer: statically computes select expressions (e.g. record field access from a known record)
ConstSimplifier: propagates constants
Keramelizer rewrites TLA+ expressions into KerA. For many TLA+ expressions this translation is clear, however, some expressions cannot be easily translated. Below we discuss such expressions and the decisions that we have made.