const Max = 3
range Int = 0..Max
SEMAPHORE(N=0) = SEMA[N],
SEMA[v:Int] = (up -> SEMA[v + 1] | when (v > 0) down -> SEMA[v - 1]),
SEMA[Max + 1] = ERROR.

LOOP   = (mutex.down -> pega -> devolve -> mutex.up -> LOOP).
||DEMO = (p[1..3]:LOOP || {p[1..3]}::mutex:SEMAPHORE(1)).

property  MUTEX  = (p[i:1..3].pega -> p[i].devolve -> MUTEX).
||TESTE = (DEMO || MUTEX).