informalsystems/apalache

APALACHE: symbolic model checker for TLA+ and Quint

APALACHE

A symbolic model checker for TLA+

Apalache translates TLA+ into the logic supported by SMT solvers such as Microsoft Z3. Apalache can check inductive invariants (for fixed or bounded parameters) and check safety of bounded executions (bounded model checking). To see the list of supported TLA+ constructs, check the supported features. In general, Apalache runs under the same assumptions as TLC.

To learn more about TLA+, visit Leslie Lamport's page on TLA+ and his Video course.

Releases

Check the releases page for our latest release.

For a stable release, we recommend that you pull the latest docker image with docker pull ghcr.io/informalsystems/apalache:main, use the jar from the most recent release, or checkout the source code from the most recent release tag.

To try the latest cool features, check out the head of the main branch.

You can also find Apalache packaged via Nix at cosmos.nix

For more information on installation options, see the manual.

Getting started

• Read the Beginner's tutorial.
• Check the material at TLA-Apalache workshop.
• Read the Apalache user manual.
• Consult the (WIP) Idioms for writing better TLA+.
• Consult the (WIP) TLA+ language manual for engineers.

Website

Our current website is served at https://apalache.informal.systems .

The site is hosted by github, and changes can be made through PRs into the gh-pages branch of this repository. See the README.md on that branch for more information.

The user documentation is automatically deployed to the website branch as per the CI configuration.

Our old website is still available at https://forsyte.at/research/apalache/ .

Community

• Join the chat in the Apalache zulip stream.
• Contribute to the development of Apalache.

Help wanted

Want to contribute? Here is a list of issues that could be solved without knowing too much about the internals of Apalache. Solving these issues would improve usability! Please comment in the relevant issue, if you are going to solve it.

• Writing annotations in the JSON format: #804
• Add support for VIEW in the TLC config: #851
• Translate \E x \in STRING: P and \A x \in STRING: P: #844
• Interval analysis for a..b: #446

Industrial examples

• Check Light client specs and Model-based testing of the Tendermint light client.

• Check Tendermint specs to see how we use TLA+ and Apalache at Informal to design and specify protocols for the Tendermint blockchain.

• To see more examples, check the standard repository of TLA+ examples.

Talks

• Informal Systems Tutorial: TLA+ Basics

• Extended version of the Apalache tutorial. TLA+ tutorial at DISC 2021 (October 2021).

• How TLA+ and Apalache Helped Us to Design the Tendermint Light Client. Interchain Conversations 2020 (December 2020).

• Model-based testing with TLA+ and Apalache. TLA+ Community Event 2020 (October 2020).

• Type inference for TLA+ in Apalache. TLA+ Community Event 2020 (October 2020).

• Formal Spec and Model Checking of the Tendermint Blockchain Synchronization Protocol 2nd Workshop on Formal Methods for Blockchains (July 2020).

• Showing safety of Tendermint Consensus with TLA+ and Apalache. Dev session at Informal Systems (May 2020).

• TLA+ model checking made symbolic OOPSLA 2019 (October 2019).

• Bounded model checking of TLA+ specifications with SMT TLA+ Community Event 2018 (July 2018).

Performance

We are collecting apalache benchmarks. See the Apalache performance when checking inductive invariants and running bounded model checking. Versions 0.6.0 and 0.7.2 are a major improvement over version 0.5.2 (the version reported at OOPSLA19).

Academic papers

To read an academic paper about the theory behind Apalache, check our paper at OOPSLA19. For the details of our novel encoding using SMT arrays, check our paper at TACAS23. Related reports and publications can be found at the Apalache page at TU Wien.

---

Apalache is developed at Informal Systems.

With additional funding from
.

Past funding from Der Wiener Wissenschafts-, Forschungs- und Technologiefonds.

apalache's Issues

Refactor AssignmentPassImpl

For some reason, it calls SymbolicTransitionPass inside. The passes should be chained.

Handle operators declared as LOCAL

Currently there is no support for local operators - the solver throws an importer exception.

Cleaning at.forsyte.apalache.tla.lir

This package has collected too many TODOs over time. We have to fix them.

Remove at.forsyte.apalache.tla.lir.assignments.DisjointSets?

This class is not used

Clean up at.forsyte.apalache.tla.lir.db

The whole package seems to be to large extent deprecated

Using \subseteq as an assignment operator

Currently, the assignment finder is looking for assignments in the expressions that match one of two patterns: x = ... or x \in {...}. it is common to use other set relations in TypeOK, e.g., msgs \subseteq Messages. We have to support such subset relations as well. I guess, the latter expression could be simply translated as msgs \in SUBSET(Messages) during the preprocessing phase.

