in TLA+ jargon, "an action" means "an action formula", that is, a formula containing primed and unprimed variables (but no temporal operators). It does not just refer to operators that define action formulas.
SF_v(dataWir!Next /\ receiveDataQueue' = << CORRUPT_DATA >>)
Of course, the two formulas are logically equivalent, but TLC evaluates expressions from left to right, and it's the action dataWir!Next that "assigns" the next-state value to the variable receiveDataQueue.
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+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.