TLA+-Guided Code Repair

Specialization of → model-guided-code-repair for TLC. The general loop is the same; this skill covers the TLC-specific mechanics: reading error traces, understanding action enablement, and the .cfg levers.

Reading a TLC error trace

TLC prints the trace as numbered states. Between states, it names which Next disjunct fired: