Non-deterministic choice
Non-deterministic choice
A number of laws apply to the choice operator :
Commutative: P R = R P
Associative: P (R S) = (P R) S = P R S
In this way, is similar to the concurrency operator ||. However, the non-determinism introduced by P || Q is concerned with the freedom of the scheduler on a single processor to choose either P or Q to execute first and with the effect of interrupts from the environment. Choice is concerned with the process level allowing “free” choice of actions. Note that while: P || SKIP = P
P SKIP = SKIP
since SKIP is always ready to be chosen.