TLA+ Starters #

These files are meant to feel as close as possible to a lightweight TLA+ “REPL”:

• keep the model tiny
• add one property at a time
• run TLC quickly
• inspect the trace

Files #

• Relation.tla
• Relation.cfg
• RelationStatus.tla
• RelationStatus.cfg
• A08Hold.tla
• A08Hold.cfg
• A08FailureWorkbook.md
• A08HoldWithEpoch.tla
• A08HoldWithEpoch.cfg
• A08HoldWithEpochBug.tla
• A08HoldWithEpochBug.cfg
• A09Schedule.tla
• A09Schedule.cfg
• A09FailureWorkbook.md
• I02Lease.tla
• I02Lease.cfg
• I02FailureWorkbook.md
• I15Fleet.tla
• I15Fleet.cfg
• I15FailureWorkbook.md

Fast Loop #

1. Start with the tiny model:
   • Users = {A, B}
2. Add one invariant or helper definition.
3. Run TLC.
4. If the invariant fails, read the counterexample trace.
5. Change one thing and rerun.

That is the closest practical workflow to a TLA+ REPL.

Good beginner moves #

1. Add a new invariant #

Examples:

• no blocked + active edge at the same time
• no pending edge after accept without explicit transition
• reverse index count matches truth

2. Add one new action #

Examples:

• Block(u, v)
• AcceptInvite(u, v)
• RejectInvite(u, v)

Then rerun TLC.

3. Intentionally add a bug #

For example:

• allow Remove(u, v) even when edge is absent
• allow self-edge insertion
• forget a guard on a status transition

Then let TLC show the bad trace.

Suggested progression for A02 Relation / Edge #

1. set-based follow/unfollow
2. add status map: Pending, Active, Blocked
3. add derived count view
4. add projector lag/refinement idea

The new status-based starter does step 2.

Good expressions to evaluate in the debug console:

rel
EdgeStatus(A, B)
ActiveFollowers(B)
PendingFollowers(B)
BlockedFollowers(B)
CountActiveFollowers(B)

Suggested progression for A08 Time-Bounded Exclusive Allocation #

1. one resource, one hold, one booking truth
2. add time ticks and expiry
3. add confirm vs expire race
4. add stale actor / epoch
5. add browse/projection lag as a refinement layer

The new A08Hold starter covers steps 1 to 3.

Good expressions to evaluate in the debug console:

holdStatus
holdOwner
holdEpoch
now
holdExpiresAt
inventoryStatus

Running TLC #

Use either:

• TLA+ Toolbox
• command-line TLC if installed locally

Typical command-line shape:

tlc tla/Relation.tla

If your local setup expects a config file explicitly:

tlc -config tla/Relation.cfg tla/Relation.tla

The exact command depends on how TLC is installed on your machine.

Local Helpers In This Repo #

From the repo root you can now use:

./run-tla.sh A08Hold
./run-tla.sh A09Schedule
./run-tla.sh I02Lease
./run-tla.sh I15Fleet

Or with make:

make tla SPEC=A08Hold
make tla SPEC=A09Schedule
make tla SPEC=I02Lease
make tla SPEC=I15Fleet

Shortcuts:

make tla-a08
make tla-a09
make tla-i02
make tla-i15