Re: [tlaplus] Symmetry sets

[Jay Parlar <parlar@xxxxxxxxx>]

A TypeOK invariant would work great. And it would have the added benefit of throwing an error at the exact step in which the set is no longer satisfying the invariant, rather than waiting for the CHOOSE to take place. 

This will make it much easier to track down _why_ things went awry. 

The only reason I see that an invariant wouldn’t be feasible is if the set in question is not one of your variables. If it’s some computer value, then you’d need to use an assert. 

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.