[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Temporal properties and index out of bounds

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!


Isaac DeFrain

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAM3xQxHFnRgEUvoLCYRmo0d-CAgfUWpypoebWyNBS%3DhGFzLv8g%40mail.gmail.com.