Dear Dr. Cristia,

You are correct that the value of CHOOSE x : x \in X depends on the value of X. Hence, if X changes, then that value might change. However, if X has the same value in two different states, then CHOOSE x : x \in X will have the same value in those two states. If that is what you want, then the CHOOSE expression is fine.

However, be aware that this is non nondeterminism in the following sense. If you have a specification that makes a nondeterministic choice of a value y, you can implement it with a system that makes any deterministic choice--for example, choosing y = 25. However, if a specification sets y to CHOOSE x : x \in X, then the implementation must also set y to that same expression.

Leslie Lamport

-----Original Message----- From: mcristia@fceia.unr.edu.ar [mailto:mcristia@fceia.unr.edu.ar] Sent: Monday, July 22, 2002 1:39 PM To: Leslie Lamport Subject: Choose operator and non-determinism

Dear Dr. Lamport:

I hope you find the time to answer a brief question regarding the choose operator and how it relates to non-determinism (if it does in any way).

You repeatedely say that this operator cannot be used to introduce non-determinism because it always returns the same (random) value. The question is what exactly means "always"?

Let's say you have a state variable, X, which is a set and an action, A, which should extract an unspecified element from X every time it's executed. Is it correct to write it like this?

A = = X # \empty /\ X' = X \ {choose x: x \in X}

In this case set X changes due to A steps and so the predicate used in the choose operator is not always the same: the set from which to extract elements is different in different states, so it is possible to say that choose will return different elements in different executions of A.

Am I correct?

Does it represent non-determinism?

If I'm wrong or if you find it in contradiction with the TLA style, could you tell me how would you write such an action?

Thank you very much!

Sincerely,

Maximiliano Cristia

Lifia and U.N.R.