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.RuntimeException
: Attempted to apply function:
( 0 :> -1 @@
1 :> 1 @@
2 :> 1 @@
--------
250 :> -1 @@
251 :> -1 @@
252 :> -1 @@
253 :> -1 @@
254 :> -1 @@
255 :> -1 @@
256 :> -1 )
to argument a, which is not in the domain of the function.
The error occurred when TLC was evaluating the nested
expressions at the following positions:
0. Line 95, column 10 to line 109, column 47 in bayermoore
1. Line 95, column 13 to line 95, column 24 in bayermoore
2. Line 96, column 13 to line 108, column 53 in bayermoore
3. Line 97, column 21 to line 105, column 29 in bayermoore
4. Line 97, column 24 to line 97, column 40 in bayermoore
5. Line 98, column 24 to line 98, column 37 in bayermoore
6. Line 99, column 24 to line 103, column 58 in bayermoore
7. Line 100, column 32 to line 101, column 41 in bayermoore
8. Line 100, column 35 to line 100, column 62 in bayermoore
9. Line 100, column 44 to line 100, column 62 in bayermoore
10. Line 6, column 13 to line 6, column 34 in bayermoore
11. Line 6, column 16 to line 6, column 20 in bayermoore
12. Line 6, column 20 to line 6, column 20 in bayermoore
13. Line 100, column 50 to line 100, column 61 in bayermoore
14. Line 100, column 54 to line 100, column 61 in bayermoore
Thanks.
Hello,you forgot to click on "set of model values" when instantiating the set "Character". Attached is the TLA+ module and a screenshot of how the instance should be displayed.TLC indicates an error when evaluating the _expression_ text[i+j] since both i and j may be 0. Please remember that TLA+ sequences are indexed from 1, not 0. But the instantiation works.Stephan