| Hello Frédéric, CHOOSE represents deterministic choice. In particular, it satisfies (CHOOSE x : P(x)) = (CHOOSE y : P(y)) and more generally (\A x : P(x) <=> Q(x)) => (CHOOSE x : P(x)) = (CHOOSE x : Q(x)) TLC has some implementation of this deterministic operator and therefore returns the same value. It is a frequent mistake in specifications to confuse CHOOSE (deterministic choice) and \E in actions. For example, HandleRequestDet == CHOOSE req \in Requests : ... vs. HandleRequestND == \E req \in Requests : ... In a state where Requests is non-empty, the first form will produce precisely one successor state during model checking, and the second form Card(Requests) successor states. Typically it is the latter that you want. Also note that the PlusCal statement (with x \in S) { ...} translates to existential quantification. Best regards, Stephan
|