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

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!

On Friday, October 19, 2018 at 2:09:07 PM UTC-7, loki der quaeler wrote:

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