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

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 input0 : Value
channel output0 : Value
channel write0 : CellId.Direction.Value
channel read0 : CellId.Direction.Value


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_Controller0 = <(input,input0),(output,output0),(write,write0),(read,read0)> 
Controller0 = rename(Controller, Inst_Controller0) 


GET_CHANNELS(P) =
 	 let f =
 	 < 
	(Controller0, { input0,output0,write0,read0 }),

	(PROT_IMP_Controller0_write0,{write0}),

	(PROT_IMP_Controller0_read0,{read0}) 	 > 

 	 within apply(f,P )

inputs( P ) = 
 	 let f = 
	<
 	 ( Controller0, {| input0,write0.1.ack,write0.2.ack,write0.3.ack,read0.1.ack,read0.2.ack,read0.3.ack |}),
	(PROT_IMP_Controller0_write0,inputs_PROT_IMP(Controller0,write0)),

	(PROT_IMP_Controller0_read0,inputs_PROT_IMP(Controller0,read0)),

	(PROT_IMP_Controller0_write0_R_IO_read0,inputs_R_IO(PROT_IMP_Controller0_write0,write0,read0)),

	(PROT_IMP_Controller0_read0_R_IO_write0,inputs_R_IO(PROT_IMP_Controller0_read0,read0,write0)),

	(DUAL_PROT_IMP_Controller0_write0_R_IO_read0,outputs(PROT_IMP_Controller0_write0_R_IO_read0)),

	(DUAL_PROT_IMP_Controller0_read0_R_IO_write0,outputs(PROT_IMP_Controller0_read0_R_IO_write0))
 	 > 

 	 within apply(f, P )


 outputs( P ) = 
 	 let f =
	  < 
	 ( Controller0, {| output0,write0.1.req,write0.2.req,write0.3.req,read0.1.req,read0.2.req,read0.3.req |}),
	(PROT_IMP_Controller0_write0,outputs_PROT_IMP(Controller0,write0)),

	(PROT_IMP_Controller0_read0,outputs_PROT_IMP(Controller0,read0)),

	(PROT_IMP_Controller0_write0_R_IO_read0,outputs_R_IO(Controller0,write0,read0)),

	(PROT_IMP_Controller0_read0_R_IO_write0,outputs_R_IO(Controller0,read0,write0)),

	(DUAL_PROT_IMP_Controller0_write0_R_IO_read0,inputs(PROT_IMP_Controller0_write0_R_IO_read0)),

	(DUAL_PROT_IMP_Controller0_read0_R_IO_write0,inputs(PROT_IMP_Controller0_read0_R_IO_write0))
 	 > 

 	 within apply(f, P )

PROT_IMP_Controller0_write0 = PROT_CTRL(write.1)

PROT_IMP_Controller0_read0 = PROT_CTRL(read.1)

DUAL_PROT_IMP_Controller0_write0 = DUAL_PROT_CTRL(write.1)

DUAL_PROT_IMP_Controller0_read0 = DUAL_PROT_CTRL(read.1)

PROT_IMP_Controller0_write0_R_IO_read0 = PROT_IMP_R(PROT_IMP_Controller0_write0,R_IO(Controller0,write0,read0))
PROT_IMP_Controller0_read0_R_IO_write0 = PROT_IMP_R(PROT_IMP_Controller0_read0,R_IO(Controller0,read0,write0))

DUAL_PROT_IMP_Controller0_write0_R_IO_read0 = DUAL_PROT_IMP_R(DUAL_PROT_IMP_Controller0_write0,R_IO(Controller0,write0,read0))
DUAL_PROT_IMP_Controller0_read0_R_IO_write0 = DUAL_PROT_IMP_R(DUAL_PROT_IMP_Controller0_read0,R_IO(Controller0,read0,write0))

--REFLEXIVE COMPOSITION

Controller0_Controller0 = REF(Controller0, write0, read0)


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

