PAT Forum
Would you like to react to this message? Create an account in a few clicks or log in to continue.

Possibility ot hide all event created by a channel

2 posters

Go down

Possibility ot hide all event created by a channel Empty Possibility ot hide all event created by a channel

Post  alex2ren Thu Oct 10, 2013 8:26 am

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;
==================

alex2ren

Posts : 6
Join date : 2012-12-03

Back to top Go down

Possibility ot hide all event created by a channel Empty Re: Possibility ot hide all event created by a channel

Post  pat team Tue Dec 24, 2013 6:55 pm

You have to explicitly to give all the events as below.

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;
==================

pat team
Admin

Posts : 17
Join date : 2010-02-15

http://www.comp.nus.edu.sg/~pat/

Back to top Go down

Back to top

- Similar topics

 
Permissions in this forum:
You cannot reply to topics in this forum