You're viewing the readable version of this site. The interactive extras (search, diagrams, read-aloud) need JavaScript and a current browser. Enable JavaScript; if it is already enabled, update your browser.

Learn · All the Ways It Can Break

growing

Types Make the Symbolic World Finite Enough

Apalache must know the shape of a symbolic value before it can encode the question for a solver.

formal-methods, apalache, tla-plus, types, symbolic-model-checking, learn

You will install Apalache 0.61.0, annotate a state variable, run the type checker, and diagnose a deliberate type mismatch. Experienced readers will also separate language semantics, the supported checker fragment, and the solver encoding as three distinct boundaries.

Give the symbol a shape

Download the Apalache 0.61.0 binary distribution from its official release and place its bin directory on your path. Confirm the version, then type-check the capacity module:

apalache-mc version
apalache-mc typecheck Capacity.tla

If the shell cannot find apalache-mc, invoke the executable from the downloaded bin directory or repair that directory's PATH entry. If the reported version is not 0.61.0, stop and select the pinned distribution before interpreting output; a different tool version is a different evidence environment.

The load-bearing annotation sits immediately before the variable:

tla code/all-the-ways-it-can-break/symbolic-capacity/Capacity.tla#typed-state Capacity.tla The comment is semantic input to Apalache even though another TLA+ tool may treat it as an ordinary comment.

Diagnosis — classify the checker outcome before interpreting it.

Types constrain expressions, not runtime objects

Int describes every value used may take in the checked fragment. It does not allocate an integer object or impose the capacity bound. The invariant 0 < used /\ used <= Capacity= supplies that domain claim separately.

Sets, functions, records, tuples, variants, and operator arguments need shapes that the checker can determine. When inference becomes ambiguous, annotate the boundary rather than guessing which interpretation the solver received.

Three boundaries

TLA+ as a language is broader than one checker. Apalache supports a documented fragment and gives that fragment a symbolic encoding. The underlying solver then decides the resulting constraints within the requested bound. A valid TLA+ module may therefore be unsupported by Apalache, and an Apalache-typed module may still contain a false invariant. “Parses,” “type-checks,” and “holds” are three different observations.

Lessons

  • Symbolic encoding needs an unambiguous type for every relevant expression.
  • Type rejection produces no verification verdict.
  • Types describe value shapes; invariants express domain rules.
  • A language, a checker's supported fragment, and its encoding are distinct boundaries.
  • Version and type-check completion belong in the evidence record.

Practice

  1. Retrieval. Where does an Apalache variable annotation appear?
  2. Discrimination. Is used: Int enough to prove used > 0=?
  3. Transfer. Type a function from string job identifiers to integer retry counts.

Worked answers

  1. In an @type comment immediately before the declaration it annotates.
  2. No. Integers include negative values; an invariant or transition guard must exclude them.
  3. Str -> Int.

References

  1. Apalache team. Type annotations in Apalache. — typed TLA+ syntax and rationale
  2. Apalache team. Apalache 0.61.0 release. — the version used by this route

← Say Eventually Precisely Ask for the Whole Bounded Trace →