assert not Controller0 \ {|write0|} [T= Controller0



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

assert not Controller0 \ {|read0|} [T= Controller0

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


assert PROT_IMP_Controller0_write0 :[divergence free [FD]]

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

assert PROT_IMP_Controller0_write0 [F= PROT_IMP_def(Controller0,write0)

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

assert PROT_IMP_def(Controller0,write0) [FD= PROT_IMP_Controller0_write0

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


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

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

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

assert InBufferProt(PROT_IMP_Controller0_write0_R_IO_read0, write0) :[deterministic [F]]

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


assert PROT_IMP_Controller0_read0 :[divergence free [FD]]

--D.5.2 

assert PROT_IMP_Controller0_read0 [F= PROT_IMP_def(Controller0,read0)

--D.5.3 

assert PROT_IMP_def(Controller0,read0) [FD= PROT_IMP_Controller0_read0

--D.5.4 


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

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

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

assert InBufferProt(PROT_IMP_Controller0_read0_R_IO_write0, read0) :[deterministic [F]]

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

----	 * D.6.2: Protocols are communication protocols
assert not Test(subseteq(inputs(PROT_IMP_Controller0_write0_R_IO_read0), {| write0|})) [T= ERROR
assert not Test(subseteq(outputs(PROT_IMP_Controller0_write0_R_IO_read0), {|read0|})) [T= ERROR
assert not Test(inputs(PROT_IMP_Controller0_write0_R_IO_read0) == outputs(DUAL_PROT_IMP_Controller0_write0_R_IO_read0)) [T= ERROR

assert not Test(outputs(PROT_IMP_Controller0_write0_R_IO_read0) == inputs(DUAL_PROT_IMP_Controller0_write0_R_IO_read0)) [T= ERROR

assert DUAL_PROT_IMP_Controller0_write0_R_IO_read0 [T= PROT_IMP_Controller0_write0_R_IO_read0

assert PROT_IMP_Controller0_write0_R_IO_read0 [T= DUAL_PROT_IMP_Controller0_write0_R_IO_read0



assert DUAL_PROT_IMP_Controller0_write0_R_IO_read0 [F= PROT_IMP_Controller0_read0_R_IO_write0



assert PROT_IMP_Controller0_read0_R_IO_write0 [F= DUAL_PROT_IMP_Controller0_write0_R_IO_read0

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

----	 * D.6.2: Protocols are communication protocols
assert not Test(subseteq(inputs(PROT_IMP_Controller0_write0_R_IO_read0), {| write0|})) [T= ERROR
assert not Test(subseteq(outputs(PROT_IMP_Controller0_write0_R_IO_read0), {|read0|})) [T= ERROR
assert not Test(inputs(PROT_IMP_Controller0_write0_R_IO_read0) == outputs(DUAL_PROT_IMP_Controller0_write0_R_IO_read0)) [T= ERROR

assert not Test(outputs(PROT_IMP_Controller0_write0_R_IO_read0) == inputs(DUAL_PROT_IMP_Controller0_write0_R_IO_read0)) [T= ERROR

assert DUAL_PROT_IMP_Controller0_write0_R_IO_read0 [T= PROT_IMP_Controller0_write0_R_IO_read0

assert PROT_IMP_Controller0_write0_R_IO_read0 [T= DUAL_PROT_IMP_Controller0_write0_R_IO_read0



assert DUAL_PROT_IMP_Controller0_write0_R_IO_read0 [F= PROT_IMP_Controller0_read0_R_IO_write0



assert PROT_IMP_Controller0_read0_R_IO_write0 [F= DUAL_PROT_IMP_Controller0_write0_R_IO_read0

assert PROT_IMP_Controller0_read0_R_IO_write0 :[deadlock free [FD]]

assert not Test(subseteq(inputs(PROT_IMP_Controller0_read0_R_IO_write0), {| read0|})) [T= ERROR
assert not Test(subseteq(outputs(PROT_IMP_Controller0_read0_R_IO_write0), {| write0|})) [T= ERROR
assert not Test(inputs(PROT_IMP_Controller0_read0_R_IO_write0) == outputs(DUAL_PROT_IMP_Controller0_read0_R_IO_write0)) [T= ERROR
assert not Test(outputs(PROT_IMP_Controller0_read0_R_IO_write0) == inputs(DUAL_PROT_IMP_Controller0_read0_R_IO_write0)) [T= ERROR
assert DUAL_PROT_IMP_Controller0_read0_R_IO_write0 [T= PROT_IMP_Controller0_read0_R_IO_write0

assert PROT_IMP_Controller0_read0_R_IO_write0 [T= DUAL_PROT_IMP_Controller0_read0_R_IO_write0



assert DUAL_PROT_IMP_Controller0_read0_R_IO_write0 [F= PROT_IMP_Controller0_write0_R_IO_read0



assert PROT_IMP_Controller0_write0_R_IO_read0 [F= DUAL_PROT_IMP_Controller0_read0_R_IO_write0

--D.7: Protocols have Finite Output Property 

--D.7.1

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

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

Controller0_LR1 = <(write0.1.req.v) | v <- seq(Value)> 
Controller0_LR2 = <(read0.1.ack.v) | v <- seq(Value)> 


assert PROJECTION(Controller0, {write0, read0}) [| {| write0, read0 |} |] BUFF_IO_1(Controller0_LR1, Controller0_LR2):[deadlock free [F]]