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 rd1 : Direction.Value
channel wrt1 : 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 <- rd1,wrt <- wrt1]] 


BricIRCell2 = BricRingCell [[rd <- rd2,wrt <- wrt2]] 

Inst_Cell1 = <(rd,rd1),(wrt,wrt1)> 
Cell1 = rename(BricRingCell, Inst_Cell1) 

Inst_Cell2 = <(rd,rd2),(wrt,wrt2)> 
Cell2 = rename(BricRingCell, Inst_Cell2) 


GET_CHANNELS(P) =
 	 let f =
 	 < 
	(Cell1, { rd1,wrt1 }),

	(Cell2, { rd2,wrt2 }),

	(PROT_IMP_Cell1_rd1,{rd1}),

	(PROT_IMP_Cell2_rd2,{rd2}) 	 > 

 	 within apply(f,P )

inputs( P ) = 
 	 let f = 
	<
 	 ( Cell1, {| rd1.req,wrt1.req |}),
 	 ( Cell2, {| rd2.req,wrt2.req |}),
	(PROT_IMP_Cell1_rd1,inputs_PROT_IMP(Cell1,rd1)),

	(PROT_IMP_Cell2_rd2,inputs_PROT_IMP(Cell2,rd2)),

	(PROT_IMP_Cell1_rd1_R_IO_rd2,inputs_R_IO(PROT_IMP_Cell1_rd1,rd1,rd2)),

	(PROT_IMP_Cell2_rd2_R_IO_rd1,inputs_R_IO(PROT_IMP_Cell2_rd2,rd2,rd1)),

	(DUAL_PROT_IMP_Cell1_rd1_R_IO_rd2,outputs(PROT_IMP_Cell1_rd1,rd1,rd2)),

	(DUAL_PROT_IMP_Cell2_rd2_R_IO_rd1,outputs(PROT_IMP_Cell2_rd2,rd2,rd1))
 	 > 

 	 within apply(f, P )


 outputs( P ) = 
 	 let f =
	  < 
	 ( Cell1, {| rd1.ack,wrt1.ack |}),
	 ( Cell2, {| rd2.ack,wrt2.ack |}),
	(PROT_IMP_Cell1_rd1,outputs_PROT_IMP(Cell1,rd1)),

	(PROT_IMP_Cell2_rd2,outputs_PROT_IMP(Cell2,rd2)),

	(PROT_IMP_Cell1_rd1_R_IO_rd2,outputs_R_IO(PROT_IMP_Cell1_rd1,rd1,rd2)),

	(PROT_IMP_Cell2_rd2_R_IO_rd1,outputs_R_IO(PROT_IMP_Cell2_rd2,rd2,rd1)),

	(DUAL_PROT_IMP_Cell1_rd1_R_IO_rd2,inputs(PROT_IMP_Cell1_rd1_R_IO_rd2)),

	(DUAL_PROT_IMP_Cell2_rd2_R_IO_rd1,inputs(PROT_IMP_Cell2_rd2_R_IO_rd1))
 	 > 

 	 within apply(f, P )

PROT_IMP_Cell1_rd1 = PROT_CELL(rd1)
PROT_IMP_Cell2_rd2 = PROT_CELL(rd2)

DUAL_PROT_IMP_Cell1_rd1 = DUAL_PROT_CELL(rd1)
DUAL_PROT_IMP_Cell2_rd2 = DUAL_PROT_CELL(rd2)



--COMMUNICATION COMPOSITION

Cell1_Cell2 = COMM(Cell1, Cell2, rd1, wrt2)


--D.1 channel1 is in the alphabet of contract

