const A = 5
const E = 2
ARQ = (salva -> escreve -> ARQ).
EDITOR = (cria -> edita -> arq[i:1..A].mutex.down -> arq[i].salva -> arq[i].mutex.up -> EDITOR |
          arq[i:1..A].carrega -> edita -> arq[i].mutex.down -> arq[i].salva -> arq[i].mutex.up -> EDITOR).

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

||SIST = (arq[1..A]:ARQ || editor[i:1..E]:EDITOR || arq[1..A].mutex:SEMAPHORE(1)) 
			/{editor[1..E].arq[j:1..A].salva/arq[j].salva, 
			  editor[1..E].arq[j:1..A].mutex.down/arq[j].mutex.down,
			  editor[1..E].arq[j:1..A].mutex.up/arq[j].mutex.up}.