When to use TLA+.

[MK Bug]

Hi,

If I want to achieve "Input Validation" of a model, like a constant must contains "Some" or is of specific type. So is it achievable by using TLA+ language in TLC.

If it is then can you please share how? just an overview.

If not then what is the best way to do it?

Regards,

Malaika

[Ron Pressler]

Try using the ASSUME construct. E.g:

    CONSTANT N

    ASSUME N \in Nat /\ n > 10

[MK Bug]

Thanks for the response.

But actually my code is like

For example:

Constant Z     /* constant contains Z = 'Name.com' and i want to check that every time Z has some value this must contains Dot .

Any type of help is appreciated 

--
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/183880c2-e0e8-4c7b-b17e-6af303d8d79a%40googlegroups.com.

[Martin]

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

> To view this discussion on the web visit
> https://groups.google.com/d/msgid/tlaplus/183880c2-e0e8-4c7b-b17e-6af303d8d79a%40googlegroups.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>.