Re: [tlaplus] Re: Proofs of integer properties

[Markus Alexander Kuppe <tlaplus-go...@xxxxxxxxxxx>]

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/?

Markus