I reread some of Specifying Systems but found no explicit reference to fairness constraints SF_<v>(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