const A = 2
const E = 2
ARQ = (salva -> escreve -> ARQ1),
ARQ1 = (salva -> escreve -> ARQ1 | existe -> ARQ1).

EDITOR = (cria -> edita -> TESTA |
          arq[i:1..A].carrega -> edita -> arq[i].mutex.down -> arq[i].salva -> arq[i].mutex.up -> EDITOR),

TESTA = (arq[i:1..A].existe -> PERG[i] | arq[i:1..A].mutex.down -> arq[i].salva -> arq[i].mutex.up -> EDITOR),
PERG[i:1..A] = (grava -> arq[i].mutex.down -> arq[i].salva -> arq[i].mutex.up -> EDITOR | descarta -> EDITOR).

SEMAPHORE(N=0) = SEMA[N],
SEMA[v:0..A] = (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].existe/arq[j].existe,
		      editor[1..E].arq[j:1..A].escreve/arq[j].escreve,
		      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}.