No entiendo la especificación para hacer un programa

[kikue]

Hola , tengo un problema , tengo que hacer un programa , para hacerlo me han dado la especificación pero no la entiendo,le agradecería a cualquiera que me ayudase aunque sea un poco.
la especificación es la siguiente:

C-TAD Gestor De Eventos

OPERACIONES

ACCIÓN Emitir: EID[e]
ACCIÓN Subscribir: PID[e] × EID[e]
ACCIÓN Desubscribir: PID[e] × EID[e]
ACCIÓN Escuchar: PID[e] × EID[s]
SEMÁNTICA

DOMINIO:
TIPO: Gestor De Eventos= (subscritos : EID → Conjunto(PID) ×
porescuchar : EID → Conjunto(PID))

EID= 0 .. N EVENTOS
PID= 0 .. N OBSERVADORES

INICIAL: ? eid ? EID • self.subscritos(eid) =0
? self.porescuchar(eid) =0

CPRE: Cierto
Emitir(eid)
POST: self.porescuchar(eid) = selfpr e .subscritos(eid) ?
? e ? EID • (self.subscritos(e) = selfpr e .subscritos(e) ?
(e eid => self.porescuchar(e) = selfpr e .porescuchar(e)))

CPRE: Cierto
Subscribir(pid,eid)
POST: self.subscritos(eid) = selfpr e .subscritos(eid) ? {pid} ?
? e ? EID • (self.porescuchar(e) = selfpr e .porescuchar(e) ?
(e eid => self.subscritos(e) = selfpr e .subscritos(e)))

PRE: pid ? self.subcritos(eid)
CPRE: Cierto
Desubscribir(pid,eid)
POST: self.subscritos(eid) = selfpr e .subscritos(eid) \ {pid} ?
self.porescuchar(eid) = selfpr e .porescuchar(eid) \ {pid} ?
? e ? EID • e eid => (self.porescuchar(e) = selfpr e .porescuchar(e) ?
self.subscritos(e) = selfpr e .subscritos(e))

CPRE: ? e ? EID • pid ? self.porescuchar(e)
Escuchar(pid,eid)
POST: pid ? selfpr e .porescuchar(eid) ?
self.porescuchar(eid) = selfpr e .porescuchar(eid) \ {pid} ?
? e ? EID • (self.subscritos(e) = selfpr e .subscritos(e) ?
(e eid => self.porescuchar(e) = selfpr e .porescuchar(e)))

/////////////////////////////////////////////////////////////////////////////////////////
el código que llevo realizado es el siguiente(falta casi todo lo se pero una vez que mas o menos tenga la ida de como va sabría acabarlo):

import es.upm.babel.cclib.Monitor;
import es.upm.babel.cclib.Monitor.*;
import org.jcsp.lang.*;

public class GestorDeEventosMonitor implements GestorDeEventos {
//Declaracion de los Locks & Conditions

Monitor mutex;
Cond cEmitir,cSubscribir,cDesubscribir,cEscuchar;
int porescuchar,subscritos;

public GestorDeEventosMonitor() {
mutex = new Monitor();
cEmitir= mutex.newCond();
cSubscribir= mutex.newCond();
cDesubscribir= mutex.newCond();
cEscuchar = mutex.newCond();
}

@Override
public void emitir(int eid) {
// TODO Auto-generated method stub
mutex.enter();
porescuchar = eid;



//Protocolo de salida de la seccion critica y codigo de sincronizacion
// para poder emitir
cEmitir.signal();
mutex.leave();

}

@Override
public void subscribir(int pid, int eid) {
// TODO Auto-generated method stub
mutex.enter();
//codigo de sincronizacion para poder subscribirse
if(porescuchar==0){
cSubscribir.await();
}

//Protocolo de salida de la seccion critica y codigo de sincronizacion
// para poder subscribirse
cSubscribir.signal();
mutex.leave();
}

@Override
public void desubscribir(int pid, int eid) {
// TODO Auto-generated method stub
mutex.enter();


//Protocolo de salida de la seccion critica y codigo de sincronizacion
// para poder desubscribirse
cDesubscribir.signal();
mutex.leave();
}

@Override
public int escuchar(int pid) {
// TODO Auto-generated method stub
mutex.enter();



//Protocolo de salida de la seccion critica y codigo de sincronizacion
// para poder escuchar
cEscuchar.signal();
mutex.leave();
return 0;
}


}

Muchas gracias por adelantado. [/img]