In order to create the plant model P, we first identify the independent
subsystems, which are simply Pushers 1 and 2.
Figure 5, shows
the automaton for Pusher i, called 
. The states
of are I(i), M(i), and E(i), indicating
Pusher i's initial, middle, and extended positions, respectively.
State I(i) is both the initial and final state.
Figure 5: : Automaton for Pusher i, (i=1,2)
The plant model is given by: 
. The controllable events are 
, and the uncontrollable events are 
.
Figure 6: :
Plant Model for Two-Pusher Example
In Figure 7, we give the recognizers for requirements
(i) and (ii) of Specifications I. Note that they are are
already self-looped. 
represents the forbidden state 
specification.
We can think of state A as the resource (``space'') which the two
pushers are to share. Initially, this space is available, and then it
can be ``used up'' by Pusher 1 (through event 
), or by Pusher 2
(through event 
). Notice that when this resource is being used
by Pusher 1 (Pusher 2), the system is in state B (C), from which
event 
( ) is not allowed. That is, there is a mutual
exclusive use of the resource by the pushers. The recognizer 
gives the
sequence of events that will move the workpiece through the desired
positions.
Figure 7: State Machines for Specifications I(Self-looped)
Our next figure, Figure 8, shows the legal states as
specified by requirement (i) of Specifications I. This is
obtained by constructing 
.
Finally, the legal language, shown in Figure 9, is obtained by
constructing 
. For
simplicity, we have ignored the ``A,'' ``B,'' ``C'' labels of the
states in 
. Also, to avoid a crowded graph, some states
appear twice (those which are boxed in).
Figure 9: 
: Generator of Legal Language for
Two-Pusher Example.
The reader can verify that is a controllable
language. This means that
there is no uncontrollable event which is possible from some state in
P, but which is not possible in the corresponding state of . In the specific context of our example, from every state in containing position Ei, the uncontrollable event zi, which
is always possible in P, remains possible in .
However, notice that contains the following blocking
states: 
, 
, 
, 
,
, and 
.
Upon ``deletion'' of these states (i.e. by disabling the appropriate
controllable events), we obtain the recognizer for a
proper supervisor S, as shown in Figure 10, and the
control pattern given in Table 1:
Figure 10: S: Proper Supervisor for Two-Pusher Example.
