Hello,
TLC is restricted to verifying finite-state instances. For a variable x that takes natural numbers as its values, you can verify this by writing x \in Nat, say in an invariant. For an action that takes a natural number parameter, say
Increment == \E k \in Nat : x' = x+k
you get unbounded non-determinism that TLC cannot handle. You can however perform incomplete verification by overriding Nat by a finite set, say, 0 .. 10 (see Spec Options -> Definition Override in the Toolbox). However, watch out for interactions: for example, overriding Nat by 0 .. 10 will also apply to the invariant x \in Nat, which may then no longer hold (if the initial value of x is 5, for example), so you may want to use different sets for different purposes. Also, for a variable that may take unboundedly many values (say, the above action can be repeated indefinitely), you need to combine definition override with a constraint on the values that you consider interesting. For example, you could add the state constraint x \in 0 .. 100 (see Spec Options -> State Constraint). A useful way of looking at this is that model checking is a powerful debugging tool, and you use engineering judgement to determine what parts of the state space are interesting to analyze.
For your second question, TLA+ is not meant to analyze probabilistic systems in the sense that the result of the analysis depends on probability distributions (e.g., compute expected values or probabilities of specific events). As long as you are only interested in considering the reachable spaces, you can replace probabilistic choice with non-deterministic choice (i.e., disjunction / existential quantification) and for example consider both heads and tails as possible successor states.
Regards,
Stephan
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.
Amirhossein
--
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.