Solutions

The channel is replaced by two storage cells in sequence. The channel itself is not represented in Figure 11, but rather the condition that says whether or not the channel is empty. Accordingly, we stipulate conditions indicating whether or not the storage cells are empty. The fact that the storage cells are arranged sequentially means that objects can be transferred from the first storage cell to the second. Thus, in the model there must be an event, which, when it occurs, causes the condition ’storage cell 1 occupied’ to be unfulfilled and the condition ’storage cell 2 occupied’ to be fulfilled.