Madiel de Souza Conserva Filho / bts

c5cc3535e1b88b529686c92f04acbe3d0e33427e.svn-base 1.21 KB
edit raw blame history 
  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
include "auxiliar.csp" 
include "rules.csp"

datatype Direction = req | ack
Value = {1..3}
channel write : Direction.Value
channel read : Direction.Value

BricRingCell = write.req?x -> write.ack.x -> read.req?dumb -> read.ack!x -> BricRingCell
channel write2 : Direction.Value
channel read2 : Direction.Value
channel write3 : Direction.Value
channel read3 : Direction.Value

Rename1(i) = BricRingCell [[write <- write2,read <- read2]] 


Rename2(i) = BricRingCell [[write <- write3,read <- read3]] 
Inst_Cell2 = <(write,write2),(read,read2)> 
Cell2 = rename(BricRingCell, Inst_Cell2) 

Inst_Cell3 = <(write,write3),(read,read3)> 
Cell3 = rename(BricRingCell, Inst_Cell3) 


GET_CHANNELS(P) =
 	 let f =
 	 < 
	(Cell2, { write2,read2 }),

	(Cell3, { write3,read3 })

 	 > 

 	 within apply(f,P )

inputs( P ) = 
 	 let f = 
	<
 	 ( Cell2, {| write2.req,read2.req |}),
 	 ( Cell3, {| write3.req,read3.req |})
 	 > 

 	 within apply(f, P )
 outputs( P ) = 
 	 let f =
	  < 
	 ( Cell2, {| write2.ack,read2.ack |}),
	 ( Cell3, {| write3.ack,read3.ack |})
 	 >
 	 within apply(f, P )

--INTERLEAVING COMPOSITION 
newComponent = INTER(Cell2,Cell3) 
assert STOP [T= RUN(inter(events(Cell2),events(Cell3)))
assert newComponent:[deadlock free[FD]]