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

[tlaplus] Dealing with a `pc` variable in refinement?

I've only recently started playing with refinement between specs, checking that one spec implies another. For illustrative purposes, we'll say the refinement is `THEOREM B => A`

An early stumbling block I ran into was when I had a `pc` variable that appears in both specs. 

B introduces "extra" states, but they only modify variables that don't appear in A. That would normally be fine, except that it causes `pc` to not match.

Is there a right way to more or less ignore a `pc` variable when checking if one spec refines another? I feel like there's a super obvious answer to this, but it's not coming to me.

Jay P.

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.