Thread Model
Thread Model
We have seen that the behaviour of a process is defined by the sequence of statements it executes. The notation:
P = (a ® P’)
means that process P is said to engage in the event or action a and then behave like P’. If P’ = (b ® P’’) it follows that:
P = (a ® b ® P’’).
The loop processes of the example can be defined as:
loopA = (rotateA ® loopA)
loopB = (rotateB ® loopB).
The ThreadDemo program can now be abstractly described by:
demo = loopA || loopB