Principles of Symbolic Model Checking with Apalache

In order to take advantage of Apalache’s symbolic model checking, there are a few principles one must bear in mind when writing TLA.

Note that Apalache requires type annotations. Check the Snowcat tutorial and HOWTO on annotations.

Topics:

• Assignments and symbolic transitions
• Folding sets and sequences
• Invariants: State, Action, Trace
• Enumeration of counterexamples
• The Apalache Module
• Naturals module