- Add the experimental command
simulate
that randomly picks transitions, see #1809
- Fix nested set membership in the arrays encoding, see #1819
- Fixed bug in inlining ASSUME statements, see #1794
- Introduce dedicated exit codes for type-checking errors, parser errors, and evaluation errors (e.g., due to unsupported language constructs or operators), see #1749
- Support sound records (over rows) in the model checker, see #1717
- Fix potential non-determinism when picking from
[S -> T]
, see #1753 - Fix the bug in uninterpreted types, see #1792
- Support sound records (over rows) in the model checker, see #1717
- Support for native ARM64/AArch64 JVMs (and thus Apple Silicon), see #751
- Fix usage of sets of function sets in the arrays encoding, see #1680
- Fix an uncaught exception when setting up the output manager, see #1706
- Handle heap memory exhaustion gracefully, see #1711
- Recommended JDK version was bumped to JDK17, see #1662
- Add the option
--features
to enable experimental features, see #1648 - Never report a deadlock when
--no-deadlock=1
, see #1679
- Include the version number in
detailed.log
, see #1678 - Add the option
--features
to enable experimental features, see #1648 - Never load TLC config files by default, see #1676
- Experimental type unification over rows, new records, and variants, see #1646
- Experimental type checking for records over rows, see #1688
- Fix references to
--tune-here
(actually--tuning-options
), see #1579 - Not failing when assignment and
UNCHANGED
appear in invariants, see #1664
- Rename
--tuning
to--tuning-options-file
, see #1579
- Fix references to
--tune-here
(actually--tuning-options
), see #1579
RECURSIVE
operators and functions are no longer supported, see #1569- rename Apalache
FoldSet
andFoldSeq
toApaFoldSet
andApaFoldSeqLeft
, see #1617
- Add the operator
Apalache!Guess
, see #1590 and #888 - Extend the type parser to support ADR014 (experimental), see #1602
- Keramelizer now rewrites \subseteq using forall quantification, see #1408
- Builtin operators can be passed as arguments to HO operators, see #1630
- Optimize set membership for record sets, see #1629
- Fix the generation of SMT instances with the
--debug
flag, see #1594 - Fix symbolic link generation in 'make' on Windows, see #1596
- Rework module lookup (drops support for
TLA_PATH
), see #1491
- Look up modules in the same directory, see #1491
- Support for the community module
SequencesExt
, see #1539 - Support for the community module
BagsExt
, see #1555 - Support for the community module
Folds
, see #1558
- Pack arithmetic expressions and comparisons into a single SMT constraint, see #1540 and #1545
- Fix uncaught
FileNotFoundException
in commands called on nonexistent files, see #1503 - Fix equality on sequences, see #1548, #1554
- An optimization in function application, see #1500
- Fix stack overflow and out-of-memory in function operators, see #1498
- Fix function application static check in arrays encoding, see #1490
- Add support for the community modules FiniteSetsExt and Functions, see #1484
- Add support for Bags, see #1527
- Enable records in the arrays encoding, see #1288
- Enable the remaining TLA+ features in the arrays encoding, see #1418
- Implement the sequence constructor
Apalache!MkSeq
, see #1439 - Add support for
Apalache!FunAsSeq
, see #1442 - Implement
EXCEPT
on sequences, see #1444 - Cache default values, see #1465
- Fixed bug where TLA+
LAMBDA
s wouldn't inline outsideFold
andMkSeq
, see #1446 - Fix the comment preprocessor to extract annotations after a linefeed, see #1456
- Fix the failing property-based test, see #1454
- Fixed a bug where call-by-name embedding wasn't properly called recursively
- Fix a corner case in
\E x \in S: P
, see #1426
- Complete rework of sequences, see #1353
- The
profiling.csv
file output by the--smtprof
flag moved into the configurablerun-dir
, see #1321 - The distribution package structure has changed. This shouldn't cause any breakage in operation, but may impact some automated deployment pipelines, see #1357
UNCHANGED x
now rewrites tox' := x
instead ofx' = x
, whenx
is a variable name- Some simple type errors have more informative messages, see #1341
- Handle
Cardinality(SUBSET S)
without failing, see #1370 - Add support for functions in the arrays encoding, see #1169
- Implemented
SetAsFun
and use it in counterexamples instead of:>
and@@
, see #1319, #1327
- 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
- Fix polymorphic types when the type checker is called twice, see #1300
version
command only prints the version, see #1279- tool and jar location no longer output by default, see #1279
- Added support for
--output
withtypecheck
, see #1284
- 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
- Switched build system from maven to sbt (note, will only cause breakage in pipelines that build from source), See #1234.
- Completely remove TlcOper and replace it with a custom TLA+ module, see #1253
- Fix the semantics of @@ by using the TLC definition, see #1182, #951, #1234
- Fix unexpected polymorphism, see #1262
- Fix the ITF writer on empty functions, see #1232
- ADR-014 on precise type checking for records and variants, see #1151
- Output in the Informal Trace Format, see #1220
- 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
- New errors for the following constant simplification scenarios (see #1191):
- Division by 0
- Mod (%) by 0
- Negative expoents
- Expoents bigger than an Integer
- Expoential operations that would overflow
BigInt
- The global config file is now named
$HOME/.tlaplus/apalache.cfg
, see #1160
- Support for a local config file (defaulting to
$PWD/.apalache.cfg
) see #1160
- 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
- Fix the use of set minus in the array encoding, see #1152
-
Add bug report templates, see #1094
-
Improve the format of uninterpreted constants to name_OF_TYPE, see #1130
-
Remove duplicate function indices when decoding symbolic states, fixes #962
-
Translate
a^b
for non-constanta
andb
, fixes #1136
-
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
- Restructure and update the Apalache manual: https://apalache.informal.systems/docs/index.html
- Fix computation of principal types, see #1084
- Fix error leaving contents in run-dir as empty files, see #1119
- Added support for sets to the SMT encoding with arrays, see #1092
- Add
--run-dir
flag, enabling users to write outputs directly to a known and stable location, see #1081
- Added sort-distinction for model values, see #570
- Fixed handling of polymorphic operators in folds, see #1085
- Fix regression breaking
--output
file format detection in parser command, see #1079
- Fix regression breaking behavior of
--output
flag, see #1072, #1073
- Add smt-encoding option to CLI check command, see #1053
- Added CLI and configuration interface for managing generated outputs, see #1025, #1036, #1062, #1065
- Propagate constraints passed in --cinit, see #1023
- Propagate constraints passed ASSUME, see #880
- Fix type checker to complain about polymorphism in the post phase, see #931
- Enumerated files containing intermediate module states, see #993
- Move docker containers to the GitHub container registry, see #1013
- improve SMT encoding by removing unused let-definitions, see #995
- Fixed a bug caused by big numbers on annotations, see #990
- Fixed a heisenbug caused by EXCEPT on records, which used unsorted keys, see #987
- Fixed unsound skolemization that applied to let-definitions, see #985
- Support for let-polymorphism in
typecheck
, see #869 - Support for let-polymorphism in
check
, see #953
- Fix the profiler, see #963
- Handle exceptions in record update edge case, see #917
- Fix infinite recursion in the type unifier, see #925
- Fix unhandled errors on non-existent record field access, see #874
- Fix unhandled
MatchError
on invalid operator type annotations, see #919
- Implemented support for SelectSeq, see #873
- Fixed crash on specs with no variables, see #871
- Fixed a bug which made Fold(Set/Seq) unusable in Init or CInit
- Parser: parse error on TLAPS syntax such as
Inv!2
, see #876 - Checker: support for Fold(Set/Seq), see #693
- Fixed #540
- Fixed #593
- Tool: no empty log on help message, see #830
- revision 2 of RFC006 on unit testing
- Checker: enumerating multiple counterexamples, see #542 and #827
-
Manual: manual page on enumerating counterexamples and view abstraction, see #542
-
links to ADR005
- Checker: support for action invariants, see #801
- Checker: support for trace invariants, see #819
- Add type information to overriding error, see #823
- Docker: Use openjdk-16 for the runtime in the app image, see #807
- Documentation: Introduce TypeAlises operator convention, see #808
- tlair: TlaExLevelFinder and TlaDeclLevelFinder to compute TLA+ levels, see #811
- Printer: replacing '$' and '!' with supported characters, see #574
- Printer: normalizing module names and writing TLA+ & JSON in all passes, see #785
- RFC006 on unit testing: see #741
- apalache quits with a non-zero exit code on counterexample or error, see #249
- type checker: supporting one-line comments in types, see #773
- Parser: supporting annotations in multiline comments, see #718
- Parser: supporting TLA+ identifiers in annotations, see #768
- Parser: better parser for annotations, see #757
- Parser: fixed two bugs in the declaration sorter, see #645 and #758
- Printer: fixed the output for EXCEPT, see #746
- Printer: fixed pretty printing of annotations, see #633
- Printer: extending the standard modules, see #137
- The command
config --enable-stats=true
creates$HOME/.tlaplus
if needed, see #762 - IO: replaced calls to deprecated JsonReader/JsonWriter. out-parser.json is now compliant with the new format, see #778
- Builds: removed scoverage from maven, to improve build times
- Docs: updated ADR002 and HOWTO on type annotations to explain comments
- CLI: Users can set JVM args via the JVM_ARGS env var, see #790
- Checker: Support for CASE without OTHER, see #285
- Type checker: Showing an error on missing annotations CONSTANTs or VARIABLEs, see #705
- Model checker: Fix an exception on
Cardinality(a..b) > i
, see #748
- IR: simplified
SimpleFormalParam
andOperFormalParam
intoOperParam
, see #656 - IR: made consistent the names of IR operators (may break JSON compatibility), see #634
- Manual: added manual page on known issues
- IR: added
Apalache!Gen
to generate bounded data structures, see #622 - Checker: added support for
Apalache!Gen
, see #622 - Tool: added a new command
test
to quickly evaluate an action in isolation, see #622
- Manual: added a tutorial on the type checker Snowcat, see #689
- Language manual: add types for the standard operators, see #547
- Type checker: add support for type aliases,
e.g.,
@typeAlias FOO = [a: Int, b: Int]
, see #704 - Manual: updated the HOWTO on type annotations with type aliases
- Model checker: receiving the types from with the type checker Snowcat, see #668 and #350
- Model checker and type checker: Snowcat is the only way to compute types now
- Type checker: the old Apalache type annotations are no longer supported, see #668
- Type checker: tagging all expressions with the reconstructed types, see #608
- Type checker: handling TLA+ labels like
lab("a", "b") :: e
, see #653 - Type checker: always treating
<<...>>
inUNCHANGED <<...>>
as a tuple, see #660 - Type checker: handling the general case of EXCEPT, see #617
- Preprocessing: handling the general case of EXCEPT, see #647
- Preprocessing: massive refactoring of the passes to support types. This may have introduced unexpected bugs.
- Model checker: translation rules for records and functions have been modified, in order to support new types. Bugs to be expected.
- Intermediate representation: renamed BmcOper to ApalacheOper. Its operators have the prefix
Apalache!
now.
- Unused rewriting rules and
FailPredT
in the model checker, see #665 - Intermediate representation: removed non-standard operators subsetProper, supset, supseteq, see #615
- Intermediate representation: removed TlaArithOper.{sum,prod}, as they are not standard, see #580
- Intermediate representation: removed TlaOper.chooseIdiom
- Type checker: supporting TLC operators, see #601
- Parser: propagating type annotations in INSTANCES, see #592 and #596
- Type checker: removed
Typing.tla
,AssumeType
, and##
, see #518
- Support for
FunAsSeq
conversion in the type checker, see #223 - The parser outputs annotations, see #502
- HOWTO on writing type annotations, see #571
- Fixed name collisions on LOCAL operators and LOCAL INSTANCE, see #576
- Parser: a higher-order operator calling a higher-order operator, see #575
- Type checker: support for recursive functions of multiple arguments, see #582
- Type checker: support for tuple unpacking in recursive functions, see #583
- integration with Java-like annotations in comments, see #504
- support for
Assume(...)
in the type checker - new command-line option for
typecheck
:- enable inference of polymorphic types:
--infer-poly
- enable inference of polymorphic types:
- updates to ADR002 and the manual
- support for parallel assignments
<<x', y'>> = <<1, 2>>
, see #531 - always sorting declarations with topological sort (changes the order of the operator definitions), see #122
- Boolean values are now supported in TLC config files, see #512
- Promoting Desugarer to run as the first preprocessing pass, see #531
- Proper error on invalid type annotations, the parser is strengthened with Scalacheck, see #332
- Fixed a parsing bug for strings that contain '-', see #539
- Typechecking quantifiers over tuples, see #482
- new sequential model checker that is using TransitionExecutor, see #467
- new command-line options, see #467 and the manual for details:
- choose the algorithm:
--algo=(offline|incremental)
- pre-check, whether a transition disabled, discard the disabled transitions:
--discard-disabled
- do not check for deadlocks:
--no-deadlock
- pass tuning parameters in CLI:
--tune-here
- choose the algorithm:
- parsing in-comment Java-like annotations, see #226
- tracking the source of variable/constant declarations and operator definitions in the TLA+ Parser, see #262
- the new sequential model checker has uncovered a bug that was not found by the old model checker, see #467
- ADR004: In-comment annotations for declarations (of constants, variables, operators)
- Fixed path of jar in ZIP distribution, reported in #500, see #506
- handling big integers, see #450
- better parsing of SPECIFICATION in TLC configs, see #468
- expanding tuples in quantifiers, see #476
- unfolding UNCHANGED for arbitrary expressions, see #471
- unfolding UNCHANGED <<>>, see #475
- constant simplification over strings, see #197
- propagation of primes inside expressions, e.g., (f[i])' becomes f'[i'] if both f and i are state variables
- critical bugfix in unique renaming, see #429
- include missing {Apalache,Typing}.tla modules in release package, see #447
- opt-in for statistics collection (shared with TLC and TLA+ Toolbox), see #288
- new layer of TransitionExecutor (TRex), see
at.forsyte.apalache.tla.bmcmt.trex.*
- Compile the manuals into a static site using mdBook, see #400
- Description of top-level user operators, see #419
- ADR003: Architecture of TransitionExecutor
- 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
- fixed an omitted version number update
- safe checks for the user options in ConfigurationPassImpl, see #193
- introduced the tool module
Typing.tla
, see #162 - introduced the tool module
Apalache.tla
, see #183 - Lookup for modules using TLA_PATH, see #187
- Simplify JSON format to make it suitable for JsonPath queries, see #153
- Importer from JSON, see #121
- optimization for
Cardinality(S) >= k
, see #118 - sound translation of
LOCAL
operators, see #49 - unrolling recursive operators, see #67
- support for recursive functions that return integers and Booleans, see #84
- new IR for recursive functions, see #84 and TlaFunctionOper.recFunDef
- parser for the TLC configuration files, see #76
- exporter to JSON, see #77
- counterexamples in the TLC and JSON, see #45 and #116
- fixed exit codes
EXITCODE: OK
andEXITCODE: ERROR (<code>)
- normal error messages and failure messages with stack traces
- bugfixes: #12, #104, #148
-
Critical bugfix in the optimization of set comprehensions like
\E x \in {e: y \in S}: f
-
Bugfix for #108: the model checker was skipping the
FALSE
invariant, due to an optimization
-
Using
z3
version4.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 byKeramelizer
-
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 withSkolem
-
Introducing
Expand
forSUBSET S
and[S -> T]
, when they must be expanded -
Translating
e \in a..b
toa <= e /\ e <= b
, whenever possible -
Supporting sequence concatenation:
<<1, 2>> \o <<4, 5>>
-
Short-circuiting and lazy-circuiting of
a /\ b
anda \/ 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
andIncrementalRenaming
-
Massive refactoring of the TLA intermediate representation
-
TLA+ importer stopped chocking on the rare TLA+ syntax, e.g.,
ASSUME
andTHEOREM
-
Backtracking expressions to their source location in a TLA+ spec
-
LET-IN
is translated intoLetInEx
intlair
-
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 withTlaOper.apply
-
Importing
tla2tools.jar
from Maven Central
- A backport of the build system from 0.6.0
- The artifact accepted at OOPSLA19
-
support for top-level
INSTANCE
andINSTANCE WITH
operators -
command-line option
--cinit
to initializeCONSTANTS
with a predicate -
support for
[SUBSET S -> T]
and[S -> SUBSET T]
-
support for
\E x \in Nat: p
and\E x \in Int: p
-
limited support for
Int
andNat
-
support for sequence operators:
<<..>>
,Head
,Tail
,Len
,SubSeq
,DOMAIN
-
support for FiniteSets:
Cardinality
andFiniteSet
-
support for TLC operators:
@@ and :>
-
support for complex
EXCEPT
expressions -
support for nested tuples in
UNCHANGED
, e.g.,UNCHANGED << <<a>>, <<b, c>> >>
-
speed up by using constants instead of uninterpreted functions
-
options for fine tuning with
--fine-tuning
, see tuning -
bugfix in logback configuration
-
type annotations and very simple type inference, see the notes
-
a dramatic speed up of many operators by using a
QF_NIA
theory and cherry pick -
automatic simplification of expressions, including equality
-
decomposition of invariants into smaller pieces
- the version presented at the TLA+ community meeting 2018 in Oxford