/* Una palestra ha un’utenza composta da N uomini e N donne. 
Poiché dispone di un solo spogliatoio deve organizzare turni 
per evitare che persone di sesso diverso si trovino contemporaneamente 
nello spogliatoio. Un Inserviente è quindi incaricato di ottimizzare 
l’accesso allo spogliatoio consentendo a una donna (un uomo) di cambiarsi 
solo se lo spogliatoio è libero o se è già occupato da un’altra donna (un altro uomo).
La palestra ha inoltre una categoria vip, con NV membri, che consente a chi vi 
appartiene (uomo o donna) di avere la precedenza e di cambiarsi da solo.
Modellare il sistema supponendo che gli utenti possono arrivare in ordine 
qualsiasi ed abbiano un comportamento ciclico. Assumere N=3 e NV=1. 
Realizzare il sistema in Java con N e NV parametri del main. */


const N=3
const NV=1

range NRange=0..N
range PersoneRange=0..N+N+NV
range VipRange=0..NV
range SexRange=0..2 //0=donne,1=uomini, 2=vip

// N+N+NV persone

Donna = (entraDonna -> spogliaDonna -> esciDonna -> Donna).
Uomo = (entraUomo -> spogliaUomo -> esciUomo -> Uomo).
Vip = (richiediIngressoVip -> entraVip -> spogliaVip -> esciVip -> Vip).

Inserviente = Inserviente[0][0][0],
Inserviente[npersone:PersoneRange][sesso:SexRange][nvip:VipRange] = (
	//Donne
	when (nvip==0 & ((sesso==0 & npersone<(N+N+NV)) | (npersone==0))) d[NRange].entraDonna -> Inserviente[npersone+1][0][nvip] |
	when (sesso==0 & npersone>0) d[NRange].esciDonna -> Inserviente[npersone-1][0][nvip] |
	//Uomini
	when (nvip==0 & ((sesso==1 & npersone<(N+N+NV)) | (npersone==0))) u[NRange].entraUomo -> Inserviente[npersone+1][1][nvip] |
	when (sesso==1 & npersone>0) u[NRange].esciUomo -> Inserviente[npersone-1][1][nvip] |
	//Vip
	//Se c'è un vip in attesa...
	when (nvip<NV) v[VipRange].richiediIngressoVip -> Inserviente[npersone][sesso][nvip+1] |  
	//Se non ci sono persone posso far entrare un VIP
	when (npersone==0 & nvip>0) v[VipRange].entraVip -> Inserviente[npersone+1][2][nvip-1] |
	when (npersone>0) v[VipRange].esciVip -> Inserviente[npersone-1][0][nvip] 
).

||Donne = (d[NRange]:Donna).
||Uomini = (u[NRange]:Uomo).
||Vips = (v[VipRange]:Vip).

||SYS = (Donne || Uomini || Inserviente || Vips).