In the interleave expression, the Skip Process can't be run unless all processes in the interleave process becomes Skip.
Skip||a->Skip||b->Skip
For example, for above expression, it has two possible next steps, which is events {a,b},but the Skip cannot go.
The reason the operational semantics of sequential expression is defined as
P->(CompleteEvent)P'
-------------------------
P;Q->(tau)P';Q
and Skip process is defined as
--------------
Skip->(CompleteEvent)Stop
now let P=Skip||a->Skip||b->Skip
if P allows that Skip to go, all other expression will force to stop!
Subscribe to:
Post Comments (Atom)
No comments:
Post a Comment