Graphics Programs Reference
In-Depth Information
A GSPN model covered by T-invariants may be live for some initial marking,
but some other analysis must be applied to ensure that the model does not
deadlock for the set of initial markings defined by the parametric initial
marking. Applying deadlock and trap analysis, it is possible to establish
whether a model is not live. Indeed, a model may be live only if each minimal
deadlock contains a trap marked in the (parametric) initial marking. In the
AGV transport system model, every deadlock contains a trap that is marked
in the parametric initial marking. The continuous transport system model
instead has three deadlocks that do not contain any marked trap in the
parametric initial marking. This implies that some transitions are not live;
moreover this is a clue that the system may reach a dead marking.
The
three deadlocks that do not contain a marked trap
are listed below:
1.
{
idleM
1
,free
S1
,in
S1
,in
S1
}
2.
{
idleM
2
,free
S3
,in
S3
,in
S3
}
3.
{
idleM
3
,free
S5
,in
S5
,in
S5
}
Using definition
2.5.2,
it is easy to verify that the above sets of places are
indeed deadlocks. For example, the input set of the first deadlock is:
{
outM
1
,mv
1−2
,mv
1−2
,mv
LU−1
,inM
1
}
and it is contained into its output set
{
outM
1
,mv
1−2
,mv
1−2
,mv
LU−1
,mv
LU−1
,inM
1
}
.
An interpretation of the three deadlocks above can be provided in terms of
system states. Let us consider the first set of places, and try to understand
whether a state where such places are all empty makes any sense: using the
previously computed P-invariants we can deduce that if
M(idleM
1
) + M(free
S1
) + M(in
S1
) + M(in
S1
) = 0
then
1. machine M
1
is busy (due to the fact that M(idleM
1
)
=
0 and
M(idleM
1
) + M(busyM
1
) = 1);
2. the transport segment in front of machine M
1
is occupied by a part
(due to the fact that M(free
S1
) = 0);
3. the part currently in segment S1 is a type a part that needs to be pro-
cessed by M
1
(due to the fact that M(free
S1
) + M(in
S1
) + M(in
S1
) = 0
and M(free
S1
) + M(wait
1
) + M(in
S1
) + M(in
S1
) = 1).
Search WWH ::
Custom Search