include "sequence_aux.csp" include "function_aux.csp" include "auxiliar.csp" include "rules.csp" datatype Direction = req | ack Value = {1..3} CellId = {0..3} channel rd : Direction.Value channel wrt : Direction.Value channel write : CellId.Direction.Value channel read : CellId.Direction.Value channel input : Value channel output : Value BricRingCell = wrt.req?x -> wrt.ack.x -> rd.req?dumb -> rd.ack!x -> BricRingCell maxbuff = 4 maxring = maxbuff - 1 Controller = let ControllerState(cache,size,top,bot) = InputController(cache,size,top,bot) [] OutputController(cache,size,top,bot) InputController(cache,size,top,bot) = size < maxbuff & input?x -> (size == 0 & ControllerState(x,1,top,bot) [] size > 0 & write.top.req!x -> write.top.ack?dumb -> ControllerState(cache,size+1,(top%maxring)+1,bot)) OutputController(cache,size,top,bot) = size > 0 & output!cache -> (size > 1 & -- A requisição de leitura não ser uma "escolha externa (via input on dumb)" para que o processo seja Strong Output Decisive -- read.bot.req?dumb -> read.bot.ack?x -> ControllerState(x,size-1,top,(bot%maxring)+1) (|~| dumb:Value @ read.bot.req.dumb -> read.bot.ack?x -> ControllerState(x,size-1,top,(bot%maxring)+1)) [] size == 1 & ControllerState(cache,0,top,bot)) within -- The initial value of the cache is irrelevant, since the size is 0. ControllerState(0,0,1,1) channel rd0 : Direction.Value channel wrt0 : Direction.Value channel input3 : Value channel output3 : Value channel write3 : CellId.Direction.Value channel read3 : CellId.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) PROT_CTRL(e) = |~| v1:Value @ e.req.v1 -> e.ack?v2 -> PROT_CTRL(e) DUAL_PROT_CTRL(e) = |~| v2:Value @ e.req?v1 -> e.ack.v2 -> DUAL_PROT_CTRL(e) Inst_Cell0 = <(rd,rd0),(wrt,wrt0)> Cell0 = rename(BricRingCell, Inst_Cell0) Inst_Controller3 = <(input,input3),(output,output3),(write,write3),(read,read3)> Controller3 = rename(Controller, Inst_Controller3) GET_CHANNELS(P) = let f = < (Cell0, { rd0,wrt0 }), (Controller3, { input3,output3,write3,read3 }), (PROT_IMP_Cell0_wrt0,{wrt0}), (PROT_IMP_Controller3_write3,{write3}) > within apply(f,P ) inputs( P ) = let f = < ( Cell0, {| rd0.req,wrt0.req |}), ( Controller3, {| input3,write3.1.ack,write3.2.ack,write3.3.ack,read3.1.ack,read3.2.ack,read3.3.ack |}), (PROT_IMP_Cell0_wrt0,inputs_PROT_IMP(Cell0,wrt0)), (PROT_IMP_Controller3_write3,inputs_PROT_IMP(Controller3,write3)), (PROT_IMP_Cell0_wrt0_R_IO_write3,inputs_R_IO(PROT_IMP_Cell0_wrt0,wrt0,write3)), (PROT_IMP_Controller3_write3_R_IO_wrt0,inputs_R_IO(PROT_IMP_Controller3_write3,write3,wrt0)), (DUAL_PROT_IMP_Cell0_wrt0_R_IO_write3,outputs(PROT_IMP_Cell0_wrt0_R_IO_write3)), (DUAL_PROT_IMP_Controller3_write3_R_IO_wrt0,outputs(PROT_IMP_Controller3_write3_R_IO_wrt0)) > within apply(f, P ) outputs( P ) = let f = < ( Cell0, {| rd0.ack,wrt0.ack |}), ( Controller3, {| output3,write3.1.req,write3.2.req,write3.3.req,read3.1.req,read3.2.req,read3.3.req |}), (PROT_IMP_Cell0_wrt0,outputs_PROT_IMP(Cell0,wrt0)), (PROT_IMP_Controller3_write3,outputs_PROT_IMP(Controller3,write3)), (PROT_IMP_Cell0_wrt0_R_IO_write3,outputs_R_IO(Cell0,wrt0,write3)), (PROT_IMP_Controller3_write3_R_IO_wrt0,outputs_R_IO(Cell0,write3,wrt0)), (DUAL_PROT_IMP_Cell0_wrt0_R_IO_write3,inputs(PROT_IMP_Cell0_wrt0_R_IO_write3)), (DUAL_PROT_IMP_Controller3_write3_R_IO_wrt0,inputs(PROT_IMP_Controller3_write3_R_IO_wrt0)) > within apply(f, P ) PROT_IMP_Cell0_wrt0 = PROT_CELL(wrt0) PROT_IMP_Controller3_write3 = PROT_CTRL(write.1) DUAL_PROT_IMP_Cell0_wrt0 = DUAL_PROT_CELL(wrt0) DUAL_PROT_IMP_Controller3_write3 = DUAL_PROT_CTRL(write.1) PROT_IMP_Cell0_wrt0_R_IO_write3 = PROT_IMP_R(PROT_IMP_Cell0_wrt0,R_IO(Cell0,wrt0,write3)) PROT_IMP_Controller3_write3_R_IO_wrt0 = PROT_IMP_R(PROT_IMP_Controller3_write3,R_IO(Controller3,write3,wrt0)) DUAL_PROT_IMP_Cell0_wrt0_R_IO_write3 = DUAL_PROT_IMP_R(DUAL_PROT_IMP_Cell0_wrt0,R_IO(Cell0,wrt0,write3)) DUAL_PROT_IMP_Controller3_write3_R_IO_wrt0 = DUAL_PROT_IMP_R(DUAL_PROT_IMP_Controller3_write3,R_IO(Controller3,write3,wrt0)) --COMMUNICATION COMPOSITION Cell0_Controller3 = COMM(Cell0, Controller3, wrt0, write3) --D.1 channel1 is in the alphabet of contract assert not Cell0 \ {|wrt0|} [T= Cell0 --D.1 channel1 is in the alphabet of contract assert not Controller3 \ {|write3|} [T= Controller3 --D.4 : I/O confluence for first component --D.4.1 It is divergence-free assert PROT_IMP_Cell0_wrt0 :[divergence free [FD]] --D.4.2 It is refined by the projection on the channel assert PROT_IMP_Cell0_wrt0 [F= PROT_IMP_def(Cell0,wrt0) --D.4.3 It is a refinement of the projection on the channel assert PROT_IMP_def(Cell0,wrt0) [FD= PROT_IMP_Cell0_wrt0 --D.4.4 It is a port-protocol (communication protocol) --D.4.4.1 assert not Test(subseteq(inputs_PROT_IMP(Cell0,wrt0),{|wrt0|})) [T= ERROR --D.4.4.2 assert not Test(subseteq(outputs_PROT_IMP(Cell0,wrt0),{|wrt0|})) [T= ERROR --D.4.5 : The renamed version is I/O Confluent assert InBufferProt(PROT_IMP_Cell0_wrt0_R_IO_write3, wrt0.1) :[deterministic [F]] --D.5 : I/O confluence for second component --D.5.1 assert PROT_IMP_Controller3_write3 :[divergence free [FD]] --D.5.2 assert PROT_IMP_Controller3_write3 [F= PROT_IMP_def(Controller3,write3) --D.5.3 assert PROT_IMP_def(Controller3,write3) [FD= PROT_IMP_Controller3_write3 --D.5.4 --D.5.4.1 assert not Test(subseteq(inputs_PROT_IMP(Controller3,write3),{|write3|})) [T= ERROR --D.5.4.2 assert not Test(subseteq(outputs_PROT_IMP(Controller3,write3),{|write3|})) [T= ERROR --D.5.5 : The renamed version is I/O Confluent assert InBufferProt(PROT_IMP_Controller3_write3_R_IO_wrt0, write3) :[deterministic [F]] ---- D.6: Protocols are Strong Compatible assert PROT_IMP_Cell0_wrt0_R_IO_write3 :[deadlock free [FD]] ---- * D.6.2: Protocols are communication protocols assert not Test(subseteq(inputs(PROT_IMP_Cell0_wrt0_R_IO_write3), {| wrt0|})) [T= ERROR assert not Test(subseteq(outputs(PROT_IMP_Cell0_wrt0_R_IO_write3), {|write3|})) [T= ERROR assert not Test(inputs(PROT_IMP_Cell0_wrt0_R_IO_write3) == outputs(DUAL_PROT_IMP_Cell0_wrt0_R_IO_write3)) [T= ERROR assert not Test(outputs(PROT_IMP_Cell0_wrt0_R_IO_write3) == inputs(DUAL_PROT_IMP_Cell0_wrt0_R_IO_write3)) [T= ERROR assert DUAL_PROT_IMP_Cell0_wrt0_R_IO_write3 [T= PROT_IMP_Cell0_wrt0_R_IO_write3 assert PROT_IMP_Cell0_wrt0_R_IO_write3 [T= DUAL_PROT_IMP_Cell0_wrt0_R_IO_write3 assert DUAL_PROT_IMP_Cell0_wrt0_R_IO_write3 [F= PROT_IMP_Controller3_write3_R_IO_wrt0 assert PROT_IMP_Controller3_write3_R_IO_wrt0 [F= DUAL_PROT_IMP_Cell0_wrt0_R_IO_write3 ---- D.6: Protocols are Strong Compatible assert PROT_IMP_Cell0_wrt0_R_IO_write3 :[deadlock free [FD]] ---- * D.6.2: Protocols are communication protocols assert not Test(subseteq(inputs(PROT_IMP_Cell0_wrt0_R_IO_write3), {| wrt0|})) [T= ERROR assert not Test(subseteq(outputs(PROT_IMP_Cell0_wrt0_R_IO_write3), {|write3|})) [T= ERROR assert not Test(inputs(PROT_IMP_Cell0_wrt0_R_IO_write3) == outputs(DUAL_PROT_IMP_Cell0_wrt0_R_IO_write3)) [T= ERROR assert not Test(outputs(PROT_IMP_Cell0_wrt0_R_IO_write3) == inputs(DUAL_PROT_IMP_Cell0_wrt0_R_IO_write3)) [T= ERROR assert DUAL_PROT_IMP_Cell0_wrt0_R_IO_write3 [T= PROT_IMP_Cell0_wrt0_R_IO_write3 assert PROT_IMP_Cell0_wrt0_R_IO_write3 [T= DUAL_PROT_IMP_Cell0_wrt0_R_IO_write3 assert DUAL_PROT_IMP_Cell0_wrt0_R_IO_write3 [F= PROT_IMP_Controller3_write3_R_IO_wrt0 assert PROT_IMP_Controller3_write3_R_IO_wrt0 [F= DUAL_PROT_IMP_Cell0_wrt0_R_IO_write3 assert PROT_IMP_Controller3_write3_R_IO_wrt0 :[deadlock free [FD]] assert not Test(subseteq(inputs(PROT_IMP_Controller3_write3_R_IO_wrt0), {| write3|})) [T= ERROR assert not Test(subseteq(outputs(PROT_IMP_Controller3_write3_R_IO_wrt0), {| wrt0|})) [T= ERROR assert not Test(inputs(PROT_IMP_Controller3_write3_R_IO_wrt0) == outputs(DUAL_PROT_IMP_Controller3_write3_R_IO_wrt0)) [T= ERROR assert not Test(outputs(PROT_IMP_Controller3_write3_R_IO_wrt0) == inputs(DUAL_PROT_IMP_Controller3_write3_R_IO_wrt0)) [T= ERROR assert DUAL_PROT_IMP_Controller3_write3_R_IO_wrt0 [T= PROT_IMP_Controller3_write3_R_IO_wrt0 assert PROT_IMP_Controller3_write3_R_IO_wrt0 [T= DUAL_PROT_IMP_Controller3_write3_R_IO_wrt0 assert DUAL_PROT_IMP_Controller3_write3_R_IO_wrt0 [F= PROT_IMP_Cell0_wrt0_R_IO_write3 assert PROT_IMP_Cell0_wrt0_R_IO_write3 [F= DUAL_PROT_IMP_Controller3_write3_R_IO_wrt0 --D.7: Protocols have Finite Output Property --D.7.1 assert PROT_IMP_Cell0_wrt0_R_IO_write3 \ outputs(PROT_IMP_Cell0_wrt0_R_IO_write3):[divergence free [FD]] assert PROT_IMP_Controller3_write3_R_IO_wrt0 \ outputs(PROT_IMP_Controller3_write3_R_IO_wrt0):[divergence free [FD]]