Re: [tlaplus] Re: When to use TLA+.

[MK Bug <android.ruba@xxxxxxxxx>]

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 

On Thu, Jul 25, 2019, 6:38 PM Ron Pressler <ron.pressler@xxxxxxxxx> wrote:

Try using the ASSUME construct. E.g:

    CONSTANT N

    ASSUME N \in Nat /\ n > 10

On Friday, July 5, 2019 at 10:59:04 AM UTC+1, MK Bug wrote:

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

--
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/183880c2-e0e8-4c7b-b17e-6af303d8d79a%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/CA%2BkanULEQU2qsW%2Bq-uV5j%3DcmpR3d8sy5mk6rY-mXPvRY6R5XXg%40mail.gmail.com.