include "auxiliar.csp" 
include "rules.csp"

datatype Direction = req | ack
Value = {1..3}
channel write : Direction.Value
channel read : Direction.Value

BricRingCell = write.req?x -> write.ack.x -> read.req?dumb -> read.ack!x -> BricRingCell
channel write2 : Direction.Value
channel read2 : Direction.Value
channel write3 : Direction.Value
channel read3 : Direction.Value

Rename1(i) = BricRingCell [[write <- write2,read <- read2]] 


Rename2(i) = BricRingCell [[write <- write3,read <- read3]] 
Inst_Cell2 = <(write,write2),(read,read2)> 
Cell2 = rename(BricRingCell, Inst_Cell2) 

Inst_Cell3 = <(write,write3),(read,read3)> 
Cell3 = rename(BricRingCell, Inst_Cell3) 


GET_CHANNELS(P) =
 	 let f =
 	 < 
	(Cell2, { write2,read2 }),

	(Cell3, { write3,read3 })

 	 > 

 	 within apply(f,P )

inputs( P ) = 
 	 let f = 
	<
 	 ( Cell2, {| write2.req,read2.req |}),
 	 ( Cell3, {| write3.req,read3.req |})
 	 > 

 	 within apply(f, P )
 outputs( P ) = 
 	 let f =
	  < 
	 ( Cell2, {| write2.ack,read2.ack |}),
	 ( Cell3, {| write3.ack,read3.ack |})
 	 >
 	 within apply(f, P )

--INTERLEAVING COMPOSITION 
newComponent = INTER(Cell2,Cell3) 
assert STOP [T= RUN(inter(events(Cell2),events(Cell3)))
assert newComponent:[deadlock free[FD]]