We can construct a satisfactory model of the master–slave program by observing that, although it creates a sequence of new slave processes, only a single slave thread is active at any one time. Consequently, we use a single slave process, which after it terminates, immediately becomes available to be started again:
SLAVE = (start->rotate->join->SLAVE).
The master thread is modeled by the following process:
MASTER = (slave.start->rotate ->slave.join->rotate->MASTER).
The master–slave program can now be modeled as the composition:
||MASTER_SLAVE = (MASTER || slave:SLAVE).
The behavior of this model is depicted in the LTS of Figure 9.9.
Figure 9.9: MASTER_SLAVE LTS.
From the LTS, it can be seen that the slave rotation action, slave.rotate, and the master rotation action, rotate, are concurrent since they can occur in any order. However, after the slave.join action only the master rotation action can take place, as in the applet. The model can easily be generalized to a system in which two or more slave processes are active concurrently.