Library prosa.behavior.job

Require Export prosa.util.all.
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.
Definition of a generic type of parameter relating jobs to an absolute deadline.