Information Technology Reference
In-Depth Information
The intuition is that
Ext
splits each event in its argument, relabels the start
event back to the original and hides the end event and does so whilst faithfully
translating the process combinators.
A proof by structural induction is given in our technical report [6], using the
results of the next section, which enforce the intuition and enable the proof to
proceed uniformly.
The information stored in the bag held by
C
can be exploited in various ways.
One obvious way is to introduce guards
g
0
,...,
g
3
as follows.
C
0
(
X
)=
g
0
(
X
)&
s
?
x
→
C
0
(
X
[[
x
]] )
g
1
(
X
)&
sh
?
x
→
C
0
(
X
[[
x
]])
g
2
(
X
)&
e
?
x
→
C
0
(
X
∪
[[
x
]])
g
3
(
X
)&
eh
?
x
→
C
0
(
X
∪
[[
x
]] )
term
→
SKIP
Since the guards restrict the behavior of
C
0
relative to
C
,wehave
C
T
C
0
.
Modifying the extension
Ext
of
P
to use
C
0
yields
Ext
0
(
P
)=
Hr
((
T
(
P
);
term
→
SKIP
)
|
S
Con
|
C
0
([[ ]])
.
By construction of
C
0
and Theorem 1 we have
P
T
Ext
0
(
P
)
.
In the case that checking with FDR fails to establish the refinement
Ext
0
(
P
)
T
P
,
it provides a counterexample leading to a state violating
g
i
.
5 Properties
In this section,
t
,
u
are sequences, the concatenation of sequences
t
and
u
is
written
t
u
,
t
X
restricts
t
to the elements that are contained in
X
and #
t
denotes the length of the sequence
t
. Containment of an element
x
in a sequence
t
is written
x
in
t
. The results of this section are used in proving Theorem 1.
Proofs are largely routine.
First observe the following relations between
s
and
e
events.
Proposition 1 (
s-e-precedence
).
Each instance of an event e
.
x
:
Σ
T
(
P
)
is
preceded by its corresponding instance s
.
x
:
Σ
T
(
P
)
:
t
∀
e
.
x
:
traces
(
T
(
P
))
·
#(
t
{
s
.
x
}
)
>
#(
t
{
e
.
x
}
)
.
Search WWH ::
Custom Search