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

Re: [tlaplus] need help with starting with writing a spec



The grammars in the collection of standard examples [1] may be of interest to you. Note, however, that TLA+ may not be the most suitable language for specifying grammars and parsers.

Stephan

[1] https://github.com/tlaplus/Examples/tree/master/specifications/SpecifyingSystems/Syntax

On 17 Dec 2023, at 06:05, szcze <akonsu@xxxxxxxxx> wrote:

I want to add to what I said. I think that grammars for my parser should be modeled as sequences too. So I would need to give a specific grammar to the model as well and this would be even more limiting... Perhaps I do not understand how to specify something like this effectively... Please help.

суббота, 16 декабря 2023 г. в 23:54:38 UTC-5, szcze:
Hello, I am a beginner and I am only starting to learn the concepts. I need to write a specification for a parser, and as far as I understand the only way to model the input stream of tokens is by using sequences. That is, I have to give a specific sequence of tokens to my model and run the model on this sequence. But any such sequence limits the ability of TLA+ to enumerate all possibilities and help me find problems in my spec. I would have to give manually generate a set of possible inputs for my model and try them one by one, I think, to be able to "exercise" all possible behaviors. Is what I am saying correct? Would someone please comment on this and point me in the right direction?

--
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/b8ebd8a7-05a7-4301-814f-e3bd6a810d25n%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/9A58F885-884C-41C2-901E-9F016055C5FB%40gmail.com.