%%ext_atomic=false
%%MinI = 0
%%MaxI = 8
%%InitB = false
%%InitI = MinI
%%ditype = {1..N}
%%dctype = {MinI..MaxI}

sig send1:int;
sig send2:int; 
sig receive1:int; 
sig receive2:int;

Psva(i) = iter {
 sig(send1.i);
 sig(send2.1);
 sig(receive1.i);
 sig(receive2.1);
}


PsvaC = < Psva(1) >

%%dom(m) = { x | (x,y)<-m }
%%MaxT(<>) = SKIP
%%MaxT(s) = head(s) -> MaxT(tail(s))
%%Linker(map) = [] s : dom(map) @ MaxT(s); [] e : { e | (s1,e) <- map, s==s1 } @ e -> Linker(map)
%%MapEvs(Psva,map) = ( Psva [|Signals|] Linker(map) ) \ Signals
%%
%%channel send, receive : {1}.{1}
%%P(i) = send.i.1 -> receive.i.1 -> P(i)
%%P_ = P(1)
%%
%%MAP = { (<send1.1, send2.1>, send.1.1), (<receive1.1, receive2.1>, receive.1.1) }

assert %- P_ [T= MapEvs(PsvaC,MAP) -% in PsvaC
assert %- MapEvs(PsvaC,MAP) [T= P_ -% in PsvaC