Functions in the standard libraries

[mohan radhakrishnan]

Hello,

           I was looking for functions to get the ASCII value of characters but realized I couldn't

find a list of all functions available. Should I look for a facility to add my own functions ?

I posted the code in https://stackoverflow.com/questions/74801070/syntax-errors-in-pluscal-code-for-bayermoore-algorithm

Can I check if the code returns the correct value before checking the model and state spaces ? The state space for this is enormous anyway.

Thanks,

Mohan

[Stephan Merz]

Hello,

please check Section 16.1.10 of Specifying Systems, which discusses strings and characters and even contains a function to convert lower-case letters to ASCII. In short, TLA+ has no hardwired definition of what characters are. In your representation, the variables in_pattern and in_text are sequences of strings, not characters.

As far as I can tell, the algorithm is independent of any concrete representation of characters. I suggest that you make the set of characters as well as the inputs to the algorithm parameters of your specification, i.e. introduce (at the top of the module)

CONSTANT Character, text, pattern

ASSUME text \in Seq(Character) /\ pattern \in Seq(Character)

When you use TLC to check your algorithm, you can instantiate these constants by concrete values, e.g.

Character <- {a,b,c}  \* a set of model values

text <- << a, a, b, a, c >>

pattern <- << b, a >>

In this way, you'll also alleviate the effect of state explosion. If you want to go further than testing the algorithm on concrete inputs, you can replace the parameters `text' and `pattern' by variables and nondeterministically assign them finite (bounded-length) sequences of characters by writing something like

define {

  \* sequences of characters of length at most n

  CharSeq(n) == UNION { [1 .. k -> Character] : k \in 0 .. n }

}

[...]

variables text \in CharSeq(5), pattern \in CharSeq(3);

[...]

In this way, TLC will check the algorithm for all text / pattern strings of bounded length.

Remember that TLA+ is a language for specifying algorithms at a high level of abstraction, not a programming language. 

Hope this helps,

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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/6c72f651-82f0-416c-b01f-744a7bef5662n%40googlegroups.com.

[mohan radhakrishnan]

Hello,

             I experimented with the changes and they work but the function

Ascii(char) == 96 + CHOOSE z \in 1 .. 26 :"abcdefghijklmnopqrstuvwxyz"[z] = char

throws this. I have converted the code in the book to Pluscal. Is that wrong ?

The exception was a java.lang.RuntimeException

: A non-function (a string) was applied as a function.

Thanks,

Mohan

[Stephan Merz]

Please see https://github.com/tlaplus/tlaplus/issues/512.

But I believe that for your application, using an abstract set of characters is preferable.

Stephan

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/1d759b36-d03a-4bb3-a33a-7ba05d47914dn%40googlegroups.com.

[mohan radhakrishnan]

I am able to use 

struct == [a |-> 97, b |-> 98, c |-> 99]

and a small subset to complete the model check phase. States are less in number now. But the code is very convoluted.

I believe you meant that this is what abstraction means ? The Pluscal code will be quite complex if I try to code the entire program

which isn't our goal. But. I have a question. If the Pluscal code isn't complete(in this case), the algorithm is wrong and the model

checker still completes. What does it mean for the specification ? How do I interpret that state ?

Thanks,

Mohan

[Andrew Helwer]

What do you mean that the algorithm is "wrong"?

[mohan radhakrishnan]

I mean that the Pluscal isn't coded very well because the language doesn't seem to be expressive like Java.

Attempts to code an entire algorithm is discouraged. I guess.

TLA is what I should be using. That is more. powerful. I am just beginning.

Thanks,

Mohan

[Stephan Merz]

Can you explain what `struct' represents? Assuming the module pasted on StackOverflow is the one you are currently working with, I don't understand why you compare struct[pattern[j+1]] and struct[text[i + j]] rather than just comparing pattern[j+1] and text[i+j], as in the Java version of the algorithm.

What values did you choose for instantiating the constant parameters in your model? I suggest you use something like

Characters <- {a,b,c}  \* set of model values

text <- << a, b, a, a, c >>  \* ordinary value

pattern <- << a, a >>   \* ordinary value

Concerning expressiveness, PlusCal and TLA+ expressions are the same, and PlusCal should certainly be powerful enough to represent the algorithm. Both languages are way more expressive than Java, in a mathematical sense.

Stephan

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/11a602f5-3bef-4262-8645-765b6079e5fdn%40googlegroups.com.

[mohan radhakrishnan]

Characters <- {a,b,c}  \* set of model values

text <- << a, b, a, a, c >>  \* ordinary value

pattern <- << a, a >>   \* ordinary value

This shows an error for all the values . (e.g)  Unknown operator : 'b'. The UI shows a small popup and a miniscule red square in the section "What is the model?"

So I used double quotes and the struct holds ASCII values.

I also think I have not used the FP constructs or support for Math in Pluscal. So it looked like it supports only imperative styles.

Thanks,

Mohan

[Stephan Merz]

Don't use quotes, just abstract (i.e., model) values.

Stephan

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8d453cbb-7202-4d1d-83ec-1cd9057529d7n%40googlegroups.com.

[mohan radhakrishnan]

Hello,

            This screenshot shows the error. The model wouldn't execute if I don't use double quotes.

Thanks,

Mohan

[Stephan Merz]

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

[mohan radhakrishnan]

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.

[Stephan Merz]

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

--
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/eeb46b71-9813-45e7-a7a6-cedd7f443b91n%40googlegroups.com.