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

[david streader <davidistreader@xxxxxxxxx>]

Sorry to be so slow.  

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

many thanks david

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