Transitions in TLA+ are atomic, as are groups of PlusCal statements in between two labels. Your approach of splitting assignments into two separate statements, using an auxiliary variable, is the idiomatic way of modeling non-atomic assignments.
Stephan I’m new to TLA+ and formal specs in general and I’m playing around with generating a spec for a simple lock-free concurrent data structure as a means to learn TLA+ & PlusCal. My question concerns non-atomic assignment and if there is an idiomatic way to specify that an assignment be non-atomic? The only thing I came up with was to split the assignment up with a temporary as in the following PlusCal snippet:
... shared_global_var_intermediate’ := new_val; label: shared_global_var’ := shared_global_val_intermediate; assert shared_global_var = new_val; ...
How do others handle this?
Thanks in advance!
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
|