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 rd0 : Direction.Value
channel wrt0 : 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)


Inst_Cell0 = <(rd,rd0),(wrt,wrt0)> 
Cell0 = rename(BricRingCell, Inst_Cell0) 


GET_CHANNELS(P) =
 	 let f =
 	 < 
	(Cell0, { rd0,wrt0 }),

	(PROT_IMP_Cell0_rd0,{rd0}),

	(PROT_IMP_Cell0_wrt0,{wrt0}) 	 > 

 	 within apply(f,P )

inputs( P ) = 
 	 let f = 
	<
 	 ( Cell0, {| rd0.req,wrt0.req |}),
	(PROT_IMP_Cell0_rd0,inputs_PROT_IMP(Cell0,rd0)),

	(PROT_IMP_Cell0_wrt0,inputs_PROT_IMP(Cell0,wrt0)),

	(PROT_IMP_Cell0_rd0_R_IO_wrt0,inputs_R_IO(PROT_IMP_Cell0_rd0,rd0,wrt0)),

	(PROT_IMP_Cell0_wrt0_R_IO_rd0,inputs_R_IO(PROT_IMP_Cell0_wrt0,wrt0,rd0)),

	(DUAL_PROT_IMP_Cell0_rd0_R_IO_wrt0,outputs(PROT_IMP_Cell0_rd0_R_IO_wrt0)),

	(DUAL_PROT_IMP_Cell0_wrt0_R_IO_rd0,outputs(PROT_IMP_Cell0_wrt0_R_IO_rd0))
 	 > 

 	 within apply(f, P )


 outputs( P ) = 
 	 let f =
	  < 
	 ( Cell0, {| rd0.ack,wrt0.ack |}),
	(PROT_IMP_Cell0_rd0,outputs_PROT_IMP(Cell0,rd0)),

	(PROT_IMP_Cell0_wrt0,outputs_PROT_IMP(Cell0,wrt0)),

	(PROT_IMP_Cell0_rd0_R_IO_wrt0,outputs_R_IO(Cell0,rd0,wrt0)),

	(PROT_IMP_Cell0_wrt0_R_IO_rd0,outputs_R_IO(Cell0,wrt0,rd0)),

	(DUAL_PROT_IMP_Cell0_rd0_R_IO_wrt0,inputs(PROT_IMP_Cell0_rd0_R_IO_wrt0)),

	(DUAL_PROT_IMP_Cell0_wrt0_R_IO_rd0,inputs(PROT_IMP_Cell0_wrt0_R_IO_rd0))
 	 > 

 	 within apply(f, P )

PROT_IMP_Cell0_rd0 = PROT_CELL(rd0)
PROT_IMP_Cell0_wrt0 = PROT_CELL(wrt0)

DUAL_PROT_IMP_Cell0_rd0 = DUAL_PROT_CELL(rd0)
DUAL_PROT_IMP_Cell0_wrt0 = DUAL_PROT_CELL(wrt0)

PROT_IMP_Cell0_rd0_R_IO_wrt0 = PROT_IMP_R(PROT_IMP_Cell0_rd0,R_IO(Cell0,rd0,wrt0))
PROT_IMP_Cell0_wrt0_R_IO_rd0 = PROT_IMP_R(PROT_IMP_Cell0_wrt0,R_IO(Cell0,wrt0,rd0))

DUAL_PROT_IMP_Cell0_rd0_R_IO_wrt0 = DUAL_PROT_IMP_R(DUAL_PROT_IMP_Cell0_rd0,R_IO(Cell0,rd0,wrt0))
DUAL_PROT_IMP_Cell0_wrt0_R_IO_rd0 = DUAL_PROT_IMP_R(DUAL_PROT_IMP_Cell0_wrt0,R_IO(Cell0,wrt0,rd0))

--COMMUNICATION COMPOSITION

Cell0_Cell0 = FEED(Cell0, rd0, wrt0)


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

