OUT = {10,20,50}

channel in
channel out : OUT

CHANGE1 = in -> out.50 -> out.50 -> CHANGE1  

CHANGE2 = in -> out.50 -> out.20 -> out.20 -> out.10 -> CHANGE2 

  
CHANGE3 = in -> out.50 -> out.20 -> out.10 -> out.10 -> out.10 -> CHANGE3 

CHANGE = in -> CH_OUT(100)  
  
CH_OUT(x) = if (x==0) then CHANGE 
	    else ((x >= 50) &  CH_OUT1(x)
	          [] 
	  	  (x<50 and 20<=x) & CH_OUT2(x)
	          []
	          (x<20) & out.10 -> CH_OUT(x-10))

CH_OUT1(x) =  out.10 -> CH_OUT(x-10)
  	  |~| out.20 -> CH_OUT(x-20)
  	  |~| out.50 -> CH_OUT(x-50)

CH_OUT2(x) =  out.10 -> CH_OUT(x-10)
  	  |~| out.20 -> CH_OUT(x-20)

assert CHANGE [T= CHANGE1
assert CHANGE [T= CHANGE2
assert CHANGE [T= CHANGE3