pcp_scheduler {Semaphore : TYPE; 
               NumberOfTasks : NATURAL, 
               task_descriptors : pcp_task{Semaphore; NumberOfTasks}!TaskDescriptors
              } : CONTEXT =
BEGIN

  taskCtx : CONTEXT = pcp_task{Semaphore; NumberOfTasks};

  rsrcCtx : CONTEXT = pcp_rsrc{Semaphore; NumberOfTasks, task_descriptors};

  jobSetCtx : CONTEXT = set{taskCtx!JobIdx;};

  semSetCtx : CONTEXT = set{Semaphore;};

  JobIdx : TYPE = taskCtx!JobIdx;

  RSRC : TYPE = rsrcCtx!RSRC;

  period(j : JobIdx) : NATURAL =
    taskCtx!period(j, task_descriptors);

  budget(j : JobIdx) : NATURAL = 
    taskCtx!budget(j, task_descriptors);
	
  lcm(m : NATURAL, n : NATURAL) : NATURAL = math!lcm(m,n);

  % maximum period should be the lcm of the period of each task.
  compute_max_period(result : NATURAL, i : NATURAL) : NATURAL = 
    IF i <= NumberOfTasks 
    THEN compute_max_period(lcm(result, period(i)), i+1)
    ELSE result ENDIF; 

  max_period : NATURAL = 
	  IF NumberOfTasks = 0 THEN 1
    ELSIF NumberOfTasks = 1 THEN period(1)
    ELSE compute_max_period(period(1), 2) ENDIF;  

  compute_max_budget(result : NATURAL, i : NATURAL) : NATURAL =
		IF i <= NumberOfTasks
		THEN compute_max_budget(max(result, budget(i)), i+1)
		ELSE result ENDIF;
		
  max_budget : NATURAL =
		IF NumberOfTasks = 0 THEN 0
		ELSIF NumberOfTasks = 1 THEN budget(1)
		ELSE compute_max_budget(budget(1), 2) ENDIF;

  ClockRange : TYPE = [0..(max_period - 1)];
	PC : TYPE = [0..max_budget]; % PC = 0 means the process is sleeping 

  adjust(val : NATURAL) : ClockRange =
    IF val < max_period THEN val
    ELSE val - max_period ENDIF;

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

  uses_sem?(j : JobIdx, s : Semaphore) : BOOLEAN = rsrcCtx!uses_sem?(j, s);

  ceiling(s : Semaphore) : NATURAL = rsrcCtx!ceiling(s);

  blocked?(r : RSRC, j : JobIdx) : BOOLEAN = rsrcCtx!blocked?(r, j);

  blk(r : RSRC, j : JobIdx) : jobSetCtx!Set = rsrcCtx!blk(r, j);

  % In the absence of blocking, jobs of high priority are executed first
  precedes?(j : JobIdx, k : JobIdx) : BOOLEAN =
    priority(j) >= priority(k);

  JobState : TYPE = ARRAY JobIdx OF PC;
  
  sleeping?(j : JobIdx, job_state : JobState) : BOOLEAN =
		job_state[j] = 0;

  end_of_budget?(j : JobIdx, job_state : JobState) : BOOLEAN =
		job_state[j] = budget(j);

  ready_to_execute?(j : JobIdx, job_state : JobState) : BOOLEAN =
		NOT sleeping?(j, job_state);

  topjob?(j : JobIdx, rsrc : RSRC, job_state : JobState) : BOOLEAN =
    ready_to_execute?(j, job_state) AND
    (FORALL (k : JobIdx): ready_to_execute?(k, job_state) => precedes?(j, k));

  eligible?(j : JobIdx, rsrc : RSRC, job_state : JobState) : BOOLEAN =
    (topjob?(j, rsrc, job_state) AND NOT blocked?(rsrc, j))
    OR
    (EXISTS (k : JobIdx): topjob?(k, rsrc, job_state) AND 
	                        blocked?(rsrc, k) AND 
                          jobSetCtx!contains?(blk(rsrc, k), j));

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

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

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

  step(r : RSRC, j : JobIdx) : RSRC =
    rsrcCtx!wakeup(r, j);
   
  Turn : TYPE = DATATYPE
                  job_turn(job_turn_id : JobIdx),
                  idle_turn
                END;

  Command : TYPE = DATATYPE
                     cmd_lock(cmd_lock_s : Semaphore),
                     cmd_unlock(cmd_unlock_s : Semaphore),
                     cmd_unlock_all,
	                   cmd_step
                   END; 

  valid_command?(j : JobIdx, c : Command) : BOOLEAN =
    (IF cmd_lock?(c) THEN uses_sem?(j, cmd_lock_s(c))
     ELSIF cmd_unlock?(c) THEN uses_sem?(j, cmd_unlock_s(c))
     ELSE TRUE ENDIF);

  turn?(t : Turn, j : JobIdx) : BOOLEAN =
    job_turn?(t) AND job_turn_id(t) = j;

  scheduler : MODULE = 
  BEGIN
    LOCAL  clock : ClockRange
    LOCAL  dispatch : ARRAY JobIdx OF ClockRange
		LOCAL  job_state : JobState
    OUTPUT turn : Turn
    LOCAL  rsrc : RSRC
    INPUT  cmd : Command
    INITIALIZATION
      clock = 0;
      dispatch = [ [j : JobIdx] 0];
      job_state = [ [j : JobIdx] 0];
      rsrc = rsrcCtx!initial_rsrc;
      turn = idle_turn
    TRANSITION
      clock' = adjust(clock + 1);
      job_state' = [ [j : JobIdx] 
										 IF sleeping?(j, job_state) AND dispatch[j] = clock THEN 1
										 ELSIF turn?(turn, j) THEN
                       IF end_of_budget?(j, job_state) THEN 0 % go to sleep
                       ELSE job_state[j] + 1 ENDIF % increase the program counter   
                     ELSE job_state[j] ENDIF ]; 
      dispatch' = [ [j : JobIdx] 
                    IF dispatch[j] = clock 
                    THEN adjust(dispatch[j] + period(j)) 
                    ELSE dispatch[j] ENDIF];
      rsrc' = (IF turn = idle_turn 
               THEN rsrc
               ELSE LET j : JobIdx = job_turn_id(turn) IN
                      IF end_of_budget?(j, job_state) THEN unlock_all(rsrc, j) % ignore the cmd...
	   						 	 	  ELSIF cmd_lock?(cmd) AND uses_sem?(j, cmd_lock_s(cmd)) THEN lock(rsrc, j, cmd_lock_s(cmd))
                      ELSIF cmd_unlock?(cmd) AND uses_sem?(j, cmd_unlock_s(cmd)) THEN unlock(rsrc, j, cmd_unlock_s(cmd))
				  				    ELSIF cmd_unlock_all?(cmd) THEN unlock_all(rsrc, j)
                      ELSE rsrc ENDIF
               ENDIF);
      [
        ([] (j : JobIdx ) : eligible?(j, rsrc, job_state') --> turn' = job_turn(j))
        []
        ELSE --> turn' = idle_turn
      ]
  END; 

  deadline_missed? (dispatch : ARRAY JobIdx OF ClockRange,
                    job_state : JobState,
                    clock : ClockRange) : BOOLEAN =
    (EXISTS (j : JobIdx) : dispatch[j] = clock AND NOT sleeping?(j, job_state));

  deadlock? (job_state : JobState, t : Turn) : BOOLEAN =
    idle_turn?(t) AND (EXISTS (j : JobIdx) : ready_to_execute?(j, job_state));

  consistent1? (job_state : JobState) : BOOLEAN =
    (FORALL (j : JobIdx) : job_state[j] <= budget(j));

END