# Library prosa.model.priority.edf

Require Export prosa.model.priority.classes.

# EDF Priority Policy

We define what it means for an abstract job-level fixed-priority policy to behave as EDF.
Section EDFPolicy.
Consider jobs with absolute deadlines.
Context {Job : JobType} `{JobDeadline Job}.
A JLFP policy is EDF if it never assigns higher priority to a job with a later absolute deadline. Ties among jobs with equal deadlines may be resolved by any reflexive, transitive, and total tie-breaking rule.
Definition policy_is_EDF (JLFP : JLFP_policy Job) :=
(∀ j1 j2, hep_job j1 j2 →
job_deadline j1 ≤ job_deadline j2)
∧ reflexive_job_priorities JLFP
∧ transitive_job_priorities JLFP
∧ total_job_priorities JLFP.
End EDFPolicy.