Translator from LTS to state machine.

//Semaphore Specification
SEMAPHORE(N=4) = SEMA[0],
SEMA[0]        = (up -> SEMA[1]),
SEMA[i:1..N-1] = (up -> SEMA[i+1] | down -> SEMA[i-1]),
SEMA[N]        = (down -> SEMA[N-1]).

// Producer Specification
PROD = (produce -> up -> PROD).

//Consumer Specification
CONS = (down ->consume -> CONS).


// Golfball Allocator Specification
(N=8)
GOLFBALL(N=8)= BALL[N],
BALL[b:0..N] = (get[i:1..b]   -> BALL[b-i]
               |put[j:1..N-b] -> BALL[b+j]
               ).