Re: [tlaplus] Functions in the standard libraries

Since Character is now a parameter rather than containing fixed char codes between 0 and 256, the variable flag must now be a function with domain Character. You want to modify its initialization to

flag = [g \in Character |-> -1];

Also, in the initial loop, the instruction flag[i] := 1 should certainly be flag[p] := 1 (as it indeed was in your initial version of the PlusCal algorithm).

Please do not rely on members of this Google group for debugging errors in your specification.

Stephan

On 19 Dec 2022, at 10:39, mohan radhakrishnan <radhakrishnan.mohan@xxxxxxxxx> wrote:

Thank you. I understood how to initialize properly.

But the attached code throws an error like this. The code I posted to SO didn't have this issue.

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.

On Monday, December 19, 2022 at 2:28:03 PM UTC+5:30 Stephan Merz wrote:
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

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/eeb46b71-9813-45e7-a7a6-cedd7f443b91n%40googlegroups.com.

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/B97FBBAA-78D3-435A-BA81-1F59DE9EEDE6%40gmail.com.