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

[alex2ren]

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]

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"};

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]

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

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"};

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;

[Sponsored content]