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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Tue, 28 Apr 2020 12:37:42 +0200*References*: <CAKxfy0uEC9pQXReo6qyTbQKw59EWMSZo=wO8Wjn+FCGdowy29g@mail.gmail.com>

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
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/DF7583A3-1B35-4BB7-81B4-4324ECF552BA%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] Model Checking Specs having Nat***From:*Amirhossein Sayyadabdi

**References**:**[tlaplus] Model Checking Specs having Nat***From:*Amirhossein Sayyadabdi

- Prev by Date:
**[tlaplus] Model Checking Specs having Nat** - Next by Date:
**Re: [tlaplus] Model Checking Specs having Nat** - Previous by thread:
**[tlaplus] Model Checking Specs having Nat** - Next by thread:
**Re: [tlaplus] Model Checking Specs having Nat** - Index(es):