Information Technology Reference
In-Depth Information
To expose the concurrency information recorded by the controller
C
we enhance
the construction presented so far. We introduce a new channel
co
:bag
Σ
P
to
communicate the recorded concurrency information and modify the processes
C
,
Con
and
Ext
as follows.
C
1
(
X
)=
co
.
X
→
(
s
?
x
→
C
1
(
X
[[
x
]] )
sh
?
x
→
C
1
(
X
[[
x
]] )
C
1
(
X
∪
e
?
x
→
[[
x
]])
→
C
1
(
X
∪
eh
?
x
[[
x
]] )
term
→
SKIP
)
Con
1
(
P
)=(
T
(
P
);
term
→
SKIP
)
|
S
Con
|
C
1
([[ ]])
Ext
1
(
P
)=
Hr
(
Con
1
(
P
))
We observe that: (a) hiding of
co
does not cause divergence because there are no
adjacent
co
events in any trace of
Ext
1
(
P
); and (b)
co
is not in conflict with any
event in
C
1
, so hiding of
co
does not introduce nondeterminism and consequently
changes neither the failures of
Ext
1
(
P
) nor its traces.
Hence
C
1
(
X
)
\{|
co
|}
=
C
(
X
)
and
=
Ext
(
P
)
.
The controller process
C
never refuses any events offered by
T
(
P
) thus, again,
the following proposition holds by construction of
Con
.
Ext
1
(
P
)
\{|
co
|}
Proposition 4.
The controller process C records the concurrent events of P:
t
∀
(
x
,
y
):
conc
(
P
)
,
∃
co
.
b
·
∧
y
in
b
.
:
traces
(
Con
1
(
P
))
x
in
b
The controller
C
is designed to record concurrency information but not change
the behavior of the transformed process
T
(
P
). This is captured formally by the
following lemma:
Lemma 1.
For any process P as above,
Ext
(
P
)=
Hr
(
T
(
P
))
.
Proof.
The proof follows by 'reduction of parallel composition'. By definition of
parallel composition,
P
|
Σ
Q
|
Q
=
P
if
Q
never refuses an event
x
:
Σ
Q
.
Ext
(
P
)
=
definition of
Ext
Hr
(
Con
(
P
))
Search WWH ::
Custom Search