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 channel rd_i : CellId.Direction.Value channel wrt_i : CellId.Direction.Value Cell = wrt.req?x -> wrt.ack.x -> rd.req?dumb -> rd.ack!x -> Cell Cell1_Cell2 = INTER(Cell1, Cell2) Inst_Cell1 = <(rd,rd_i.1),(wrt,wrt_i.1)> Cell1 = rename(Cell, Inst_Cell1) Inst_Cell2 = <(rd,rd_i.2),(wrt,wrt_i.2)> Cell2 = rename(Cell, Inst_Cell2) Cell1_Cell2_INTER_Cell3 = INTER(Cell1_Cell2_INTER, Cell3) Inst_Cell1_Cell2_INTER = <(rd,rd_i.1),(wrt,wrt_i.1),(rd,rd_i.2),(wrt,wrt_i.2)> Cell1_Cell2_INTER = rename(Cell1_Cell2, Inst_Cell1_Cell2_INTER) Inst_Cell3 = <(rd,rd_i.3),(wrt,wrt_i.3)> Cell3 = rename(Cell, Inst_Cell3) 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) 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_Cell1_Cell2_INTER_Cell3_INTER = <(rd,rd_i.1),(wrt,wrt_i.1),(rd,rd_i.2),(wrt,wrt_i.2),(rd,rd_i.3),(wrt,wrt_i.3)> Cell1_Cell2_INTER_Cell3_INTER = rename(Cell1_Cell2_INTER_Cell3, Inst_Cell1_Cell2_INTER_Cell3_INTER) Inst_Controller3 = <(input,input),(output,output),(write,write),(read,read)> Controller3 = rename(Controller, Inst_Controller3) GET_CHANNELS(P) = let f = < (Cell1_Cell2_INTER_Cell3_INTER, { rd_i.1,wrt_i.1,rd_i.2,wrt_i.2,rd_i.3,wrt_i.3 }), (Controller3, { input,output,write,read }), (PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1,{wrt_i.1}), (PROT_IMP_Controller3_write,{write.1}) > within apply(f,P ) inputs( P ) = let f = < ( Cell1_Cell2_INTER_Cell3_INTER, {| rd_i.1.req,wrt_i.1.req,rd_i.2.req,wrt_i.2.req,rd_i.3.req,wrt_i.3.req |}), ( Controller3, {| input,write.1.ack,write.2.ack,write.3.ack,read.1.ack,read.2.ack,read.3.ack |}), (PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1,inputs_PROT_IMP(Cell1_Cell2_INTER_Cell3_INTER,wrt_i.1)), (PROT_IMP_Controller3_write,inputs_PROT_IMP(Controller3,write.1)), (PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write,inputs_R_IO(PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1,wrt_i.1,write.1)), (PROT_IMP_Controller3_write_R_IO_wrt_i_1,inputs_R_IO(PROT_IMP_Controller3_write,write.1,wrt_i.1)), (DUAL_PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write,outputs(PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write)), (DUAL_PROT_IMP_Controller3_write_R_IO_wrt_i_1,outputs(PROT_IMP_Controller3_write_R_IO_wrt_i_1)) > within apply(f, P ) outputs( P ) = let f = < ( Cell1_Cell2_INTER_Cell3_INTER, {| rd_i.1.ack,wrt_i.1.ack,rd_i.2.ack,wrt_i.2.ack,rd_i.3.ack,wrt_i.3.ack |}), ( Controller3, {| output,write.1.req,write.2.req,write.3.req,read.1.req,read.2.req,read.3.req |}), (PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1,outputs_PROT_IMP(Cell1_Cell2_INTER_Cell3_INTER,wrt_i.1)), (PROT_IMP_Controller3_write,outputs_PROT_IMP(Controller3,write.1)), (PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write,outputs_R_IO(Cell1_Cell2_INTER_Cell3_INTER,wrt_i.1,write.1)), (PROT_IMP_Controller3_write_R_IO_wrt_i_1,outputs_R_IO(Cell1_Cell2_INTER_Cell3_INTER,write.1,wrt_i.1)), (DUAL_PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write,inputs(PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write)), (DUAL_PROT_IMP_Controller3_write_R_IO_wrt_i_1,inputs(PROT_IMP_Controller3_write_R_IO_wrt_i_1)) > within apply(f, P ) PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1 = PROT_CELL(wrt_i.1) PROT_IMP_Controller3_write = PROT_CTRL(write.1) DUAL_PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1 = DUAL_PROT_CELL(wrt_i.1) DUAL_PROT_IMP_Controller3_write = DUAL_PROT_CTRL(write.1) PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write = PROT_IMP_R(PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1,R_IO(Cell1_Cell2_INTER_Cell3_INTER,wrt_i.1,write.1)) PROT_IMP_Controller3_write_R_IO_wrt_i_1 = PROT_IMP_R(PROT_IMP_Controller3_write,R_IO(Controller3,write.1,wrt_i.1)) DUAL_PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write = DUAL_PROT_IMP_R(DUAL_PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1,R_IO(Cell1_Cell2_INTER_Cell3_INTER,wrt_i.1,write.1)) DUAL_PROT_IMP_Controller3_write_R_IO_wrt_i_1 = DUAL_PROT_IMP_R(DUAL_PROT_IMP_Controller3_write,R_IO(Controller3,write.1,wrt_i.1)) --COMMUNICATION COMPOSITION Cell1_Cell2_INTER_Cell3_INTER_Controller3 = COMM(Cell1_Cell2_INTER_Cell3_INTER, Controller3, wrt_i.1, write.1) --D.1 channel1 is in the alphabet of contract assert not Cell1_Cell2_INTER_Cell3_INTER \ {|wrt_i.1|} [T= Cell1_Cell2_INTER_Cell3_INTER --D.1 channel1 is in the alphabet of contract assert not Controller3 \ {|write.1|} [T= Controller3 --D.4 : I/O confluence for first component --D.4.1 It is divergence-free assert PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1 :[divergence free [FD]] --D.4.2 It is refined by the projection on the channel assert PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1 [F= PROT_IMP_def(Cell1_Cell2_INTER_Cell3_INTER,wrt_i.1) --D.4.3 It is a refinement of the projection on the channel assert PROT_IMP_def(Cell1_Cell2_INTER_Cell3_INTER,wrt_i.1) [FD= PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1 --D.4.4 It is a port-protocol (communication protocol) --D.4.4.1 assert not Test(subseteq(inputs_PROT_IMP(Cell1_Cell2_INTER_Cell3_INTER,wrt_i.1),{|wrt_i.1|})) [T= ERROR --D.4.4.2 assert not Test(subseteq(outputs_PROT_IMP(Cell1_Cell2_INTER_Cell3_INTER,wrt_i.1),{|wrt_i.1|})) [T= ERROR --D.4.5 : The renamed version is I/O Confluent assert InBufferProt(PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write, wrt_i.1) :[deterministic [F]] --D.5 : I/O confluence for second component --D.5.1 assert PROT_IMP_Controller3_write :[divergence free [FD]] --D.5.2 assert PROT_IMP_Controller3_write [F= PROT_IMP_def(Controller3,write.1) --D.5.3 assert PROT_IMP_def(Controller3,write.1) [FD= PROT_IMP_Controller3_write --D.5.4 --D.5.4.1 assert not Test(subseteq(inputs_PROT_IMP(Controller3,write.1),{|write|})) [T= ERROR --D.5.4.2 assert not Test(subseteq(outputs_PROT_IMP(Controller3,write.1),{|write|})) [T= ERROR --D.5.5 : The renamed version is I/O Confluent assert InBufferProt(PROT_IMP_Controller3_write_R_IO_wrt_i_1, write.1) :[deterministic [F]] ---- D.6: Protocols are Strong Compatible assert PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write :[deadlock free [FD]] ---- * D.6.2: Protocols are communication protocols assert not Test(subseteq(inputs(PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write), {| wrt_i.1|})) [T= ERROR assert not Test(subseteq(outputs(PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write), {|write|})) [T= ERROR assert not Test(inputs(PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write) == outputs(DUAL_PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write)) [T= ERROR assert not Test(outputs(PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write) == inputs(DUAL_PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write)) [T= ERROR assert DUAL_PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write [T= PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write assert PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write [T= DUAL_PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write assert DUAL_PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write [F= PROT_IMP_Controller3_write_R_IO_wrt_i_1 assert PROT_IMP_Controller3_write_R_IO_wrt_i_1 [F= DUAL_PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write ---- D.6: Protocols are Strong Compatible assert PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write :[deadlock free [FD]] ---- * D.6.2: Protocols are communication protocols assert not Test(subseteq(inputs(PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write), {| wrt_i.1|})) [T= ERROR assert not Test(subseteq(outputs(PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write), {|write|})) [T= ERROR assert not Test(inputs(PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write) == outputs(DUAL_PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write)) [T= ERROR assert not Test(outputs(PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write) == inputs(DUAL_PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write)) [T= ERROR assert DUAL_PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write [T= PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write assert PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write [T= DUAL_PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write assert DUAL_PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write [F= PROT_IMP_Controller3_write_R_IO_wrt_i_1 assert PROT_IMP_Controller3_write_R_IO_wrt_i_1 [F= DUAL_PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write assert PROT_IMP_Controller3_write_R_IO_wrt_i_1 :[deadlock free [FD]] assert not Test(subseteq(inputs(PROT_IMP_Controller3_write_R_IO_wrt_i_1), {| write|})) [T= ERROR assert not Test(subseteq(outputs(PROT_IMP_Controller3_write_R_IO_wrt_i_1), {| wrt_i.1|})) [T= ERROR assert not Test(inputs(PROT_IMP_Controller3_write_R_IO_wrt_i_1) == outputs(DUAL_PROT_IMP_Controller3_write_R_IO_wrt_i_1)) [T= ERROR assert not Test(outputs(PROT_IMP_Controller3_write_R_IO_wrt_i_1) == inputs(DUAL_PROT_IMP_Controller3_write_R_IO_wrt_i_1)) [T= ERROR assert DUAL_PROT_IMP_Controller3_write_R_IO_wrt_i_1 [T= PROT_IMP_Controller3_write_R_IO_wrt_i_1 assert PROT_IMP_Controller3_write_R_IO_wrt_i_1 [T= DUAL_PROT_IMP_Controller3_write_R_IO_wrt_i_1 assert DUAL_PROT_IMP_Controller3_write_R_IO_wrt_i_1 [F= PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write assert PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write [F= DUAL_PROT_IMP_Controller3_write_R_IO_wrt_i_1 --D.7: Protocols have Finite Output Property --D.7.1 assert PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write \ outputs(PROT_IMP_Cell1_Cell2_INTER_Cell3_INTER_wrt_i_1_R_IO_write):[divergence free [FD]] assert PROT_IMP_Controller3_write_R_IO_wrt_i_1 \ outputs(PROT_IMP_Controller3_write_R_IO_wrt_i_1):[divergence free [FD]]