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

*From*: szcze <akonsu@xxxxxxxxx>*Date*: Sat, 16 Dec 2023 20:54:38 -0800 (PST)

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/e08c0ea1-6424-42bb-9f92-01f5f20b272bn%40googlegroups.com.

**Follow-Ups**:

- Prev by Date:
**Re: [tlaplus] Re: Advent of TLA+** - Next by Date:
**[tlaplus] Re: need help with starting with writing a spec** - Previous by thread:
**Re: [tlaplus] Re: Advent of TLA+** - Next by thread:
**[tlaplus] Re: need help with starting with writing a spec** - Index(es):