Library rt.restructuring.behavior.job

From rt.restructuring.behavior Require Export time.
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 → work.

Definition of a generic type of parameter for job_arrival.
Class JobArrival (Job : JobType) := job_arrival : Job → instant.

Definition of a generic type of parameter relating jobs to an absolute deadline.
Class JobDeadline (Job : JobType) := job_deadline : Job → instant.