[tlaplus] checking that a pluscal spec implements another pluscal spec

[jack malkovick <sillymouse333@xxxxxxxxx>]

Hello! I have a question and I think it's not possible, but I'll give it a try.

Let's say I want to check that spec that refines another spec. The variables that they have in common should be the same (considering stuttering invariance of course). But they are both generated by PlusCal and they have a `pc` variable that clearly does not correspond state by state.

Can I somehow check that RefinedSpec => GeneralSpec ignoring that common `pc` variable?

-- 
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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/621083e7-5318-4ef6-8fce-fb725ccf806an%40googlegroups.com.