Information Technology Reference
In-Depth Information
17. Lohmann, N., Massuthe, P., Stahl, C., Weinberg, D.: Analyzing Interacting WS-
BPEL Processes Using Flexible Model Generation. In: Dustdar, S., Fiadeiro, J.L.,
Sheth, A. (eds.) BPM 2006. LNCS, vol. 4102, Springer, Heidelberg (2006)
A
General Notions and Notations
Definition 1 (Net)
Let P and T be finite, disjoint sets.
Let F
P
)
.
Then N
=(
P, T, F
)
is a
net
.
⊆
(
P
×
T
)
∪
(
T
×
The elements of
P
,
T
and
F
are
places
,
transitions
and
arcs
, graphically depicted
as circles, boxes and arrows, respectively.
In the rest of this Appendix A we assume a net
N
=(
P, T, F
).
Definition 2 (Pre-set, Post-set)
For x
∈
P
∪
T ,let
•
x
=
def
{
y
|
(
y, x
)
∈
F
}
is the
pre-set
of x
x
•
=
def
{
y
|
(
x, y
)
∈
F
}
is the
post-set
of x.
Definition 3 (Marking)
A
marking of
N is a mapping m
:
P
→
.
Graphically, a marking
m
is depicted by
m
(
p
) black dots (“
tokens
”) at each
place
p
P
.
For two markings
m
1
and
m
2
of
N
,let
m
1
+
m
2
be the marking of
N
, defined
for each
p
∈
P
by (
m
1
+
m
2
)(
p
)=
def
m
1
(
p
)+
m
2
(
p
).
For a marking
m
of
N
and a set
Q
∈
⊇
P
,extend
m
canonically to
m
:
Q
→
for each
q
∈
Q
\
P
by
m
(
q
)=0
Definition 4 (Enabling, Step)
Let t
T ,
and let m be a marking of N.
∈
•
t holds: m
(
p
)
1. m
enables
t if for each p
1
.
2. Let m enable t and let the marking n be defined by
n
(
p
)=
def
m
(
p
)
−
1
if p ∈
∈
≥
•
t \ t
•
t
•
\
•
t
n
(
p
)=
def
m
(
p
)
,otherwise.
Then
(
m, t, n
)
is a
step of
N, frequently written m
n
(
p
)=
def
m
(
p
)+1
if p
∈
t
→
n.
Definition 5 (Run)
A finite or infinite sequence m
0
t
1
m
1
t
2
... is a
run of
N if
(
m
i−
1
,t
i
,m
i
)
is a step
of N for i
=1
,
2
,....
Search WWH ::
Custom Search