Madiel de Souza Conserva Filho / bts

476d7d0f0b795c0eb84d2199d510d59b0c81d401.svn-base 1.14 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

BUF = write.req?x -> read.req.x -> write.ack!x -> read.ack.x -> BUF
channel write0 : Direction.Value
channel read0 : Direction.Value
channel write1 : Direction.Value
channel read1 : Direction.Value

Rename1(i) = BUF [[write <- write0,read <- read0]] 


Rename2(i) = BUF [[write <- write1,read <- read1]] 
Inst_BUF0 = <(write,write0),(read,read0)> 
BUF0 = rename(BUF, Inst_BUF0) 

Inst_BUF1 = <(write,write1),(read,read1)> 
BUF1 = rename(BUF, Inst_BUF1) 


GET_CHANNELS(P) =
 	 let f =
 	 < 
	(BUF0, { write0,read0 }),

	(BUF1, { write1,read1 })

 	 > 

 	 within apply(f,P )

inputs( P ) = 
 	 let f = 
	<
 	 ( BUF0, {| write0.req,read0.req |}),
 	 ( BUF1, {| write1.req,read1.req |})
 	 > 

 	 within apply(f, P )
 outputs( P ) = 
 	 let f =
	  < 
	 ( BUF0, {| write0.ack,read0.ack |}),
	 ( BUF1, {| write1.ack,read1.ack |})
 	 >
 	 within apply(f, P )

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