Information Technology Reference
In-Depth Information
We define the type of a microslot as the type of the least non-empty action
present:
ttype
MS
:
MS
→
TType
ttype
MS
(
true, true,
)
=
res
ttype
MS
(
true, ,
)
=
req
ttype
MS
(
, ,
)
=
sel
We define the type of a
Slot
as the type of the first of the microslots, if present,
otherwise it is
act
.
ttype
S
:
Slot
→
TType
ttype
S
(
,
(
p,
))
=
act
ttype
S
((
m
: )
,
)
=
ttype
MS
(
m
)
5.3
Trace Operators
We now describe a series of operators whichcanbeusedtobuildandjointraces
and their building blocks.
Building with Single Actions.
The first are a series of constructors that
construct slots of the various types from a single guarded action and accompa-
nying transition type. We shall refer to the combination of a transition type and
guarded action as a
typed action
.
Given a non-
act
, non-void action, we wish to build the corresponding mi-
croslot:
mkm
:
TType
→
GA
→
MS
mkm
sel
(
g
)
=(
g, true, true
)
mkm
req
(
g
)
=(
true, g, true
)
mkm
res
(
g
)
=(
true, true, g
)
Given a typed action we wish to build the corresponding slot, where the action
can be null only if of type
act
:
mks
:
TType
→
GA
→
Slot
mks
act
(
g
)
=(
, g
)
mks
t
(
g
)
=(
mkm
t
(
g
)
, true
)
Lifting Action Merging.
We want to lift the action merge operators to work
with microslots.
Search WWH ::
Custom Search