Re: [tlaplus] Re: TLC crashes with "File too large" IOException while writing MC.st file

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

On 19.10.18 15:57, Nipun sehrawat wrote:
>
> Thanks for the reply!  The issue was indeed the filesystem - my spec
> is in a  version control system, which was probably placing the 512MB
> limit.  Is there a way to instruct TLC to create the model directory
> elsewhere?  I couldn't find such an option in 'preferences' or on
> https://lamport.azurewebsites.net/tla/tlc-options.html.

Hi Nipun,

you can set the TLC command-line parameter "-metadir /path/to/metadir"
on the advanced page of the model editor.

Hope this help,

Markus