[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: "tlapl...@xxxxxxxxxxx" <tlapl...@xxxxxxxxxxx>*Date*: Tue, 11 Nov 2014 11:32:33 +0100*References*: <27780607-9e0a-4101-92fa-ccbb15043611@googlegroups.com> <f345cda2-414f-4b03-a7eb-b18d6889273f@googlegroups.com> <bdad52a1-62e2-4c23-a6b1-1086ade770f1@googlegroups.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.2.0

On 10.11.2014 20:13, chris...@xxxxxxxxx wrote: > I cannot reproduce this problem. More specifically, I can run TLC on > the module attached to this message. Concretely, I instantiated M > and N by 42 and 24 and told TLC to verify the invariants Inv and > PartialCorrectness. As expected, TLC complains that it cannot > enumerate Int, so I have to override the definition of Int (in > Advanced Options -> Definition Override), for example by the > interval -100 .. 100. > > > I give up. Your modules model check just fine. My euclid module, which > is almost identical to yours, simply refuses to. I guess there must be > something screwy in my environment. I tried literally copying the > contents of your files into mine, running a model check and it still > won't run. Hi Chris, can you share the disk content¹ of your spec/model including the nested *.toolbox directory? Then I can (locally) debug why TLC won't run on it. Cheers Markus ¹ The path is shown at the top of the spec editor.

**Follow-Ups**:**Re: [tlaplus] Re: Proofs of integer properties***From:*chris . . .

**References**:**Proofs of integer properties***From:*chris . . .

**Re: Proofs of integer properties***From:*Stephan Merz

**Re: Proofs of integer properties***From:*chris . . .

- Prev by Date:
**Re: Proofs of integer properties** - Next by Date:
**Re: Why Amazon Chose TLA+** - Previous by thread:
**Re: Proofs of integer properties** - Next by thread:
**Re: [tlaplus] Re: Proofs of integer properties** - Index(es):