RuleCommunicationOfCell0_Controller3.csp~ 8.88 KB
edit raw blame history

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]]