Non-deterministic choice
Non-deterministic choice
Following CSP, we introduce the operator [] to our process notation to mean non-deterministic choice.
P = X [] Y
implies that P can act as X if the conditions for X are possible, or Y if it is possible. If both X and Y are possible then a non-deterministic or “free” choice can be made between X and Y. Given the [] operator, we can now specify the COUNTER process correctly:
COUNTER = (west? ® inc ® COUNTER
[] east ? ® inc ® COUNTER
)
In the formal notation, outputs can also be a choice:
P = (ch1!a ® Q) [] (ch2!b ® R)
However, implementing outputs as possible choices in a programming language is problematic.