Re: [tlaplus] Problem with TLAPM

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)?

On 1 Feb 2017, at 16:34, Amira Methni <methni...@xxxxxxxxx> wrote:

Hi,

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?

Thank you,
Amira

--
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.
<error.PNG>