Temporal properties and index out of bounds

21 views
Skip to first unread message

Isaac DeFrain

unread,
Feb 11, 2021, 4:58:50 PMFeb 11
to tla...@googlegroups.com
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,

Isaac DeFrain

Isaac DeFrain

unread,
Feb 11, 2021, 9:02:33 PMFeb 11
to tla...@googlegroups.com
Here's the TLC output for this error.


Best,

Isaac DeFrain

index_out_of_bounds.txt

Markus Kuppe

unread,
Feb 17, 2021, 12:35:04 PMFeb 17
to tla...@googlegroups.com
On 11.02.21 18:02, Isaac DeFrain wrote:
> Here's the TLC output for this error.

Thanks, the issue will be tracked at
https://github.com/tlaplus/tlaplus/issues/585

Markus

Isaac DeFrain

unread,
Feb 17, 2021, 2:13:23 PMFeb 17
to tla...@googlegroups.com
Great! Thanks, Markus.

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/1f45f451-2654-9c58-485a-680954627568%40lemmster.de.
--
Isaac DeFrain

pfeod...@gmail.com

unread,
Feb 26, 2021, 10:06:23 PMFeb 26
to tlaplus
Hi Isaac o/

 Can you run TLC from the command-line with the `-debug` flag set? Maybe you will have a more descriptive error output.

Thanks

Reply all
Reply to author
Forward
0 new messages