What's the appropriate way to hide events caused by array of channels?

View previous topic View next topic Go down

What's the appropriate way to hide events caused by array of channels?

Post  alex2ren on Mon Dec 17, 2012 1:04 pm

The following code has syntax error. What's the appropriate way to hide events caused by array of channels? I want to show that Sys and S are equivalent. Thanks.

Code:
channel ch[2] 0;

P = put -> ch[0]!1 -> ch[1]?x -> P;
C = ch[0]?x -> get -> ch[1]!1 -> C;

Sys = (P ||| C) \ {ch[0].1, ch[1].1};

S = put -> get -> S;

#assert S refines Sys;

#assert Sys refines S;


alex2ren

Posts : 6
Join date : 2012-12-03

View user profile

Back to top Go down

Re: What's the appropriate way to hide events caused by array of channels?

Post  pat team on Mon Dec 24, 2012 11:29 pm

Thanks for reporting this.
Current PAT doesn't support this, please wait for the release of PAT 3.5 next week.
the new syntax is following
Sys = (P ||| C) \ {"ch[0].1", "ch[1].1"};

alex2ren wrote:The following code has syntax error. What's the appropriate way to hide events caused by array of channels? I want to show that Sys and S are equivalent. Thanks.

Code:
channel ch[2] 0;

P = put -> ch[0]!1 -> ch[1]?x -> P;
C = ch[0]?x -> get -> ch[1]!1 -> C;

Sys = (P ||| C) \ {ch[0].1, ch[1].1};

S = put -> get -> S;

#assert S refines Sys;

#assert Sys refines S;


pat team
Admin

Posts : 17
Join date : 2010-02-15

View user profile http://www.comp.nus.edu.sg/~pat/

Back to top Go down

Re: What's the appropriate way to hide events caused by array of channels?

Post  pat team on Sat Dec 29, 2012 12:49 am

PAT 3.5 is released and this is supported. Please download and try.

pat team wrote:Thanks for reporting this.
Current PAT doesn't support this, please wait for the release of PAT 3.5 next week.
the new syntax is following
Sys = (P ||| C) \ {"ch[0].1", "ch[1].1"};

alex2ren wrote:The following code has syntax error. What's the appropriate way to hide events caused by array of channels? I want to show that Sys and S are equivalent. Thanks.

Code:
channel ch[2] 0;

P = put -> ch[0]!1 -> ch[1]?x -> P;
C = ch[0]?x -> get -> ch[1]!1 -> C;

Sys = (P ||| C) \ {ch[0].1, ch[1].1};

S = put -> get -> S;

#assert S refines Sys;

#assert Sys refines S;


pat team
Admin

Posts : 17
Join date : 2010-02-15

View user profile http://www.comp.nus.edu.sg/~pat/

Back to top Go down

Re: What's the appropriate way to hide events caused by array of channels?

Post  Sponsored content


Sponsored content


Back to top Go down

View previous topic View next topic Back to top

- Similar topics

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