Library prosa.behavior.job

From mathcomp Require Export eqtype ssrnat.
Require Export prosa.behavior.time.

Notion of a Job Type

Throughout the library we assume that jobs have decidable equality.
Definition JobType := eqType.

Notion of Work

We define 'work' to denote the amount of service received or needed. In a real system, this corresponds to the number of processor cycles.
Definition work := nat.

Basic Job Parameters — Cost, Arrival Time, and Absolute Deadline

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 relating jobs to an arrival time.
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.