assert not Cell0 \ {|rd0|} [T= Cell0



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

assert not Cell0 \ {|wrt0|} [T= Cell0

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


assert PROT_IMP_Cell0_rd0 :[divergence free [FD]]

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

assert PROT_IMP_Cell0_rd0 [F= PROT_IMP_def(Cell0,rd0)

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

assert PROT_IMP_def(Cell0,rd0) [FD= PROT_IMP_Cell0_rd0

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


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

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

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

assert InBufferProt(PROT_IMP_Cell0_rd0_R_IO_wrt0, rd0) :[deterministic [F]]

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


assert PROT_IMP_Cell0_wrt0 :[divergence free [FD]]

--D.5.2 

assert PROT_IMP_Cell0_wrt0 [F= PROT_IMP_def(Cell0,wrt0)

--D.5.3 

assert PROT_IMP_def(Cell0,wrt0) [FD= PROT_IMP_Cell0_wrt0

--D.5.4 


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

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

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

assert InBufferProt(PROT_IMP_Cell0_wrt0_R_IO_rd0, wrt0) :[deterministic [F]]

---- D.6: Protocols are Strong Compatible
assert PROT_IMP_Cell0_rd0_R_IO_wrt0 :[deadlock free [FD]]

----	 * D.6.2: Protocols are communication protocols
assert not Test(subseteq(inputs(PROT_IMP_Cell0_rd0_R_IO_wrt0), {| rd0|})) [T= ERROR
assert not Test(subseteq(outputs(PROT_IMP_Cell0_rd0_R_IO_wrt0), {|wrt0|})) [T= ERROR
assert not Test(inputs(PROT_IMP_Cell0_rd0_R_IO_wrt0) == outputs(DUAL_PROT_IMP_Cell0_rd0_R_IO_wrt0)) [T= ERROR

assert not Test(outputs(PROT_IMP_Cell0_rd0_R_IO_wrt0) == inputs(DUAL_PROT_IMP_Cell0_rd0_R_IO_wrt0)) [T= ERROR

assert DUAL_PROT_IMP_Cell0_rd0_R_IO_wrt0 [T= PROT_IMP_Cell0_rd0_R_IO_wrt0

assert PROT_IMP_Cell0_rd0_R_IO_wrt0 [T= DUAL_PROT_IMP_Cell0_rd0_R_IO_wrt0



assert DUAL_PROT_IMP_Cell0_rd0_R_IO_wrt0 [F= PROT_IMP_Cell0_wrt0_R_IO_rd0



assert PROT_IMP_Cell0_wrt0_R_IO_rd0 [F= DUAL_PROT_IMP_Cell0_rd0_R_IO_wrt0

---- D.6: Protocols are Strong Compatible
assert PROT_IMP_Cell0_rd0_R_IO_wrt0 :[deadlock free [FD]]

----	 * D.6.2: Protocols are communication protocols
assert not Test(subseteq(inputs(PROT_IMP_Cell0_rd0_R_IO_wrt0), {| rd0|})) [T= ERROR
assert not Test(subseteq(outputs(PROT_IMP_Cell0_rd0_R_IO_wrt0), {|wrt0|})) [T= ERROR
assert not Test(inputs(PROT_IMP_Cell0_rd0_R_IO_wrt0) == outputs(DUAL_PROT_IMP_Cell0_rd0_R_IO_wrt0)) [T= ERROR

assert not Test(outputs(PROT_IMP_Cell0_rd0_R_IO_wrt0) == inputs(DUAL_PROT_IMP_Cell0_rd0_R_IO_wrt0)) [T= ERROR

assert DUAL_PROT_IMP_Cell0_rd0_R_IO_wrt0 [T= PROT_IMP_Cell0_rd0_R_IO_wrt0

assert PROT_IMP_Cell0_rd0_R_IO_wrt0 [T= DUAL_PROT_IMP_Cell0_rd0_R_IO_wrt0



assert DUAL_PROT_IMP_Cell0_rd0_R_IO_wrt0 [F= PROT_IMP_Cell0_wrt0_R_IO_rd0



assert PROT_IMP_Cell0_wrt0_R_IO_rd0 [F= DUAL_PROT_IMP_Cell0_rd0_R_IO_wrt0

assert PROT_IMP_Cell0_wrt0_R_IO_rd0 :[deadlock free [FD]]

assert not Test(subseteq(inputs(PROT_IMP_Cell0_wrt0_R_IO_rd0), {| wrt0|})) [T= ERROR
assert not Test(subseteq(outputs(PROT_IMP_Cell0_wrt0_R_IO_rd0), {| rd0|})) [T= ERROR
assert not Test(inputs(PROT_IMP_Cell0_wrt0_R_IO_rd0) == outputs(DUAL_PROT_IMP_Cell0_wrt0_R_IO_rd0)) [T= ERROR
assert not Test(outputs(PROT_IMP_Cell0_wrt0_R_IO_rd0) == inputs(DUAL_PROT_IMP_Cell0_wrt0_R_IO_rd0)) [T= ERROR
assert DUAL_PROT_IMP_Cell0_wrt0_R_IO_rd0 [T= PROT_IMP_Cell0_wrt0_R_IO_rd0

assert PROT_IMP_Cell0_wrt0_R_IO_rd0 [T= DUAL_PROT_IMP_Cell0_wrt0_R_IO_rd0



assert DUAL_PROT_IMP_Cell0_wrt0_R_IO_rd0 [F= PROT_IMP_Cell0_rd0_R_IO_wrt0



assert PROT_IMP_Cell0_rd0_R_IO_wrt0 [F= DUAL_PROT_IMP_Cell0_wrt0_R_IO_rd0

--D.7: Protocols have Finite Output Property 

--D.7.1

assert PROT_IMP_Cell0_rd0_R_IO_wrt0 \  outputs(PROT_IMP_Cell0_rd0_R_IO_wrt0):[divergence free [FD]]

assert PROT_IMP_Cell0_wrt0_R_IO_rd0 \  outputs(PROT_IMP_Cell0_wrt0_R_IO_rd0):[divergence free [FD]]

assert INTER_PROT_IMP(PROT_IMP_Cell0_rd0, {rd0, wrt0}) [F= PROJECTION(Cell0, {rd0, wrt0})

assert PROJECTION(Cell0, {rd0, wrt0}) [FD= INTER_PROT_IMP(PROT_IMP_Cell0_rd0, {rd0, wrt0})

assert INTER_PROT_IMP(PROT_IMP_Cell0_wrt0, {rd0, wrt0}) [F= PROJECTION(Cell0, {rd0, wrt0})

assert PROJECTION(Cell0, {rd0, wrt0}) [FD= INTER_PROT_IMP(PROT_IMP_Cell0_wrt0, {rd0, wrt0})