The program counter is an "implementation detail" of the specification and should not be observable by the environment. Therefore the "morally correct" representation of the high-level specification is the TLA formula \EE pc : A.
TLC doesn't check properties of this kind and what you did is write a "refinement mapping" that computes the program counter of the high-level spec from the state of the low-level spec. This is the standard way of proving B => \EE pc : A, but there are certain cases when refinement mappings do not exist even if the implication is valid, see .
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.