We want to design an asynchronous process Split that is the dual of Merge (Textbook Fig. 4.3, page 129). The process Split has one input channel in and two output channels out1 and out2. The messages received on the input channel should be routed to one of the output channels in a nondeterministic manner so that all possible splittings of the input stream are feasible executions. Describe all the components of the desired process Split.

Asynchronous Model 129 queue (msg) x1 := null; X2 :=null msg in A : Full(x1) + Enqueue (in, X1) A: -Full(x2) + Enqueuein2, X2) msg out msg in, A: Empty(x1) + out := Dequeue(x1) A?: Empty(x) + out := Dequeue(x2) Figure 4.3: Asynchronous Process Merge Asynchronous Model 129 queue (msg) x1 := null; X2 :=null msg in A : Full(x1) + Enqueue (in, X1) A: -Full(x2) + Enqueuein2, X2) msg out msg in, A: Empty(x1) + out := Dequeue(x1) A?: Empty(x) + out := Dequeue(x2) Figure 4.3: Asynchronous Process Merge