A Petri Net model, P, of the uncontrolled plant is shown in Figure 12. The meaning of the places is given in Table 3.
Figure 12: Petri Net Model for Two-Pusher Example
In the above table, position ``(i-j)'' of the workpiece means that
the workpiece is between position i and position j.
The Petri Net in Figure 12 is safe and conservative. Now,
notice that the forbidden state requirement (i) of
Specifications I can be expressed by the marking constraint 
. This means we can apply Giua's method to obtain
a safety controller. First, we need the incidence matrix 
of our net. This is given in the matrix below, where row names are
given by place numbers, and column names are given by transition
numbers. Each entry (i,j)=1(-1) indicates that place i is an
output of (input to) transition j.
Now, our marking constraint in the form of a GMEC is given by
where 
and
k=1. To get the ``monitor'' solution, we then compute 
which yields
(0,0,-1,1,0,0,-1,1,0,0,0,0,-1,0,0,0,-1,0). This means that our new
supervisory place, which we will call S, is an input of transitions
, 
, 
, and 
, and Sis an output of
transitions 
and 
. The initial marking for S is obtained
by computing: 
. This monitor
solution is illustrated in Figure 13.
Notice that we still need to enforce the sequential specification for
this system. As can be seen in the PN model, it is still possible for
the pushers to move back and forth without accomplishing the movement of the
workpiece toward its final position. After careful observation of
this PN model, we can see that disabling transitions 
, 
,
, and 
, leaves no other possible path for the
workpiece to follow than the desired one. But clearly, a formal
method to impose such sequential specification on the PN model of this
system is missing.
Figure 13: Monitor Supervisor for Safetey Specification of Two-Pusher Example