include "sequence_aux.csp" 
  include "function_aux.csp" 
  include "auxiliar.csp" 
  include "rules.csp"
  datatype Direction = req | ack
  Value = {1..3}
  channel rd : Direction.Value
  channel wrt : Direction.Value
  
  
  BricRingCell = wrt.req?x -> wrt.ack.x -> rd.req?dumb -> rd.ack!x -> BricRingCell
  
  
  
  channel rd2 : Direction.Value
  channel wrt2 : Direction.Value
  channel rd2 : Direction.Value
  channel wrt2 : Direction.Value
  
  
  PROT_CELL(e) = |~| v2:Value @ e.req?v1 -> e.ack.v2 -> PROT_CELL(e)
  DUAL_PROT_CELL(e) = |~| v1:Value @ e.req.v1 -> e.ack?v2 -> DUAL_PROT_CELL(e)
  
  
  BricIRCell1 = BricRingCell [[rd <- rd2,wrt <- wrt2]] 
  
  
  BricIRCell2 = BricRingCell [[rd <- rd2,wrt <- wrt2]] 
  
  Inst_Cell2 = <(rd,rd2),(wrt,wrt2)> 
  Cell2 = rename(BricRingCell, Inst_Cell2) 
  
  Inst_Cell2 = <(rd,rd2),(wrt,wrt2)> 
  Cell2 = rename(BricRingCell, Inst_Cell2) 
  
  
  GET_CHANNELS(P) =
   	 let f =
   	 < 
  	(Cell2, { rd2,wrt2 }),
  
  	(Cell2, { rd2,wrt2 }),
  
  	(PROT_IMP_Cell2_rd2,{rd2}),
  
  	(PROT_IMP_Cell2_wrt2,{wrt2}) 	 > 
  
   	 within apply(f,P )
  
  inputs( P ) = 
   	 let f = 
  	<
   	 ( Cell2, {| rd2.req,wrt2.req |}),
   	 ( Cell2, {| rd2.req,wrt2.req |}),
  	(PROT_IMP_Cell2_rd2,inputs_PROT_IMP(Cell2,rd2)),
  
  	(PROT_IMP_Cell2_wrt2,inputs_PROT_IMP(Cell2,wrt2)),
  
  	(PROT_IMP_Cell2_rd2_R_IO_wrt2,inputs_R_IO(PROT_IMP_Cell2_rd2,rd2,wrt2)),
  
  	(PROT_IMP_Cell2_wrt2_R_IO_rd2,inputs_R_IO(PROT_IMP_Cell2_wrt2,wrt2,rd2)),
  
  	(DUAL_PROT_IMP_Cell2_rd2_R_IO_wrt2,outputs(PROT_IMP_Cell2_rd2_R_IO_wrt2)),
  
  	(DUAL_PROT_IMP_Cell2_wrt2_R_IO_rd2,outputs(PROT_IMP_Cell2_wrt2_R_IO_rd2))
   	 > 
  
   	 within apply(f, P )
  
  
   outputs( P ) = 
   	 let f =
  	  < 
  	 ( Cell2, {| rd2.ack,wrt2.ack |}),
  	 ( Cell2, {| rd2.ack,wrt2.ack |}),
  	(PROT_IMP_Cell2_rd2,outputs_PROT_IMP(Cell2,rd2)),
  
  	(PROT_IMP_Cell2_wrt2,outputs_PROT_IMP(Cell2,wrt2)),
  
  	(PROT_IMP_Cell2_rd2_R_IO_wrt2,outputs_R_IO(Cell2,rd2,wrt2)),
  
  	(PROT_IMP_Cell2_wrt2_R_IO_rd2,outputs_R_IO(Cell2,wrt2,rd2)),
  
  	(DUAL_PROT_IMP_Cell2_rd2_R_IO_wrt2,inputs(PROT_IMP_Cell2_rd2_R_IO_wrt2)),
  
  	(DUAL_PROT_IMP_Cell2_wrt2_R_IO_rd2,inputs(PROT_IMP_Cell2_wrt2_R_IO_rd2))
   	 > 
  
   	 within apply(f, P )
  
  PROT_IMP_Cell2_rd2 = PROT_CELL(rd2)
  PROT_IMP_Cell2_wrt2 = PROT_CELL(wrt2)
  
  DUAL_PROT_IMP_Cell2_rd2 = DUAL_PROT_CELL(rd2)
  DUAL_PROT_IMP_Cell2_wrt2 = DUAL_PROT_CELL(wrt2)
  
  PROT_IMP_Cell2_rd2_R_IO_wrt2 = PROT_IMP_R(PROT_IMP_Cell2_rd2,R_IO(Cell2,rd2,wrt2))
  PROT_IMP_Cell2_wrt2_R_IO_rd2 = PROT_IMP_R(PROT_IMP_Cell2_wrt2,R_IO(Cell2,wrt2,rd2))
  
  DUAL_PROT_IMP_Cell2_rd2_R_IO_wrt2 = DUAL_PROT_IMP_R(DUAL_PROT_IMP_Cell2_rd2,R_IO(Cell2,rd2,wrt2))
  DUAL_PROT_IMP_Cell2_wrt2_R_IO_rd2 = DUAL_PROT_IMP_R(DUAL_PROT_IMP_Cell2_wrt2,R_IO(Cell2,wrt2,rd2))
  
  --COMMUNICATION COMPOSITION
  
  Cell2_Cell2 = FEED(Cell2, rd2, wrt2)
  
  
  --D.1 channel1 is in the alphabet of contract
  
  assert not Cell2 \ {|rd2|} [T= Cell2
  
  
  
  --D.1 channel1 is in the alphabet of contract
  
  assert not Cell2 \ {|wrt2|} [T= Cell2
  
  --D.4 : I/O confluence for first component
  --D.4.1 It is divergence-free
  
  
  assert PROT_IMP_Cell2_rd2 :[divergence free [FD]]
  
  --D.4.2 It is refined by the projection on the channel 
  
  assert PROT_IMP_Cell2_rd2 [F= PROT_IMP_def(Cell2,rd2)
  
  --D.4.3 It is a refinement of the projection on the channel 
  
  assert PROT_IMP_def(Cell2,rd2) [FD= PROT_IMP_Cell2_rd2
  
  --D.4.4 It is a port-protocol (communication protocol) 
  
  
  --D.4.4.1 
  assert not Test(subseteq(inputs_PROT_IMP(Cell2,rd2),{|rd2|})) [T= ERROR
  
  --D.4.4.2 
  assert not Test(subseteq(outputs_PROT_IMP(Cell2,rd2),{|rd2|})) [T= ERROR
  
  --D.4.5 : The renamed version is I/O Confluent
  
  assert InBufferProt(PROT_IMP_Cell2_rd2_R_IO_wrt2, rd2) :[deterministic [F]]
  
  --D.5 : I/O confluence for second component 
  --D.5.1 
  
  
  assert PROT_IMP_Cell2_wrt2 :[divergence free [FD]]
  
  --D.5.2 
  
  assert PROT_IMP_Cell2_wrt2 [F= PROT_IMP_def(Cell2,wrt2)
  
  --D.5.3 
  
  assert PROT_IMP_def(Cell2,wrt2) [FD= PROT_IMP_Cell2_wrt2
  
  --D.5.4 
  
  
  --D.5.4.1 
  assert not Test(subseteq(inputs_PROT_IMP(Cell2,wrt2),{|wrt2|})) [T= ERROR
  
  --D.5.4.2 
  assert not Test(subseteq(outputs_PROT_IMP(Cell2,wrt2),{|wrt2|})) [T= ERROR
  
  --D.5.5 : The renamed version is I/O Confluent
  
  assert InBufferProt(PROT_IMP_Cell2_wrt2_R_IO_rd2, wrt2) :[deterministic [F]]
  
  ---- D.6: Protocols are Strong Compatible
  
  assert PROT_IMP_Cell2_rd2_R_IO_wrt2 :[deadlock free [FD]]
  
  assert PROT_IMP_Cell2_wrt2_R_IO_rd2 :[deadlock free [FD]]
  
  ----	 * D.6.2: Protocols are communication protocols
  
  --D.6.2.1
  assert not Test(subseteq(inputs(PROT_IMP_Cell2_rd2_R_IO_wrt2), {| rd2|})) [T= ERROR
  
  --D.6.2.2
  assert not Test(subseteq(outputs(PROT_IMP_Cell2_rd2_R_IO_wrt2), {|wrt2|})) [T= ERROR
  
  --D.6.2.3
  assert not Test(subseteq(inputs(PROT_IMP_Cell2_wrt2_R_IO_rd2), {| wrt2|})) [T= ERROR
  
  --D.6.2.4
  assert not Test(subseteq(outputs(PROT_IMP_Cell2_wrt2_R_IO_rd2), {| rd2|})) [T= ERROR
  
  --D.6.3: It is a Dual Protocol
  
  
  
  assert not Test(inputs(PROT_IMP_Cell2_rd2_R_IO_wrt2) == outputs(DUAL_PROT_IMP_Cell2_rd2_R_IO_wrt2)) [T= ERROR
  
  
  
  assert not Test(outputs(PROT_IMP_Cell2_wrt2_R_IO_rd2) == inputs(DUAL_PROT_IMP_Cell2_wrt2_R_IO_rd2)) [T= ERROR
  
  
  
  assert DUAL_PROT_IMP_Cell2_rd2_R_IO_wrt2 [T= PROT_IMP_Cell2_rd2_R_IO_wrt2
  
  assert PROT_IMP_Cell2_rd2_R_IO_wrt2 [T= DUAL_PROT_IMP_Cell2_rd2_R_IO_wrt2
  
  
  
  assert DUAL_PROT_IMP_Cell2_rd2_R_IO_wrt2 [F= PROT_IMP_Cell2_wrt2_R_IO_rd2
  
  
  
  assert PROT_IMP_Cell2_wrt2_R_IO_rd2 [F= DUAL_PROT_IMP_Cell2_rd2_R_IO_wrt2
  
  --D.7: Protocols have Finite Output Property 
  
  --D.7.1
  
  assert PROT_IMP_Cell2_rd2_R_IO_wrt2 \  outputs(PROT_IMP_Cell2_rd2_R_IO_wrt2):[divergence free [FD]]
  
  assert PROT_IMP_Cell2_wrt2_R_IO_rd2 \  outputs(PROT_IMP_Cell2_wrt2_R_IO_rd2):[divergence free [FD]]
  
  assert INTER_PROT_IMP(Cell2, {rd2, wrt2}) [F= PROJECTION(Cell2, {rd2, wrt2})
  
  assert PROJECTION(Cell2, {rd2, wrt2}) [FD= INTER_PROT_IMP(Cell2, {rd2, wrt2})