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

[loki der quaeler <qua...@xxxxxxxxx>]

Hi -

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

-loki

On Friday, October 19, 2018 at 12:35:50 PM UTC-7, Nipun sehrawat wrote:

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