Re: [tlaplus] ArrayIndexOutOfBoundsException

[Markus Alexander Kuppe <tlaplus-go...@xxxxxxxxxxx>]

On 10.09.2017 15:29, Alon Be wrote:
> I have a funny bug, 
> I can't post the whole code right now, but I could tomorrow if need be.
> 
> I wrote this function :
> 
> VectorToSet(V,size) == { V[i] : i \in 1 .. size }
> 
> And kept on receiving an index out of bounds exception, when calling it
> with parameters: (<<{7},{6},{5}>>, 3).
> To debug, I changed the implementation to:
> 
> VectorToSet(V,size) == { V[i] : i \in 1..Print(<<"in VectorToSet,
> V=",V>>,size) }
> 
> And suddenly - no bugs!
> I am clueless.
> I would love it if anyone here could explain what is going on.
> 
> This is the error message:
> 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
> : 1

Hi Alon,

can you (privately) send me the full spec? I cannot reproduce the bug
locally.

By the way, you can get rid of the size parameter by using the Len
operator from the Sequences standard module or - without Sequences - the
built-in DOMAIN operator.

Thanks
Markus