introduce 'work' as unit of service received or needed

restructuring/behavior/job.v

@@ -4,8 +4,12 @@ From mathcomp Require Export eqtype ssrnat.
 (* Throughout the library we assume that jobs have decidable equality. *)
 Definition JobType := eqType.
 
+(* We define 'work' to denote the unit of service received or needed. In a
+   real system, this corresponds to the number of processor cycles. *)
+Definition work  := nat.
+
 (* Definition of a generic type of parameter relating jobs to a discrete cost. *)
-Class JobCost (Job : JobType) := job_cost : Job -> duration.
+Class JobCost (Job : JobType) := job_cost : Job -> work.
 
 (* Definition of a generic type of parameter for job_arrival. *)
 Class JobArrival (Job : JobType) := job_arrival : Job -> instant.

restructuring/behavior/schedule.v

@@ -12,7 +12,7 @@ Class ProcessorState (Job : JobType) (State : Type) :=
     scheduled_in: Job -> State -> bool;
     (* For a given processor state, the [service_in] function determines how much
        service a given job receives in that state. *)
-    service_in: Job -> State -> nat;
+    service_in: Job -> State -> work;
     (* For a given processor state, a job does not receive service if it is not scheduled
        in that state *)
     service_implies_scheduled :