assert not Cell1 \ {|rd1|} [T= Cell1



--D.2 channel2 is in the alphabet of contract

assert not Cell2 \ {|rd2|} [T= Cell2



--D.3:Alphabets are disjont

assert STOP [T= RUN(inter(events(Cell1),events(Cell2)))

--D.4 : I/O confluence for first component
--D.4.1 It is divergence-free


assert PROT_IMP_Cell1_rd1 :[divergence free [FD]]

--D.4.2 It is refined by the projection on the channel 

assert PROT_IMP_Cell1_rd1 [F= PROT_IMP_def(Cell1,rd1)

--D.4.3 It is a refinement of the projection on the channel 

assert PROT_IMP_def(Cell1,rd1) [FD= PROT_IMP_Cell1_rd1

--D.4.4 It is a port-protocol (communication protocol) 


--D.4.4.1 
assert not Test(subseteq(inputs_PROT_IMP(Cell1,rd1),{|rd1|})) [T= ERROR

--D.4.4.2 
assert not Test(subseteq(outputs_PROT_IMP(Cell1,rd1),{|rd1|})) [T= ERROR

--D.4.5 : The renamed version is I/O Confluent

PROT_IMP_Cell1_rd1_R_IO_rd2 = PROT_IMP_R(PROT_IMP_Cell1_rd1,R_IO(Cell1,rd1,rd2))
PROT_IMP_Cell2_rd2_R_IO_rd1 = PROT_IMP_R(PROT_IMP_Cell2_rd2,R_IO(Cell2,rd2,rd1))

assert InBufferProt(PROT_IMP_Cell1_rd1_R_IO_rd2, rd1) :[deterministic [F]]

--D.5 : I/O confluence for second component 
--D.5.1 


assert PROT_IMP_Cell2_rd2 :[divergence free [FD]]

--D.5.2 

assert PROT_IMP_Cell2_rd2 [F= PROT_IMP_def(Cell2,rd2)

--D.5.3 

assert PROT_IMP_def(Cell2,rd2) [FD= PROT_IMP_Cell2_rd2

--D.5.4 


--D.5.4.1 
assert not Test(subseteq(inputs_PROT_IMP(Cell2,rd2),{|rd2|})) [T= ERROR

--D.5.4.2 
assert not Test(subseteq(outputs_PROT_IMP(Cell2,rd2),{|rd2|})) [T= ERROR

--D.5.5 : The renamed version is I/O Confluent

PROT_IMP_Cell2_rd2_R_IO_rd1 = PROT_IMP_R(PROT_IMP_Cell2_rd2,R_IO(Cell2,rd2,rd1))

assert InBufferProt(PROT_IMP_Cell2_rd2_R_IO_rd1, rd2) :[deterministic [F]]

---- D.6: Protocols are Strong Compatible

----	     * Condition D.6.1.1: Left

assert PROT_IMP_Cell1_rd1_R_IO_rd2 :[deadlock free [FD]]

----	     * Condition D.6.1.2: Right

assert PROT_IMP_Cell2_rd2_R_IO_rd1 :[deadlock free [FD]]

----	 * D.6.2: Protocols are communication protocols

--D.6.2.1
assert not Test(subseteq(inputs(PROT_IMP_Cell1_rd1_R_IO_rd2), {| rd1|})) [T= ERROR

--D.6.2.2
assert not Test(subseteq(outputs(PROT_IMP_Cell1_rd1_R_IO_rd2), {|rd2|})) [T= ERROR

--D.6.2.3
assert not Test(subseteq(inputs(PROT_IMP_Cell2_rd2_R_IO_rd1), {| rd2|})) [T= ERROR

--D.6.2.4
assert not Test(subseteq(outputs(PROT_IMP_Cell2_rd2_R_IO_rd1), {| rd1|})) [T= ERROR

--D.6.3: It is a Dual Protocol

DUAL_PROT_IMP_Cell1_rd1_R_IO_rd2 = DUAL_PROT_IMP_R(Cell1,rd1,R_IO(Cell1,rd1,rd2))
DUAL_PROT_IMP_Cell2_rd2_R_IO_rd1 = DUAL_PROT_IMP_R(Cell2,rd2,R_IO(Cell2,rd2,rd1))
--D.6.3.1

assert not Test(inputs(PROT_IMP_Cell1_rd1_R_IO_rd2) == outputs(DUAL_PROT_IMP_Cell1_rd1_R_IO_rd2)) [T= ERROR

--D.6.3.2

assert not Test(outputs(PROT_IMP_Cell2_rd2_R_IO_rd1) == inputs(DUAL_PROT_IMP_Cell1_rd1_R_IO_rd2)) [T= ERROR

--D.6.3.3:

--D.6.3.3.1:
assert DUAL_PROT_IMP_Cell1_rd1_R_IO_rd2 [T= PROT_IMP_Cell1_rd1_R_IO_rd2

--D.6.3.3.2:
assert PROT_IMP_Cell1_rd1_R_IO_rd2 [T= DUAL_PROT_IMP_Cell1_rd1_R_IO_rd2

--D.6.4:

--DEFINITION: PROTOCOLS ARE STRONG COMPATIBLE if the DUAL PROTOCOL of one is refined (in Failures) by the other

assert DUAL_PROT_IMP_Cell1_rd1_R_IO_rd2 [F= PROT_IMP_Cell2_rd2_R_IO_rd1

--D.6.5

--DEFINITION: PROTOCOLS ARE MATCHING COMPATIBLE if the DUAL PROTOCOL of one is equivalent (in Failures) to the other
assert PROT_IMP_Cell2_rd2_R_IO_rd1 [F= DUAL_PROT_IMP_Cell1_rd1_R_IO_rd2