Information Technology Reference
In-Depth Information
3. if
(
q
T
,a,ϕ
T
,c
T
,q
T
)
∈
E
T
and
(
q
S
,a,ϕ
S
,c
S
,q
S
)
∈
E
S
thisgives
((
q
T
,q
S
)
,a,
ϕ
T
∧
ϕ
S
,c
T
∪
c
S
,
(
q
T
,q
S
))
∈
E
4. foreach
(
q
S
,a,ϕ
S
,c
S
,q
S
)
∈
Act
o
E
S
with
a
∈
thisgivesriseto
((
q
T
,q
S
)
,a,
,l
∅
)
where
G
T
=
{
ϕ
T
|
(
q
T
,a,ϕ
T
,c
T
,q
T
)
}
ϕ
S
∧¬
G
T
,
{
x
new
}
5. if
(
q
T
,a,ϕ
T
,c
T
,q
T
)
∈
Act
S
then
((
q
T
,q
S
)
,a,ϕ
T
,c
T
,
(
q
T
E
T
,
a/
∈
,q
S
))
∈
E
Act
o
thisgivesriseto
((
q
T
,q
S
)
,a,
6. foreach
(
q
T
,a,ϕ
T
,c
T
,q
T
)
∈
E
T
with
a
∈
,l
u
)
where
G
S
=
{
ϕ
S
|
(
q
S
,a,ϕ
S
,c
S
,q
S
)
}
¬
G
S
,
{}
7. foreach
a
∈
Act
i
thisgivesriseto
(
l
∅
,a,x
new
=0
,
{}
,l
∅
)
8. foreach
a
∈
Act
thisgivesriseto
(
l
u
,a,
true
,
{}
,l
u
)
The quotients input set,
Act
i
, consists of the inputs to the outer component
A
T
and the outputs of the existing inner component
A
S
(See Figure 9c) and
a new fresh input action
i
new
. The output set of the quotient,
Act
o
,issimply
theoutputsetoftheoutercomponent,
A
T
,minus theoutputs handledbythe
existinginnercomponent
A
S
.Theresultingquotienthastwonewspecialstates
l
u
and
l
∅
.Thefirst
universal
state,
l
u
,representsallthecaseswheretheexisting
innercomponent
A
s
hasviolatedtheguaranteesoftheoutercomponent
A
T
and
thustherearenorestrictionsonthefuturebehaviourofthequotient.Thesecond
inconsistent
state,
l
∅
,representsallthecaseswherethequotientbytakingthis
actionwoulditselfviolatetheassumptionsoftheothercomponents.
Intheabovedefinitionwehaveeightrules.Thefirstrulecreatesanewtransi-
tionleadingtothe
universal
statewithaguardthatequalstheoriginalinvariant
oftheexistinginnerspecification.Thesecondrulereflectsthecasewherethein-
variantof
A
T
isnotsatisfiedwhiletheinvariantof
A
S
is.Thethirdrulehandles
allregularsynchronisationwherethe guardsofboth componentsaresatisfied.
Thefourthrulehandlesthecasewheretheinnercomponentgeneratesanoutput
at a time where it is not allowed by any of the matching guards in the outer
component
A
T
.Thefifthrulehandlesthecaseswhere
A
T
takesanactionwhich
isnotintheactionsetof
A
S
.Thesixthrulerepresentsallthecaseswhere
A
T
takesanactionwhichisnotallowedbyanyofthematchingguardsin
A
S
thus
leading to the universal state. Finally the seventh rule makes the
l
∅
state in-
consistent and the eighth rule ensuresthat the universalstate has all possible
behaviour.Figure9illustratesonestepinthecomputationofaquotient.
LikeConjunction,thequotientoperationmayproduce(locally)inconsistent
specifications.Hence,eachquotientoperationhastobefollowedbyapruning.
In[12],wehaveshownthatthequotientoperationproducesthemostliberal
specificationwithrespecttorefinement.Formallywehavethefollowingtheorem.
Theorem 1.
Foranytwospecificationautomata
A
S
and
A
T
suchthatthequo-
tientisdefined,andforanyimplementation
X
over thesamealphabet as
T
\\
S
wehavethat
S
||
X
isdefinedand
S
||
X
≤
T
iff
X
≤
T
\\
S
.
5 Tool Implementation
We beginwith summarisingthe functionality ofthe tool,andproceedlater to
presentarunningexample.
