# Learn TLA+ from PlusCal ## Metadata **Status**:: #x **Zettel**:: #zettel/fleeting **Created**:: [[2026-01-14]] ## Single Process ``` VARIABLES people, accounts, sender, receiver, amount, pc ``` Use `vars` to include all variables. ``` vars == << people, accounts, sender, receiver, amount, pc >> ``` Use `pc` to control the workflow. ``` Init == (* Global variables *) /\ people = {"alice", "bob"} /\ accounts = [p \in people |-> 5] /\ sender = "alice" /\ receiver = "bob" /\ amount \in 1..5 /\ pc = "Lbl_1" Lbl_1 == /\ pc = "Lbl_1" /\ TRUE /\ pc' = "Done" /\ UNCHANGED << people, accounts, sender, receiver, amount >> ``` Add `Terminating` for finite workflow. And ensure the algorithm is eventually terminated. ``` (* Allow infinite stuttering to prevent deadlock on termination. *) Terminating == pc = "Done" /\ UNCHANGED vars Next == Lbl_1 \/ Terminating Spec == Init /\ [][Next]_vars Termination == <>(pc = "Done") ``` ## Multiple Processes Multiple processes algorithm uses a function for `pc`. The key is the input argument to each `Process`. If there are multiple `Process` blocks, ensure their domain disjoints.