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