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.
Attachment:
euclid_pluscal.zip
Description: Zip archive