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

Re: [tlaplus] Re: Proofs of integer properties

On 12.11.2014 00:28, chris...@xxxxxxxxx wrote:
>     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.

Hi Chris,

all four Euclid models can be successfully checked with TLC here. The
only parts I had to adapt are the mappings to TLAPS' standard modules
(I'm on Linux).
Is there anything helpful in the .log file located in the Toolbox's
installation directory under workspace/.metadata/?