[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: mohan radhakrishnan <radhakrishnan.mohan@xxxxxxxxx>*Date*: Sun, 18 Dec 2022 20:54:31 -0800 (PST)*References*: <6c72f651-82f0-416c-b01f-744a7bef5662n@googlegroups.com> <ECAA9F9A-1BE6-4CB9-A832-56E384F2A9D8@gmail.com> <1d759b36-d03a-4bb3-a33a-7ba05d47914dn@googlegroups.com> <B34824F7-21B5-4757-9DB0-6655E72E42C7@gmail.com> <17c1a443-829b-4c81-8119-f4414211af8en@googlegroups.com> <405d1a39-1eca-451c-b85e-f11aa8cf5b41n@googlegroups.com> <11a602f5-3bef-4262-8645-765b6079e5fdn@googlegroups.com> <EC81EA75-9368-473C-A651-17347531F655@gmail.com>

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

On Sunday, December 18, 2022 at 1:50:53 PM UTC+5:30 Stephan Merz wrote:

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 likeCharacters <- {a,b,c} \* set of model valuestext <- << a, b, a, a, c >> \* ordinary valuepattern <- << a, a >> \* ordinary valueConcerning 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.StephanOn 18 Dec 2022, at 05:21, mohan radhakrishnan <radhakris...@xxxxxxxxx> wrote: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,MohanWhat do you mean that the algorithm is "wrong"?I am able to usestruct == [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

On Friday, December 16, 2022 at 4:13:01 PM UTC+5:30 Stephan Merz wrote:Please see https://github.com/tlaplus/tlaplus/issues/512.But I believe that for your application, using an abstract set of characters is preferable.StephanOn 16 Dec 2022, at 11:11, mohan radhakrishnan <radhakris...@xxxxxxxxx> wrote:Hello,I experimented with the changes and they work but the functionAscii(char) == 96 +

CHOOSEz \in 1 .. 26 :"abcdefghijklmnopqrstuvwxyz"[z] = charthrows 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,MohanOn Thursday, December 15, 2022 at 1:30:33 PM UTC+5:30 Stephan Merz wrote: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, patternASSUME 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 valuestext <- << 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 likedefine {\* sequences of characters of length at most nCharSeq(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,StephanOn 15 Dec 2022, at 05:53, mohan radhakrishnan <radhakris...@xxxxxxxxx> wrote:Hello,I was looking for functions to get the ASCII value of characters but realized I couldn'tfind 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-algorithmCan 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--

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...@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/6c72f651-82f0-416c-b01f-744a7bef5662n%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+u...@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/1d759b36-d03a-4bb3-a33a-7ba05d47914dn%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+u...@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/11a602f5-3bef-4262-8645-765b6079e5fdn%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/8d453cbb-7202-4d1d-83ec-1cd9057529d7n%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Functions in the standard libraries***From:*Stephan Merz

**References**:**[tlaplus] Functions in the standard libraries***From:*mohan radhakrishnan

**Re: [tlaplus] Functions in the standard libraries***From:*Stephan Merz

**Re: [tlaplus] Functions in the standard libraries***From:*mohan radhakrishnan

**Re: [tlaplus] Functions in the standard libraries***From:*Stephan Merz

**Re: [tlaplus] Functions in the standard libraries***From:*mohan radhakrishnan

**Re: [tlaplus] Functions in the standard libraries***From:*Andrew Helwer

**Re: [tlaplus] Functions in the standard libraries***From:*mohan radhakrishnan

**Re: [tlaplus] Functions in the standard libraries***From:*Stephan Merz

- Prev by Date:
**[tlaplus] Converting TLA+ spec to PlusCal** - Next by Date:
**Re: [tlaplus] Functions in the standard libraries** - Previous by thread:
**Re: [tlaplus] Functions in the standard libraries** - Next by thread:
**Re: [tlaplus] Functions in the standard libraries** - Index(es):