Hello TLA+ community,
I'm using the command-line version of TLC to check a model with temporal properties and came across this strange error:
Error: 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.lang.ArrayIndexOutOfBoundsException
: Index -574397211 out of bounds for length 1573086437
To give some context, the model I'm checking has been checked exhaustively (with no errors found) for smaller values of the constants. I only increased the constant values and TLC returned the above error. Has anyone else run into this phenomenon? Any anecdotes or insights would be greatly appreciated. Also, what is meant by the "User Output or TLC Console" in this context? I understand what this means when using the toolbox, but not when using the command-line.
Thanks in advance!
Best,