[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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.