TLC crashes with "File too large" IOException while writing MC.st file

[Nipun sehrawat]

Hello,

I am running into TLC crashes, especially when checking for some liveness properties.  The error reported by TLC is:

TLC threw an unexpected exception.

This was probably caused by an error in the spec or model.

See the User Output or TLC Console for clues to what happened.

The exception was a java.io.IOException

: File too large

The error occurred when TLC was evaluating the nested

expressions at the following positions:

    The error call stack is empty.

TLC threw an unexpected exception.

This was probably caused by an error in the spec or model.

See the User Output or TLC Console for clues to what happened.

The exception was a java.io.IOException

: File too large

I debugged a bit and found that TLC crashes right after MC.st file crosses 512MB in size.  I have disabled checkpoints and snapshots but that didn't help.  Any ideas how to fix/avoid these crashes?

Thanks,

Nipun

[loki der quaeler]

Hi -

What OS are you on, and what filesystem is being used? (Also, the usual version questions for Java and the TLA+ Toolbox.)

-loki

[Nipun sehrawat]

Hi Loki,

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.

Thanks a lot!

[Markus Kuppe]

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