Re: [tlaplus] Re: add fairness properties to a specification with PlusCal INSTANCEs

Hi David,

I reread some of Specifying Systems but found no explicit reference to fairness constraints SF_<v>(A) where A is more than just an action.

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.

So in the additional predicate can you only refer to the prestate?

SF_<v>((receiveDataQueue = <<CORRUPT_DATA>>) /\ dataWir!Next)

TLC runs with the above but what I want is to refer to the post state
SF_<v>((receiveDataQueue' = <<CORRUPT_DATA>>) /\ dataWir!Next)
with this TLC complains with unexpected runtime error
In evaluation, the identifier receiveDataQueue is either undefined or not an operator.

Try writing

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.

Regards,

Stephan

--
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.