PlusCal uses labels (e.g. "Give:") to designate atomic actions - when you translate it, each labelled section is turned into an atomic action [1]. You can start

PlusCal uses labels (e.g. "Give:") to designate atomic actions - when you translate it, each labelled section is turned into an atomic action [1]. You can start off with a very simple spec with totally atomic transactions, and gradually make it more granular by introducing more labels, as shown in Wayne's Strange Loop presentation [2] [1] https://learntla.com/concurrency/labels/ https://learntla.com/concurrency/labels/ [2] https://youtu.be/_9B__0S21y8?t=955 https://youtu.be/_9B__0S21y8?t=955 (15:55)