Graphics Programs Reference
In-Depth Information
As a consequence we can state the following property
[64]
: if in a PN system
every deadlock contains a trap marked in the initial marking then the system
is partially live (there is always at least one transition fireable in every
reachable marking) and therefore it will not block. Notice that a P-semiflow
is both a deadlock and a trap. Since deadlocks and traps have been defined
only for ordinary nets, then also the above property holds only on this
subclass. In the particular case of ordinary free-choice nets the property is
even stronger: indeed the presence of a marked trap into each deadlock is a
su
cient condition for the system to be live.
Structural relations between transitions — In section
2.3.4
we in-
troduced the concepts of conflict, confusion, mutual exclusion, and causal
connection. We now define some properties that characterize from a struc-
tural point of view the corresponding behavioural properties.
The structural conflict relation between transitions is a necessary condition
for the existence of an effective conflict relation.
Definition 2.5.4 Transition t
i
is in structural conflict relation with tran-
sition t
j
(denoted t
i
SC t
j
) iff
•
•
t
i
∩
•
t
j
6
=
∅
or
•
t
•
i
∩
◦
t
j
6
=
∅
Indeed, a transition t
i
that fires can affect the enabling degree of another
transition t
j
only if it changes the marking of either the input or the inhibi-
tion set of t
j
.
We can similarly define a necessary condition for a conflict to be free-choice
by defining a free-choice structural conflict as follows:
Definition 2.5.5 Transition t
i
is in free-choice structural conflict relation
with transition t
j
iff
•
I(t
i
) = I(t
j
) and
•
H(t
i
) = H(t
j
)
It is clear from the definition that this conflict is symmetric and that if two
transitions are in free-choice structural conflict then they are always enabled
together in any possible marking, with the same enabling degree.
It is also possible to find necessary conditions for mutual exclusion of tran-
sitions: one is based on inhibitor arcs and one on invariants. Mutual exclu-
sion due to inhibitor arcs is called HME, and we can intuitively say that
t
l
HME t
m
if there are places that are at the same time part of the input
set of t
l
and of the inhibition set of t
m
with arc multiplicities such that if one
has concession the other one has not, and viceversa; an example is shown in
Fig.
2.15.
More precisely:
Search WWH ::
Custom Search