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