I would suspect that the problem is due to certain operators that appear in your proof obligation. Would it be possible for you to send me the problematic spec (possibly by private email)?
I'm trying to prove a lemma with TLAPS.But, I get an error message (see the attached picture)
For information, the lemma used a predicate composed of a disjunction of several formulas. When I comment some formulas of this disjunction, TLAPS succeeds to prove the lemma. Otherwise, I have the error message.
Is this due to the size of my predicate?
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+u...@xxxxxxxxxxxxxxxx
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx
Visit this group at https://groups.google.com/group/tlaplus
For more options, visit https://groups.google.com/d/optout