TLA Plus

TLA Plus is specification language based on the Temporal Logic of Actions.

Example: 1 Bit Clock

State variable: $b$ Initial predicate: $b=0\lor b=1$ Next step action ($b^{\prime}$ is the variable at the next state; same as $\bigcirc b$)

VARIABLE b

Init == (b = 0) \/ (b = 1)

TypeInv == b \in {0, 1}

Spec == \/ b = 0 /\ b' = 1 \/ b = 1 /\ b' = 0

Spec == Init /\ [][Next]_<<b>>

THEOREM Spec => []TypeInv