Temporal properties and index out of bounds

31 views
Skip to first unread message

Isaac DeFrain

unread,
Feb 11, 2021, 4:58:50 PM2/11/21
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 PM2/11/21
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 PM2/17/21
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 PM2/17/21
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 PM2/26/21
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