Information Technology Reference
In-Depth Information
We will want to merge a single guarded non-
act
action into a pre-existing
microslot:
♦
:
GA
×
TType
×
MS
→
MS
g
♦
sel
(
s, q, r
)
=(
g
♦
s, q, r
)
g
♦
req
(
s, q, r
)
=(
s, g
♦
q, r
)
g
♦
res
(
s, q, r
)
=(
s, q, g
♦
r
)
We describe the merging of two microslots later when the parallel construct is
discussed.
Typed Cons-ing.
By “typed cons-ing” (:: or ::
t
) we mean the process of placing
a typed action at the start of an existing list of actions, at the microslot, slot or
trace level. We first consider cons-ing a non-
act
, non-null action into a microslot
or slots. If the action has a type greater than that of the microslot, then we have
to create a new microslot immediately prior to the given one, containing the
action. This is because “consing” means pre-pending an earlier action, so if an
action of type
res
(say) is being placed in front of a microslot containing
sel
or
req
actions, then it must have occurred in an earlier microslot. This is why the
signature of the function indicates that merging a typed action with a microslot
may result in more than one microslot as a result.
::
MS
+
:
GA
→
TType
→
MS
→
g
::
t
m
=
if
t > ttype
MS
(
m
)
then
We can extend this to work with microslot sequences in the obvious way:
::
mkm
t
(
g
)
, m
else
g
♦
t
m
MS
∗
MS
∗
:
GA
→
TType
→
→
g
::
t
=
mkm
t
(
g
)
=(
g
::
t
m
)
μ
We can now extend type-consing to slots and traces, in which case we can now
handle
act
-actions. Consing an
act
-action always creates a new slot at the front:
::
g
::
t
(
m
:
μ
)
Slot
+
:
GA
→
TType
→
Slot
→
g
::
act
s
=
mk
act
(
g
)
, s
g
::
t
(
μ, a
)
=
(
g
::
t
μ, a
)
::
:
GA
→
TType
→
Trc
→
Trc
=(
g
::
t
s
)
τ
g
::
t
(
s
:
τ
)
Concatenation for Microslots.
We can now define a form of concatenation for
microslots (
9
) which merges the last microslot of the first sequence (
ante-slot
)with
the first microslot of the second (
post-slot
), if possible. This is possible when no
action in the ante-slot has a type greater than that of an action in the post-slot. We
first define an operator (
) taking a pair of micro-slots to a sequence of same:
Search WWH ::
Custom Search