Information Technology Reference
In-Depth Information
a)
k
T
o
X
!
q
T
c)
o
s
!
Inv
T
A
T
0
A
T
3
l
∅
h
T
X
g
T
i
?
o
S
!
···
i
?
s
T
r
T
S
l
u
o
x
!
A
T
2
T
A
T
1
d)
T
0
\\ S
0
T
1
\\ S
1
b)
w
S
o
X
!
z
S
Inv
S
A
S
0
A
S
3
v
S
u
S
o
S
!
···
i
?
p
S
T
3
\\ S
3
t
S
A
S
2
A
S
1
l
∅
l
u
T
2
\\ S
2
Fig. 9.
Initialstates oftwoexampleTIOAa)
A
T
,b)
A
S
,c)anoverviewofthecom-
municationflowandd)theinitialstateoftheresultingquotient
A
U
,wehavethat
A
T
composablewith
A
U
and
A
S
||
A
U
≤
A
T
||
A
U
.Moreover
if
A
T
compatiblewith
A
U
then
A
S
compatiblewith
A
U
.
4.3 Quotient
Anessentialoperatorinacompletespecificationtheoryistheoneof
quotienting
.
Itallowsforfactoringoutbehaviourfromalargercomponent.Ifonehasalarge
componentspecification
A
T
andasmallone
A
S
then
A
T
\\
A
S
isthespecification
ofexactlythosecomponentsthatwhencomposedwith
A
S
refine
A
T
.Inother
words,
A
T
\\
A
S
specifiestheworkthatstillneedstobedone,givenavailability
ofanimplementationof
A
S
,inordertoprovideanimplementationof
A
T
.This
isanontrivialoperationwhichreducestosynthesisofatimedgame.Tothebest
ofourknowledge,wearethefirsttocomputethequotientinatimedsetting.
Werequirethatforthedividend
A
T
andthedivisor
A
S
thefollowingrelations
onactionsetshold:
Σ
i
⊆
Σ
o
.Iftheserequirementsontheinput
and output sets are met, then the quotient of
A
T
by
A
S
, which is denoted
A
T
\\
Σ
i
and
Σ
o
⊆
,
q
0
=(
q
0
,q
0
)
,
Clk
=
A
S
istheTIOAgivenby:
Loc
=
Loc
T
×
Loc
S
∪{
l
u
,l
∅
}
Clk
T
.
The two new states
l
u
and
l
∅
are respectively universal and inconsistent. The
set of actions
Act
=
Act
i
Clk
S
{
x
new
}
,
Inv
((
q
T
,q
S
)) =
Inv
(
l
u
)=
true
and
Inv
(
l
∅
)=
{
x
new
≤
0
}
Act
o
is given by
Act
i
=
Act
i
∪
Act
o
∪{
i
new
}
and
Act
o
=
Act
o
\
Act
o
.Thesetofedges
E
isdefinedbythefollowingrules:
1. if
q
T
∈
Loc
T
,q
S
∈
Loc
S
,
a
∈
Act
then
((
q
T
,q
S
)
,a,
¬
Inv
S
(
q
S
)
,
{
x
new
}
,l
u
)
∈
E
2. if
q
T
∈
Loc
T
,q
S
∈
Loc
S
then
((
q
T
,q
S
)
,i
new
,
¬
Inv
T
(
q
T
)
∧
Inv
S
(
q
S
)
,
{
x
new
}
,l
∅
)
∈
E
