

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

I was hoping there was another technique though, to more or less “ignore” `pc` in the temporal property checking. 
There's existential hiding (section 4.3 of Specifying Systems), but I don't believe TLC is currently able to check it.
