Dear inevity,
the best way to understand the atomicity of TLA actions from PlusCal is to translate the PlusCal code and see the output.
Each label is associated with a variable that changes from one PlusCal step to the next.
Assignments and transactions in PlusCal will be transpiled into the specific TLA+ description, which is quite different from
what one might expect from a programming language.
Each action is atomic and simply describes the current state (unprimed) and the next state (primed).
E.g.
Action == var1 = 1 /\ var2 = "label 1" /\ var3 = "content1" /\
var1' = var1 + 2 /\ var2 = "label 2" /\ var3' = "next content"
Remember, each "=" is not an assignment, just a description. Whenever "Action" happens, the system is in the state
described by
var1 = 1 /\ var2 = "label 1" /\ var3 = "content1" and the next state of the variables is
var1' = var1 + 2 /\ var2 = "label 2" /\ var3' = "next content" . In the next state var1' becomes var1 etc.
This is how atomicity is modeled.
In addition: concurrency is modeled serially, but with the possibility of non-determinism to model random order of operations.
I hope this could answer your question.
Kind regards
Andreas