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
channel rd1 : Direction.Value
channel wrt1 : 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 <- rd0,wrt <- wrt0]]
BricIRCell2 = BricRingCell [[rd <- rd1,wrt <- wrt1]]
Inst_Cell0 = <(rd,rd0),(wrt,wrt0)>
Cell0 = rename(BricRingCell, Inst_Cell0)
Inst_Cell1 = <(rd,rd1),(wrt,wrt1)>
Cell1 = rename(BricRingCell, Inst_Cell1)
GET_CHANNELS(P) =
let f =
<
(Cell0, { rd0,wrt0 }),
(Cell1, { rd1,wrt1 }),
(PROT_IMP_Cell0_rd0,{rd0}),
(PROT_IMP_Cell1_rd1,{rd1}) >
within apply(f,P )
inputs( P ) =
let f =
<
( Cell0, {| rd0.req,wrt0.req |}),
( Cell1, {| rd1.req,wrt1.req |}),
(PROT_IMP_Cell0_rd0,inputs_PROT_IMP(Cell0,rd0)),
(PROT_IMP_Cell1_rd1,inputs_PROT_IMP(Cell1,rd1)),
(PROT_IMP_Cell0_rd0_R_IO_rd1,inputs_R_IO(PROT_IMP_Cell0_rd0,rd0,rd1)),
(PROT_IMP_Cell1_rd1_R_IO_rd0,inputs_R_IO(PROT_IMP_Cell1_rd1,rd1,rd0)),
(DUAL_PROT_IMP_Cell0_rd0_R_IO_rd1,outputs(PROT_IMP_Cell0_rd0_R_IO_rd1)),
(DUAL_PROT_IMP_Cell1_rd1_R_IO_rd0,outputs(PROT_IMP_Cell1_rd1_R_IO_rd0))
>
within apply(f, P )
outputs( P ) =
let f =
<
( Cell0, {| rd0.ack,wrt0.ack |}),
( Cell1, {| rd1.ack,wrt1.ack |}),
(PROT_IMP_Cell0_rd0,outputs_PROT_IMP(Cell0,rd0)),
(PROT_IMP_Cell1_rd1,outputs_PROT_IMP(Cell1,rd1)),
(PROT_IMP_Cell0_rd0_R_IO_rd1,outputs_R_IO(Cell0,rd0,rd1)),
(PROT_IMP_Cell1_rd1_R_IO_rd0,outputs_R_IO(Cell0,rd1,rd0)),
(DUAL_PROT_IMP_Cell0_rd0_R_IO_rd1,inputs(PROT_IMP_Cell0_rd0_R_IO_rd1)),
(DUAL_PROT_IMP_Cell1_rd1_R_IO_rd0,inputs(PROT_IMP_Cell1_rd1_R_IO_rd0))
>
within apply(f, P )
PROT_IMP_Cell0_rd0 = PROT_CELL(rd0)
PROT_IMP_Cell1_rd1 = PROT_CELL(rd1)
DUAL_PROT_IMP_Cell0_rd0 = DUAL_PROT_CELL(rd0)
DUAL_PROT_IMP_Cell1_rd1 = DUAL_PROT_CELL(rd1)
PROT_IMP_Cell0_rd0_R_IO_rd1 = PROT_IMP_R(PROT_IMP_Cell0_rd0,R_IO(Cell0,rd0,rd1))
PROT_IMP_Cell1_rd1_R_IO_rd0 = PROT_IMP_R(PROT_IMP_Cell1_rd1,R_IO(Cell1,rd1,rd0))
DUAL_PROT_IMP_Cell0_rd0_R_IO_rd1 = DUAL_PROT_IMP_R(DUAL_PROT_IMP_Cell0_rd0,R_IO(Cell0,rd0,rd1))
DUAL_PROT_IMP_Cell1_rd1_R_IO_rd0 = DUAL_PROT_IMP_R(DUAL_PROT_IMP_Cell1_rd1,R_IO(Cell1,rd1,rd0))
--COMMUNICATION COMPOSITION
Cell0_Cell1 = COMM(Cell0, Cell1, rd0, wrt1)
--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 Cell1 \ {|rd1|} [T= Cell1
--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_rd1, rd0) :[deterministic [F]]
--D.5 : I/O confluence for second component
--D.5.1
assert PROT_IMP_Cell1_rd1 :[divergence free [FD]]
--D.5.2
assert PROT_IMP_Cell1_rd1 [F= PROT_IMP_def(Cell1,rd1)
--D.5.3
assert PROT_IMP_def(Cell1,rd1) [FD= PROT_IMP_Cell1_rd1
--D.5.4
--D.5.4.1
assert not Test(subseteq(inputs_PROT_IMP(Cell1,rd1),{|rd1|})) [T= ERROR
--D.5.4.2
assert not Test(subseteq(outputs_PROT_IMP(Cell1,rd1),{|rd1|})) [T= ERROR
--D.5.5 : The renamed version is I/O Confluent
assert InBufferProt(PROT_IMP_Cell1_rd1_R_IO_rd0, rd1) :[deterministic [F]]
---- D.6: Protocols are Strong Compatible
assert PROT_IMP_Cell0_rd0_R_IO_rd1 :[deadlock free [FD]]
assert PROT_IMP_Cell1_rd1_R_IO_rd0 :[deadlock free [FD]]
---- * D.6.2: Protocols are communication protocols
--D.6.2.1
assert not Test(subseteq(inputs(PROT_IMP_Cell0_rd0_R_IO_rd1), {| rd0|})) [T= ERROR
--D.6.2.2
assert not Test(subseteq(outputs(PROT_IMP_Cell0_rd0_R_IO_rd1), {|rd1|})) [T= ERROR
--D.6.2.3
assert not Test(subseteq(inputs(PROT_IMP_Cell1_rd1_R_IO_rd0), {| rd1|})) [T= ERROR
--D.6.2.4
assert not Test(subseteq(outputs(PROT_IMP_Cell1_rd1_R_IO_rd0), {| rd0|})) [T= ERROR
--D.6.3: It is a Dual Protocol
--D.6.3.1
assert not Test(inputs(PROT_IMP_Cell0_rd0_R_IO_rd1) == outputs(DUAL_PROT_IMP_Cell0_rd0_R_IO_rd1)) [T= ERROR
--D.6.3.2
assert not Test(outputs(PROT_IMP_Cell1_rd1_R_IO_rd0) == inputs(DUAL_PROT_IMP_Cell0_rd0_R_IO_rd1)) [T= ERROR
--D.6.3.3:
--D.6.3.3.1:
assert DUAL_PROT_IMP_Cell0_rd0_R_IO_rd1 [T= PROT_IMP_Cell0_rd0_R_IO_rd1
--D.6.3.3.2:
assert PROT_IMP_Cell0_rd0_R_IO_rd1 [T= DUAL_PROT_IMP_Cell0_rd0_R_IO_rd1
--D.6.4:
assert DUAL_PROT_IMP_Cell0_rd0_R_IO_rd1 [F= PROT_IMP_Cell1_rd1_R_IO_rd0
--D.6.5
assert PROT_IMP_Cell1_rd1_R_IO_rd0 [F= DUAL_PROT_IMP_Cell0_rd0_R_IO_rd1