Hi Malaika,
You have been asking questions around specifying particular strings in different
ways. Certainly, using the representation of a string as sequence of codes
allows you to do it. I'm just asking myself if you are working on the right
abstraction level - TLA+ really shines when you want to prove temporal
properties of distributed algorithms. But for example, when you want to show
that a server eventually hands out an ID to everyone who asks for it, it is not
important how the ID actually looks like, only that is unique per client.
If you are interested in what happens with an invalid name, you could just say
that your names can be partitioned into valid and invalid names (where obviously
no name is both valid and invalid):
CONSTANT ValidNames, InvalidNames
ASSUME ValidNames \cap InvalidNames = {} (* those tw *)
Names == ValidNames \cup InvalidNames
In general, you might want to think about what properties you would like to
check about your specification and write your specification with that level of
detail in mind.
cheers,
Martin
> <mailto:
tlaplus+u...@googlegroups.com>.
> <
https://groups.google.com/d/msgid/tlaplus/183880c2-e0e8-4c7b-b17e-6af303d8d79a%40googlegroups.com?utm_medium=email&utm_source=footer>.
>
> --
> 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
> <mailto:
tlaplus+u...@googlegroups.com>.
> To view this discussion on the web visit
>
https://groups.google.com/d/msgid/tlaplus/CA%2BkanULEQU2qsW%2Bq-uV5j%3DcmpR3d8sy5mk6rY-mXPvRY6R5XXg%40mail.gmail.com
> <
https://groups.google.com/d/msgid/tlaplus/CA%2BkanULEQU2qsW%2Bq-uV5j%3DcmpR3d8sy5mk6rY-mXPvRY6R5XXg%40mail.gmail.com?utm_medium=email&utm_source=footer>.