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

*From*: chris...@xxxxxxxxx*Date*: Tue, 11 Nov 2014 15:28:00 -0800 (PST)*Cc*: tlapl...@xxxxxxxxxxx*References*: <27780607-9e0a-4101-92fa-ccbb15043611@googlegroups.com> <f345cda2-414f-4b03-a7eb-b18d6889273f@googlegroups.com> <bdad52a1-62e2-4c23-a6b1-1086ade770f1@googlegroups.com> <5461E5C1.6090604@lemmster.de>

On Tuesday, November 11, 2014 3:20:55 AM UTC-8, tlap...@xxxxxxxxxxx wrote:

On 10.11.2014 20:13, chri...@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.

Attached.

**Attachment:
euclid_pluscal.zip**

**Follow-Ups**:**Re: [tlaplus] Re: Proofs of integer properties***From:*Markus Alexander Kuppe

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

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

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

**Re: [tlaplus] Re: Proofs of integer properties***From:*tlapl...@xxxxxxxxxxx

- Prev by Date:
**Re: Proofs of integer properties** - Next by Date:
**Temporal logic** - Previous by thread:
**Re: [tlaplus] Re: Proofs of integer properties** - Next by thread:
**Re: [tlaplus] Re: Proofs of integer properties** - Index(es):