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

[tlaplus] Model Checking Specs having Nat

Hi everyone,

I have 2 questions that I would be really grateful if you kindly helped me.

1- What is a convenient way of model checking a spec that has a variable that belongs to Nat?

2- How do I specify an action that is probabilistic? For example, I need to specify a an action that represents tossing a coin which will result in either a heads or a tails.

Thanks in advance.


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/CAKxfy0uEC9pQXReo6qyTbQKw59EWMSZo%3DwO8Wjn%2BFCGdowy29g%40mail.gmail.com.