Suppose that we want the following process:
The above process can be got by getting rid of the right-upper state and the left-lower state from the following process. So we are going to make this lattice-like process first. Let's call it PL.
The process PL generates the event a three times and the event b two times in any order. We first define two processes PA and PB which generates only the event a and b respectively.
We can construct the process PL by combining the process PA and PB. The method to combine two processes is the interleave, because each type of event can occur independently. The interleave is realized by specifying the empty list as a sync-list in the par form.
(define-process PAB (par '() PA0 PB0))
The result of the parallel composition is as follows. It is certainly the same as the process PL.
Secondly we consider cutting two states at the corners of the process PAB. It is achieved by defining a process which keeps track of the behaviors of the process PAB and restricts part of them. Let's call this process a constraint process Q. The process Q restricts the third occurrence of the event a and the second occurrence of the event.
We combine the process PAB and the constraint process Q by parallel composition. Since the constraint process inhibits some occurrences of events, it is necessary to specify all of events that the process PAB can generate as the sync-list in the par form. It is (list a b) in this case.
(define-process PABQ (par (list a b) PAB Q))
The result is as follows, which is what we wanted.
I described in the SyncStitch Users Guide that the parallel compositions have two roles in modeling.
Additionally, as we seen so far, the parallel compositions can be used as a tool to model processes. Roughly speaking, they can be used for two objectives: one is for interleaving and another is constraints.
The parallel compositions as a modeling tool enable us to model a large complicated process from relatively small processes.