Possibility ot hide all event created by a channel
2 posters
PAT Forum :: Support :: Using PAT :: CSP and PCSP Module
Page 1 of 1
Possibility ot hide all event created by a channel
Hi,
Is it possible in CSP# to hide all the event caused by a channel without explicitly enumerating all of them? Thanks.
The following code is my try which doesn't work at all. (All the assertions fail.)
========================
channel ch1 0;
channel ch2 0;
P = ch1?x -> b -> ch2!3 -> P;
Q = a -> ch1!3 -> ch2?x -> Q;
P1 = (P ||| Q) \{ch1, ch2};
P2 = a -> b -> P2;
#assert P1 refines P2;
#assert P2 refines P1;
#assert P1 refines<F> P2;
#assert P2 refines<F> P1;
#assert P1 refines<FD> P2;
#assert P2 refines<FD> P1;
==================
Is it possible in CSP# to hide all the event caused by a channel without explicitly enumerating all of them? Thanks.
The following code is my try which doesn't work at all. (All the assertions fail.)
========================
channel ch1 0;
channel ch2 0;
P = ch1?x -> b -> ch2!3 -> P;
Q = a -> ch1!3 -> ch2?x -> Q;
P1 = (P ||| Q) \{ch1, ch2};
P2 = a -> b -> P2;
#assert P1 refines P2;
#assert P2 refines P1;
#assert P1 refines<F> P2;
#assert P2 refines<F> P1;
#assert P1 refines<FD> P2;
#assert P2 refines<FD> P1;
==================
alex2ren- Posts : 6
Join date : 2012-12-03
Re: Possibility ot hide all event created by a channel
You have to explicitly to give all the events as below.
P1 = (P ||| Q) \{ch1.1, ch1.2, ch2.1};
P1 = (P ||| Q) \{ch1.1, ch1.2, ch2.1};
alex2ren wrote:Hi,
Is it possible in CSP# to hide all the event caused by a channel without explicitly enumerating all of them? Thanks.
The following code is my try which doesn't work at all. (All the assertions fail.)
========================
channel ch1 0;
channel ch2 0;
P = ch1?x -> b -> ch2!3 -> P;
Q = a -> ch1!3 -> ch2?x -> Q;
P1 = (P ||| Q) \{ch1, ch2};
P2 = a -> b -> P2;
#assert P1 refines P2;
#assert P2 refines P1;
#assert P1 refines<F> P2;
#assert P2 refines<F> P1;
#assert P1 refines<FD> P2;
#assert P2 refines<FD> P1;
==================
Similar topics
» What's the appropriate way to hide events caused by array of channels?
» the semantics of channel in CSP#
» the semantics of channel in CSP#
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
|
|