the semantics of channel in CSP#
2 posters
PAT Forum :: Support :: Using PAT :: CSP and PCSP Module
Page 1 of 1
the semantics of channel in CSP#
Q1: It seems to me that the channel is CSP# is totally different from that in CSPm. But in the document 3.1.1.2, it says "One exception is the channel names are allowed, because we may want to use channel name in a specific process to simulate the channel behaviors and use refinement checking to compare with real channel events." Is there any example illustrating this idea? Thanks.
Q2: What's the semantics of P4 in the following model? Is P4 a refinement of P5?
channel ch 0;
P0 = ch!3 -> e -> P0;
P1 = ch?x -> e -> P1;
P2 = ch?x -> e -> P2;
P4 = P0 || P1 || P2;
P5 = ch!3 -> e -> P5;
Q2: What's the semantics of P4 in the following model? Is P4 a refinement of P5?
channel ch 0;
P0 = ch!3 -> e -> P0;
P1 = ch?x -> e -> P1;
P2 = ch?x -> e -> P2;
P4 = P0 || P1 || P2;
P5 = ch!3 -> e -> P5;
alex2ren- Posts : 6
Join date : 2012-12-03
Re: the semantics of channel in CSP#
For Q1: please refer to the following paper for a more detailed discussion.
http://www.comp.nus.edu.sg/~pat/publications/icfem12%20comparison.pdf
in CSP#, channel is more like a Promela channel so that they can be synchronous or asynchronous.
You can use channel name as event name as shown in the following, we don't have restriction on the use of channel name. c becomes a channel if it is used as a channel communication. the event c is an normal event, and has nothing to do with channel c.
channel c 0;
P = a -> c -> Skip;
For Q2: you can use the PAT simulator to draw its graph. then you can see that channel are pair-wise synchronization. for synchronous channel, they will become . after the synchronization.
that is P1 sync with P2 becomes ch.3, which is missing in P5, so the refinement doesn't hold.
Let us know if you have more questions.
http://www.comp.nus.edu.sg/~pat/publications/icfem12%20comparison.pdf
in CSP#, channel is more like a Promela channel so that they can be synchronous or asynchronous.
You can use channel name as event name as shown in the following, we don't have restriction on the use of channel name. c becomes a channel if it is used as a channel communication. the event c is an normal event, and has nothing to do with channel c.
channel c 0;
P = a -> c -> Skip;
For Q2: you can use the PAT simulator to draw its graph. then you can see that channel are pair-wise synchronization. for synchronous channel, they will become . after the synchronization.
that is P1 sync with P2 becomes ch.3, which is missing in P5, so the refinement doesn't hold.
Let us know if you have more questions.
alex2ren wrote:Q1: It seems to me that the channel is CSP# is totally different from that in CSPm. But in the document 3.1.1.2, it says "One exception is the channel names are allowed, because we may want to use channel name in a specific process to simulate the channel behaviors and use refinement checking to compare with real channel events." Is there any example illustrating this idea? Thanks.
Q2: What's the semantics of P4 in the following model? Is P4 a refinement of P5?
channel ch 0;
P0 = ch!3 -> e -> P0;
P1 = ch?x -> e -> P1;
P2 = ch?x -> e -> P2;
P4 = P0 || P1 || P2;
P5 = ch!3 -> e -> P5;
PAT Forum :: Support :: Using PAT :: CSP and PCSP Module
Page 1 of 1
Permissions in this forum:
You cannot reply to topics in this forum
|
|