pcp_generic {; NumberOfTasks : NATURAL, 
               NumberOfSemaphores : NATURAL,
               tasks : pcp_task{[1..NumberOfSemaphores]; NumberOfTasks}!TaskDescriptors,
               budgets : ARRAY [1..NumberOfTasks] OF NATURAL
            } : CONTEXT =
BEGIN

  Semaphore : TYPE = [1..NumberOfSemaphores];

  semSetCtx : CONTEXT = simple_set{Semaphore;};

  SemSet : TYPE = semSetCtx!Set;

  taskCtx : CONTEXT = pcp_task{Semaphore; NumberOfTasks};

  JobIdx : TYPE = taskCtx!JobIdx;
  
  rsrcCtx : CONTEXT = pcp_rsrc{Semaphore; NumberOfTasks, tasks};

  RSRC : TYPE = rsrcCtx!RSRC;

  schCtx : CONTEXT = pcp_scheduler{Semaphore; NumberOfTasks, tasks};
  
  Turn : TYPE = schCtx!Turn;

  alloc_step(r : RSRC, j : JobIdx, s : Semaphore) : RSRC =
    rsrcCtx!alloc_step(r,j,s);

  release_step(r : RSRC, j : JobIdx, s : Semaphore) : RSRC =
    rsrcCtx!release_step(r,j,s);

  turn?(t : Turn, j : JobIdx) : BOOLEAN = schCtx!turn?(t, j);

  JobStatus : TYPE = schCtx!JobStatus;

  precedes?(j : JobIdx, k : JobIdx) : BOOLEAN =
    schCtx!precedes?(j,k);

  priority(j : JobIdx) : NATURAL =
    schCtx!priority(j);

  lock(r : RSRC, j : JobIdx, s : Semaphore) : RSRC =
		schCtx!lock(r,j,s);

  unlock(r : RSRC, j : JobIdx, s : Semaphore) : RSRC = 
    schCtx!unlock(r,j,s);

  unlock_all(r : RSRC, j : JobIdx) : RSRC = 
    schCtx!unlock_all(r,j);

  step(r : RSRC, j : JobIdx) : RSRC =
    schCtx!step(r,j);

  uses?(j : JobIdx, s : Semaphore) : BOOLEAN =
    semSetCtx!contains?(s, tasks[j].semaphores);

  job [id : JobIdx] : MODULE =
  BEGIN
    INPUT turn : Turn
    OUTPUT status : JobStatus
    GLOBAL rsrc : RSRC
    OUTPUT pc : [1..budgets[id]]
  INITIALIZATION
    status = schCtx!finished;
    pc = 1
	TRANSITION
    [
      ([] (s : Semaphore) : pc < budgets[id] AND turn?(turn', id) AND 
                            uses?(id, s) --> 
            status' = IF pc = 1 THEN schCtx!started ELSE status ENDIF;
            rsrc' IN {lock(rsrc, id, s),
                      step(rsrc, id),
                      unlock(rsrc, id, s)};
            pc' = pc + 1)
      []      
      pc = budgets[id] AND turn?(turn', id) --> rsrc' = unlock_all(rsrc, id);
                                                status' = schCtx!finished;
                                                pc' = 1
    ]
  END;

  system : MODULE = 
	  schCtx!scheduler ||
	  ((WITH OUTPUT job_status : ARRAY JobIdx OF JobStatus;
	         OUTPUT job_pc : ARRAY JobIdx OF NATURAL
		([] (j : JobIdx) : RENAME status TO job_status[j],
                              pc TO job_pc[j]
                       IN job[j]))
    []
    schCtx!idle_process);  

  JobState : TYPE = schCtx!JobState;
  deadlock? (job_state : ARRAY JobIdx OF JobState, t : Turn) : BOOLEAN = schCtx!deadlock?(job_state, t);

  deadline_missed? (dispatch : ARRAY JobIdx OF schCtx!ClockRange,
                    job_state : ARRAY JobIdx OF BOOLEAN,
                    clock : schCtx!ClockRange) : BOOLEAN = schCtx!deadline_missed?(dispatch, job_state, clock);

END