Process Model & Channel communication
Process Model & Channel communication
We can denote the use of a channel ch (for sending or receiving) by the event ‘ch’. For two processes (P & Q) to communicate via a channel, the ch event must be in both alphabets:
ch Î aP and ch Î aQ
Given:
P = ( ch!e ® P’)
Q = ( ch?v ® Q’(v))
Where the expression Q’(v) means that the behaviour of Q’ is potentially dependent on the value of variable v obtained from the channel. The following Laws apply:
P || Q = ( ch!e ® P’) || ( ch?v ® Q’(v)) = ch!e ® ( P’ || Q’(e))
P || Q = (( ch!e ® P’) || ( ch?v ® Q’(v)))\ch = ( P’ || Q’(e))
The notation \ch conceals the event ch from processes other than P & Q.
a(R\a) = (aR) - {a}