RELOGIO = (tick -> RELOGIO).

SINALEIRA(A=10,B=20,C=10,D=20) = AMARELO1[1],
AMARELO1[i:1..A] = (when (i < A) tick -> amarelo -> AMARELO1[i+1] | when (i == A) tick -> amarelo -> VERMELHO[1]),
VERMELHO[i:1..B] = (when (i < B) tick -> vermelho -> VERMELHO[i+1] | when (i == B) tick -> vermelho -> AMARELO2[1]),
AMARELO2[i:1..C] = (when (i < C) tick -> amarelo -> AMARELO2[i+1] | when (i == C) tick -> amarelo -> VERDE[1]),
VERDE[i:1..D]    = (when (i == 1) tick -> mutex.down -> verde -> VERDE[i+1] |  when (i> 1 && i < D) tick -> verde -> VERDE[i+1] |
                    when (i == D) tick -> verde -> mutex.up -> AMARELO1[1]).

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

||SIST = (RELOGIO || s[1]:SINALEIRA(2,4,2,4) || s[2]:SINALEIRA(1,3,1,6) || mutex:SEMAPHORE(1))
          /{s[1..2].tick/tick, s[1..2].mutex.down/mutex.down, s[1..2].mutex.up/mutex.up}.