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

[Hillel Wayne <hwayne@xxxxxxxxx>]

Are you writing two pluscal specs? PlusCal isn't really that great for doing refinements. Your best bet is to define an operator that maps values of B!pc to A!pc, and then do INSTANCE A WITH pc <- Op(pc). I'll try to whip up a short demo tonight.

H

On 5/1/19 4:34 PM, Jay Parlar wrote:

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.

Thanks,

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.

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