formal methods – Is assignment atomic in Promela?

Is assignment atomic is Promela? That is, can concurrent

x = value1;


x = value2;

produce anything different from value1 or value2 ?

And can a concurrent execution of

x = expression1;


x = expression2;

produce anything else than the values of expression1 and expression2, executed atomically (especially if reading more than one variable in any of the expressions)?

I failed to find a clear, straight statement about this in , , or . The text says that the assignments are basic (i.e., without substatements), but does not say anything about the semantics of basic.

(PS. Of course, we know that, in the first place, Promela code is not meant to be actually executed, though printfs and translators to C exist; no question about that.)