Both processes execute the same protocol. A process consists of various types of data declarations and a set of guarded commands. A guarded command consists of a predicate, which serves to enable the command, and an action, which will be executed atomically. The set of guarded commands is evaluated repeatedly, and at each execution an enabled command is executed. If multiple commands are enabled, then one is selected non-deterministically, but under the following fairness condition: a command that is enabled continuously will eventually be executed.
Selection statements (if ... 
... ...fi)
also have the above non-deterministic and fairness properties.
One data declaration type should be mentioned: a parameter datum is generated each time the guarded command set is evaluated; the parameter is set to a random value of the same type as the parameter.