global workpool	
const int p = 5 # number of processes 
type work = int 
op pool (work) {send};  int count = 0; sem  mutex = 1;
op putwork(int me, work item) {call}
op getwork(int me, var work item) {call} 

body workpool
proc putwork(me, item) {
    P(mutex); count++; V(mutex); write("Worker ", me, " puts ", item); send pool(item)
}

proc getwork(me, item) {
    int workcount  # Warum lokaler Zähler ?
    P(mutex); workcount = count-1; count = workcount; V(mutex)
    if 	(workcount == -p) { # Termination
	item = -1; for [i=1 to p-1] { send pool(item); write("Worker ", me, " puts ", item) }}
    else { receive pool(item); write("Worker ", me, " gets ", item) }
}		
end workpool