1. Overview
  2. Tutorials
  3. 1. Overview
  4. 2. Entry-level Model Checker Tutorial
  5. 3. Type Checker Tutorial
  6. 4. Checking Pluscal specifications
  7. 5. Apalache trail tips: how to check your specs faster
  8. 6. Symbolic Model Checking
  9. 7. Specifying temporal properties and understanding counterexamples
  10. Apalache User Manual
  11. 8. Getting Started
    1. 8.1. Installation
      1. 8.1.1. Prebuilt Packages
      2. 8.1.2. Docker
      3. 8.1.3. Build from Source
    2. 8.2. Running the Tool
    3. 8.3. An Example TLA+ Specification
    4. 8.4. Specification Parameters
    5. 8.5. Symbolic Model Checking with Apalache
      1. 8.5.1. Assignments and symbolic transitions
      2. 8.5.2. Folding sets and sequences
      3. 8.5.3. Invariants: State, Action, Trace
      4. 8.5.4. Enumeration of counterexamples
      5. 8.5.5. The Apalache Module
      6. 8.5.6. Naturals
    6. 8.6. Apalache global configuration file
    7. 8.7. TLA+ Execution Statistics
    8. 8.8. Profiling Your Specification
    9. 8.9. Five minutes of theory
  12. 9. TLC Configuration Files
  13. 10. The Snowcat Type Checker
  14. 11. Supported Features
  15. 12. Obsolete: Recursive operators and functions
  16. 13. Known Issues
  17. 14. Antipatterns
  18. 15. TLA+ Preprocessing
  19. 16. Fine Tuning
  20. 17. Assignments and Symbolic Transitions in Depth
  21. 18. KerA: kernel logic of actions
  22. HOWTOs
  23. 19. Overview
  24. 20. How to write type annotations
  25. 21. How to use uninterpreted types
  26. TLA+ Language Manual for Engineers
  27. 22. Introduction
  28. 23. The standard operators of TLA+
    1. 23.1. Booleans
    2. 23.2. Control And Nondeterminism
    3. 23.3. Conditionals
    4. 23.4. Integers
    5. 23.5. Sets
    6. 23.6. Logic
    7. 23.7. Functions
    8. 23.8. Records
    9. 23.9. Tuples
    10. 23.10. Sequences
    11. 23.11. Bags
  29. 24. User-defined operators
    1. 24.1. Top-level operator definitions
    2. 24.2. LET-IN definitions
    3. 24.3. Higher-order operators definitions
    4. 24.4. Anonymous operator definitions
    5. 24.5. Local operator definitions
  30. 25. Apalache operators
  31. 26. Modules, Extends, and Instances
  32. Idiomatic TLA+
  33. 27. Introduction
  34. 28. Keep state variables to the minimum
  35. 29. Update state variables with assignments
  36. 30. Apply primes only to state variables
  37. 31. Use Boolean operators in actions, not IF-THEN-ELSE
  38. 32. Avoid sets of mixed records
  39. Design Documents
  40. 33. ADR-002: types and type annotations
  41. 34. ADR-003: transition executor (TRex)
  42. 35. ADR-004: code annotations
  43. 36. ADR-005: JSON Serialization Format
  44. 37. RFC-006: unit tests and property-based tests
  45. 38. ADR-007: restructuring
  46. 39. ADR-008: exceptions
  47. 40. ADR-009: outputs
  48. 41. ADR-011: alternative SMT encoding using arrays
  49. 42. ADR-015: ITF: informal trace format
  50. 43. ADR-016: ReTLA: Relational TLA
  51. 44. PDR-017: Checking temporal properties
  52. 45. ADR-018: Inlining in Apalache
  53. 46. ADR-020: Improving membership in arenas

Apalache Documentation

Anonymous operator definitions

work in progress...

[Back to user operators]