Re: [tlaplus] Re: Proofs of integer properties

["tlapl...@xxxxxxxxxxx" <tlapl...@xxxxxxxxxxx>]

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.