[tlaplus] Re: When to use TLA+.

[Ron Pressler <ron.pressler@xxxxxxxxx>]

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.