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
Regards,
Alon