No need for assignments when using Assert(FALSE, ...)

There is a widely-used idiom in TLC that allows one to write tests like follows:

     \/ /\ Print("Starting Test 2", TRUE)
        /\ IF x' = 2 
             THEN y' = 1 
             ELSE Assert(FALSE, "Failed Test 2")

The assignment solver fails to find an assignment for the ELSE branch. One should treat Assert(FALSE, ...) as FALSE. The other kinds of assertions should not be affected.

Rewrite OperatorHandler

The code is obfuscated and not documented

Database infrastructure

Fix LetInOper

needs proper constructor and equality check methods, consider migrating to TlaControlOper inner class.

Assume import

Multiple ASSUME statements trigger IllegalStateException("The context has duplicate keys!") in at.forsyte.apalache.tla.imp.Context.scala

Consider removing RecursiveProcessor

RecursiveProcessor seems to be a home-brewed lambda calculus inside Scala. Although it is rarely used, its applications are hard to understand. In those rare cases, when RecursiveProcessor is used, instantiate the code directly with the given parameters. It will be much easier to read. For instance, RecursiveProcessor.compute takes 6 parameters, each of them is a parameterized function.

Hand-coded IR Example: ABP

Comparison to an empty set

In some cases, a comparison to an empty set fails. When such a comparison propagates to the level of Z3, the solver complains about incompatible sorts, e.g., comparing Cell_Si to Cell_Su. For instance, check test/tla/Bakery.tla, replace EmptyIntSet == {1} \ {1} with EmptyIntSet == {}.

This problem should be resolved as soon as we have the proper type inference engine.

Eliminate theories

A symbolic state carries a theory (IntTheory, BoolTheory, CellTheory). These theories became irrelevant in the presence of types and the multi-sorted encoding. Remove them.

Importer not handling @ shorthand

On code such as
[msgs EXCEPT ![self] = @ \ {q}]
the importer throws
at.forsyte.apalache.tla.imp.SanyImporterException: Unexpected subclass of tla2sany.ExprOrOpArgNode: class tla2sany.semantic.AtNode

Consume SANY from maven central

https://oss.sonatype.org/content/repositories/snapshots/org/lamport/tla2tools/1.6.0-SNAPSHOT/

Let me know if you want 1.5.x too

Plugins + controller classes

Cleaner

Eliminate UniqueDB

Collecting expressions and their ids in a singleton is evil, as it stays in memory forever. If you have to map UID to TlaEx, use Map[UID, TlaEx] locally, so the garbage collector could eventually free it.

Fix TODOs in apalache.tla.bmcmt

eliminate EnvironmentHandler

It contains too much magic. Remove the unused methods and extract the used methods in separate classes with clear names and documentation.

Assignment solver loops on a simple input

---- MODULE boolconst ----
VARIABLES x
Init == x = 2
Next == x' = x
================================

Infinite loop in SpecHandler

The following code triggers a stack overflow:

java.lang.StackOverflowError: null
	at scala.collection.immutable.List.drop(List.scala:223)
	at scala.collection.immutable.List.drop(List.scala:86)
	at scala.collection.LinearSeqOptimized.apply(LinearSeqOptimized.scala:62)
	at scala.collection.LinearSeqOptimized.apply$(LinearSeqOptimized.scala:61)
	at scala.collection.immutable.List.apply(List.scala:86)
	at at.forsyte.apalache.tla.lir.OperatorHandler$.subAndID$1(OperatorHandler.scala:324)

--------------- MODULE test4 -------------
EXTENDS Naturals, TLC, Sequences
VARIABLE x, y, z, w

Init == 
  /\ Print("Should find only one distinct state", TRUE)
  /\ x = {1, 2, 3}
  /\ y = {"a", "b", "c"}
  /\ z = [a : {1, 2, 3}, b : {1, 2, 3}, c : {1, 2, 3}]
  /\ w = [{1, 2, 3} -> {1, 2, 3}]

Inv  == 
  /\ TRUE
  /\ x = {1, 2, 3}
  /\ y = {"a", "b", "c"}
  /\ z = [a : {1, 2, 3}, b : {1, 2, 3}, c : {1, 2, 3}]
  /\ w = [{1, 2, 3} -> {1, 2, 3}]

Next ==
  \/ /\ x' = {3, 3, 2, 1}
     /\ UNCHANGED <<y, z, w>>
     /\ Print("Test 1", TRUE)
============================================

