Information Technology Reference
In-Depth Information
6.
V
is a finite set of typed variables such that
Type
[
v
]
2
S
for all
variables
v
2
V
;
7.
G
:
T
EXPR
V
is a guard function that assigns a guard to each
transition
t
such that
Type
[
G
(
t
)]
!
¼
Bool
;
8.
E
:
F
EXPR
V
is an arc expression function that assigns an arc
expression to each arc
f
!
2
F
such that
Type
[
E
(
f
)]
¼
C
(
p
)
MS
,
where
p
is the place connected to the arc
f
; and
9.
I
:
P
EXPR
1
is an initialization function that assigns an
initialization expression to each place
p
such that
Type
[
I
(
p
)]
!
¼
C
(
p
)
MS
.
Remarks:
(1)-(3) (
P
,
T
,
F
) is a Petri net structure as defined earlier.
(4) The set of
types
each of which is a set of values. A type is also
referred to as a
color set
and each value belonging to it is referred to
as a
color
. We assume that each type has at least one value (i.e.,
color).
(5) Function
C
maps each place
p
to a type
C
(
p
). That is, each token
in place
p
must have a data value that belongs to
C
(
p
).
(6)
V
is a finite set of typed variables. Each variable belongs to a
type defined in
S
. This set of variables is to be used in expressions in
(7)-(8).
(7) The guard function
G
maps each transition
t
, into a Boolean
expression where all variables are from
V
. At runtime the Boolean
expression is evaluated to be
true
or
false
depending on the values
of variables. Only when
G
(
t
)is
true
a transition may fire. Guard
expressions that are always evaluated to be
true
are omitted.
(8) The arc expression function
E
maps each arc
f
into an
expression of type
C
(
p
)
MS
. That is, each arc expression must
be evaluated to multisets over the type of the connected place
p
,
and it indicates the tokens to take from or yield to
p
when the
associated transition fires.
(9) The initialization function
I
maps each place
p
into an expres-
sion without any variable and must be of type
C
(
p
)
MS
. Initialization
expressions that are evaluated to be empty set (
1
) are omitted.
