Requirement → TLA+ Property Generator

A requirement is a claim about behavior. A TLA+ property is the same claim, stated precisely enough to check. The translation is about finding the formal shape of an informal statement.

Step 1 — Classify: safety or liveness?

Safety = something bad never happens. Checkable at each state. Liveness = something good eventually happens. Needs fairness; checkable only over infinite traces.

Step 2 — Find the state predicate

Every property bottoms out in a predicate over state variables. Extract the nouns from the requirement; map them to VARIABLES.

Pattern catalog — NL → TLA+

Worked example

Requirement: "A write request must be replicated to a majority of nodes before it is acknowledged to the client."

Decompose:

• "A write request" → some r \in writes
• "replicated to N" → replicated[r] is a set of nodes, Cardinality(replicated[r]) >= ...
• "majority" → > Cardinality(Nodes) \div 2
• "before acknowledged" → if r \in acked then the replication condition holds. This is an ordering constraint on when acked can be set.

Property (safety — "never ack prematurely"):

Majority == Cardinality(Nodes) \div 2 + 1

SafeAck ==
  \A r \in acked :
    Cardinality(replicated[r]) >= Majority

Checkable as an invariant. If TLC finds a state where r \in acked but replicated[r] is a minority, the replication protocol is wrong.

Companion liveness — "every write does eventually get acked":

AckLiveness ==
  \A r \in writes : (r \in pending) ~> (r \in acked)

Needs fairness on the replication and ack actions to be checkable.

The precedence trap

"X before Y" is NOT X => <>Y. That says "if X, eventually Y" — nothing about order.

"X before Y" means: at the moment Y happens, X has already happened. In state terms: Y => (X has been true at some past point). TLA+ is forward-looking — past is awkward. Standard trick:

VARIABLE seen_X    \* history variable — not in the real system
Init == ... /\ seen_X = FALSE
Next == ... /\ seen_X' = (seen_X \/ X)   \* latches TRUE once X holds

Precedence == Y => seen_X

Do not

• Do not translate "eventually" without fairness. <>P is only checkable if Next has fairness — otherwise TLC says "yes, if I stutter forever P never happens, property violated." Add WF_vars(Action) for the action that achieves P.
• Do not write []<>P when you mean <>P. []<>P = "infinitely often P" (keeps happening). <>P = "at least once." Different requirements.
• Do not state liveness properties you can't check. TLC checks liveness but it's expensive. If your model is already at the state-space limit for safety, liveness won't finish.
• Do not let a requirement stay ambiguous. "The system is consistent" — consistent how? Push back for a precise statement before formalizing.

Output format

## Requirement (as given)
<verbatim>

## Classification
<safety | liveness | response | precedence>

## State mapping
<english noun> ↦ <TLA+ variable/expression>

## Property
<TLA+>

## Fairness needed (liveness only)
<WF/SF conditions — and why>

## Sanity check
<does the property trivially hold? is it vacuously true? — one sentence>