Page 119 -

106 M. Wynn et al.

Fig. 3.3 A structured net with an OR-join task and cancelation regions

has any tokens in c6, and therefore, E is enabled at M. So, even though two active
paths are chosen after OR-split task A, the OR-join evaluation should not wait for
tokens from both paths, as it is possible that not all the tokens are on the path to this
OR-join task. (Note that Fig. 3.2 is not sound as it can deadlock in c4.)
Now, let us consider an OR-join in the context of cancelation. Figure 3.3 is a
net with an OR-join task E and task D removing tokens from the conditions c2, c5
and from the internal condition of task C when firing. Consider a marking M D
c2 C c3 C c4, which results from the scenario where all outgoing paths are selected
after completing task A,and task B has subsequently been performed. At M,there
is a token in the input condition c4 of OR-join task E. To determine whether task
E should be enabled at M , we need to find out whether tokens could be put into
c5 or c6 in the reachable markings of M. As it is possible to reach a new marking
M D c3 C c4 C c5 from M by firing task C, E should not be enabled at M.Now
0
consider whether task E would be enabled at marking M D c3 C c4 C c5.At M ,
0
0
c4 and c5 have one token each and so we need to see if c6 can be marked in the
reachable markings of M (i.e., can we reach a marking c4Cc5Cc6 or bigger?). The
0
only reachable marking from M (without enabling task E itself) is M D c4 C c6
00
0
by firing task D. Note that because of the cancelation region associated with task D,
the token from c5 has been removed. Hence, task E is enabled at M . It can be seen
0
from this example that even though the net is a structured net, having cancelation
regions can drastically change the behavior of the OR-join and these cancelation
regions cannot be ignored while performing an OR-join evaluation. Note also that
if task E fires at M D c3 C c4 C c5, we reach a new marking c3 C o, which can
0
lead to another marking c6 C o after firing task D where task E is enabled again and
then to 2o after firing task E a second time. In this case, the marking 2o indicates
that there are two tokens in the output condition of the net and, as a result, the net is
not sound.

3.2.2 The Formal Semantics

Even though YAWL is based on Petri nets, the YAWL language supports complex
constructs such as multiple instances, hierarchy, cancelation, and OR-joins that are