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

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

BUF = write.req?x -> read.req.x -> write.ack!x -> read.ack.x -> BUF
channel write0 : Direction.Value
channel read0 : Direction.Value
channel write1 : Direction.Value
channel read1 : Direction.Value

Rename1(i) = BUF [[write <- write0,read <- read0]] 


Rename2(i) = BUF [[write <- write1,read <- read1]] 
Inst_BUF0 = <(write,write0),(read,read0)> 
BUF0 = rename(BUF, Inst_BUF0) 

Inst_BUF1 = <(write,write1),(read,read1)> 
BUF1 = rename(BUF, Inst_BUF1) 


GET_CHANNELS(P) =
 	 let f =
 	 < 
	(BUF0, { write0,read0 }),

	(BUF1, { write1,read1 })

 	 > 

 	 within apply(f,P )

inputs( P ) = 
 	 let f = 
	<
 	 ( BUF0, {| write0.req,read0.req |}),
 	 ( BUF1, {| write1.req,read1.req |})
 	 > 

 	 within apply(f, P )
 outputs( P ) = 
 	 let f =
	  < 
	 ( BUF0, {| write0.ack,read0.ack |}),
	 ( BUF1, {| write1.ack,read1.ack |})
 	 >
 	 within apply(f, P )

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