Introduce a TranformationListener for TrivialTypeFinder

Currently, TrivialTypeFinder is keeping type annotations that are given by the user. If an annotated expression is getting rewritten by another expression, TrivialTypeFinder does not propagate the type annotation for the new expression.

We have to introduce a TranformationListener that would listen to code transformations and propagate types.

NameStruc plugin

Clean up at.forsyte.apalache.tla.lir.plugins

It looks like the package is not used anymore. Delete.

Constant initializers are not being preprocessed

For example, expressions of the form C = 1 should automatically be transformed into C \in {1}, but they aren't.

Error reporting

When analysis plugins report errors about the source code, they must be reported consistenly, like in a Java/C/... compiler.

FAIL operator

Add a new operator FAIL(message) that is equivalent to ASSERT(FALSE, message). Use it to implement ASSERT.

Source code information is sometimes tracked incorrectly

As type checker is using SourceStore when reporting errors, we have to fix SpecHandler (or whatever unfolds the definitions) to properly track the source code. In the current version, the messages by the type checker are absolutely useless.

Extract the code transformations from *.tla.assignments.Transformer

The class at.forsyte.apalache.tla.assignments.Transformer contains several general-purpose code transformations that should be:

1. Decoupled from the assignments module.
2. Moved to the module tlair, e.g., to the package *.lir.transformers.standard.
3. Made independent from each other. That is, every transformation should be in a separate class and it should be well-documented. Every transformation also should take Map[String, TlaDecl] and return Map[String, TlaDecl]. Hence, we need a trait similar to Transformation, but defined for Map[String, TlaDecl].

Normal form for TLA+ operators

Handling LET-IN is tedious. Shall we introduce top-level operators instead?

For instance:

A(x) ==
  \E y \in S:
    LET z = x + y IN
      x * y * z

should become:

A_z(x, y) == x + y

A(x) ==
  \E y \in S:
    x * y * A_z(x, y)

tla-assignments have poor test coverage and many restrictions on code structure

This module will be given arbitrary code and it should not fail on it.

TlaExBuilder

Currently, one has to construct TLAEx objects using a variety of operators found in different classes, e.g., OperEx(TlaBoolOper.not, ...) and OperEx(TlaOper.eq, ...).

Let's add an object TlaExBuilder that contains handy constructors for all possible combinations of expressions in LIR.

Merge *.process.Renaming and transformations.VariableRenaming

Renaming variables in LET-IN

The new code that assigns names to the variables does not handle declarations inside LET-IN. For instance, see Paxos.tla.

Hand-coded IR Example: Byzantine RB

Output counterexamples in the TLC format

Rewrite SpecHandler

The code is hard to read, owing to abuse of anonymous lambdas. Similar to RecursiveProcessor it has to be rewritten or instantiated with concrete parameters.

Source code information in TLA+ expressions

We have to associate with every expression a pointer to the source code. I believe that can be done using IDs and databases that we designed some time ago.

Logging infrastructure

Use a standard library, e.g., a scala version of log4j, to log the operations at different levels

BoolType plugin

TlaEx.toString is too verbose

The current implementation of toString is producing unreadable output even on small expressions. It makes it impossible to use the output while debugging (see below). There must be a nice way to define various pretty printers in scala.

( OperEx: \cap,
    ( OperEx: {...},
        ( ValEx: TlaInt(1) , id:UID(-1) ),
        ( ValEx: TlaInt(3) , id:UID(-1) ),
      id: UID(-1)
    ),
    ( OperEx: {...},
        ( ValEx: TlaInt(3) , id:UID(-1) ),
        ( ValEx: TlaInt(4) , id:UID(-1) ),
      id: UID(-1)
    ),
  id: UID(-1)
)

Refactor *.assignments.transformations

Refactor EqualityAsContainment, Inline, LetInExplicit, Prime, Transformer, UnchangedExplicit, so they look like PrimePropagation

Cardinality comparisons

Introduce an optimization for the expressions: Cardinality(S) >= C and Cardinality <= C, where C is a constant.

Clean up at.forsyte.apalache.tla.lir.values

Remove the unused classes. Document the rest.

Clean up *.tla.lir.identifiers

There are lots of TODOs and deprecated methods

Finding assignments in CASE

The assignment solver does not look for assignments inside CASE expressions.

CASE  x = 0 -> x' = 1
   [] x = 1 -> x' = 2
   [] OTHER -> x' = 0 

Although we have not found case studies, where CASE is used like that, it should not be hard to add support for such assignments.

Remove TlaExDecorator and ToggleFlag

The purpose of these classes is not clear