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