DATA = {0,1}
N = 2

channel left, right : DATA

BUFF(s) = (#s==0) & (left?x -> BUFF(<x>))
	  []
	  (#s>0) & ((left?x -> BUFF(s^<x>) |~| STOP)
		    []
		    right.head(s) -> BUFF(tail(s)))

BUFF_2(s) = (#s==0) & (left?x -> BUFF_2(<x>))
	    []
	    (#s==2) & (right.head(s) -> BUFF_2(tail(s)))
	    []
	    (#s<2 and #s>0) & 
		((left?x -> BUFF_2(s^<x>) |~| STOP)
		 []
		 right.head(s) -> BUFF_2(tail(s)))

BUFF_4(s) = (#s==0) & (left?x -> BUFF_4(<x>))
	    []
	    (#s==4) & (right.head(s) -> BUFF_4(tail(s)))
	    []
	    (#s<4 and #s>0) & 
		((left?x -> BUFF_4(s^<x>) |~| STOP)
		 []
		 right.head(s) -> BUFF_4(tail(s)))

assert BUFF_4(<>) [T= BUFF_2(<>)
assert BUFF_4(<>) [F= BUFF_2(<>)
assert BUFF_4(<>) [FD= BUFF_2(<>)

assert BUFF_2(<>) :[deadlock free]
assert BUFF_4(<>) :[deadlock free]
assert BUFF(<>) :[deadlock free]