Library rt.restructuring.behavior.job
From rt.restructuring.behavior Require Export time.
From mathcomp Require Export eqtype.
(* Throughout the library we assume that jobs have decidable equality *)
Definition JobType := eqType.
(* Definition of a generic type of parameter relating jobs to a discrete cost *)
Class JobCost (J : JobType) := job_cost : J → duration.
(* Definition of a generic type of parameter for job_arrival *)
Class JobArrival (J : JobType) := job_arrival : J → instant.
(* Definition of a generic type of parameter relating jobs to an absolute deadline *)
Class JobDeadline (J : JobType) := job_deadline : J → instant.
(* Definition of a generic type of release jitter parameter. *)
Class JobJitter (J : JobType) := job_jitter : J → duration.
From mathcomp Require Export eqtype.
(* Throughout the library we assume that jobs have decidable equality *)
Definition JobType := eqType.
(* Definition of a generic type of parameter relating jobs to a discrete cost *)
Class JobCost (J : JobType) := job_cost : J → duration.
(* Definition of a generic type of parameter for job_arrival *)
Class JobArrival (J : JobType) := job_arrival : J → instant.
(* Definition of a generic type of parameter relating jobs to an absolute deadline *)
Class JobDeadline (J : JobType) := job_deadline : J → instant.
(* Definition of a generic type of release jitter parameter. *)
Class JobJitter (J : JobType) := job_jitter : J → duration.