Database Reference
In-Depth Information
arrows in
RA
)
and the rest of the transitions in ATrS
R
between the states in the
image of the mapping F
0
,
but where the transitions Out
R
and the test transitions
are substituted by the
NOP
transition
.
3.
Let us define the arrow-function F
P
:
Mor
U
P
→
Mor
R
P
such that for each atomic
arrow g
:
∂
0
(g)
→
∂
1
(g) in Mor
U
P
:
⎧
⎨
λIn
∗
ER
(Out
U
(∂
0
(g))) if g
∈{
COMMIT
,
ROLLBACK
,
CALL
n
};
F
P
(g)
=
λIn
∗
EU
(Out
R
(F
P
(∂
1
(g))))
f
n
if g
=
=
id
;
⎩
NOP
otherwise,
where f
n
is the composition of atomic transitions in ATrS
R
between the states
F
P
(∂
0
(g)) and F
P
(∂
1
(g))
,
but where the test transitions are substituted by the
NOP
transition
,
as follows
:
•
(
DEC
)
1
;
f
1
=
RETURN
◦
ACOM
◦
COM
◦
VCOM
◦
(
DEC
)
2
;
•
f
2
=
RETURN
◦
ACOM
◦
RBACK
◦
(
DEC
)
n
,
for n
•
3(
P
n
is an atomic arrow
,
as in
RA
),
and for the composition of atomic arrows g
◦
f
,
F
P
(g
◦
f)
=
F
P
(g)
◦
F
P
(f )
.
Then there exists the functor F
P
=
(F
P
,F
P
)
:
f
n
=
RETURN
◦
P
n
◦
≥
U
P
→
R
P
where the object-
function F
P
is the mapping obtained from the algorithm Smap(ATrS
U
, ATrS
R
)
.
Proof
It is easy to verify that
U
P
(and also
R
P
) is a well defined category: its
identity arrows are NOP
:
S
U
→
S
U
(which are the identity functions and hence
do not change a state), while all other arrows are the (unary) functions from
S
U
into
S
U
. Notice that also
In
∗
EU
(
In
∗
EU
(
{}
)
=
∅
)
=
NOP
:
S
U
→
S
U
is an identity
arrow as well (analogously,
In
∗
ER
(
In
∗
ER
(
{}
=
∅
=
:
S
U
→
S
U
is an identity
arrow in
R
P
). Thus, the arrows of these two categories are the unary operators (the
unary functions) of these two machines, so that their composition is another unary
function, that is, a well defined arrow (for the composition of arrows the associativity
holds, because they are the composition of functions).
Let us show that for the definition of
F
P
)
)
NOP
for the atomic arrows, the condition
F
P
(g
F
P
(f )
for the two atomic arrows
f
and
g
is satisfied. Let us
consider the following possible cases for
f
F
P
(g)
◦
f)
=
◦
:
st(l)
→
st(l
1
)
and
g
:
st(l
1
)
→
st(l
2
)
in
Fig.
6.3
(for one call from
M
U
to
M
R
):
1. If
l
2
<j
then, from definition of
F
P
,
F
P
(g
F
P
(g)
F
P
(f )
◦
f)
=
=
=
NOP
:
st
(k)
st
(k)
, so that
F
P
(g
F
P
(g)
F
P
(f )
.
→
◦
f)
=
◦
2. If
l
2
=
j
and
g
∈{
COMMIT
,
ROLLBACK
,
CALL
,n
}
then we define
In
∗
ER
Out
U
∂
0
(g)
:
F
P
(g
F
P
(g)
st
(k)
st
(k
◦
f)
=
→
+
1
).
Thus, from definition of
F
P
,
F
P
(f )
st
(k)
st
(k)
, and we obtain
=
NOP
:
→
F
P
(g
F
P
(g)
F
P
(g)
F
P
(g)
F
P
(f )
.
◦
f)
=
=
◦
NOP
=
◦
3. If
l
2
=
j
and
f
∈{
COMMIT
,
ROLLBACK
,
CALL
,n
}
then we define
In
∗
ER
Out
U
∂
0
(g)
:
F
P
(g
F
P
(f )
st
(k)
st
(k
◦
f)
=
→
+
1
).
