# Library prosa.model.priority.edf

# EDF Priority Policy

#[export] Instance EDF (Job : JobType) `{JobDeadline Job} : JLFP_policy Job :=

{

hep_job (j1 j2 : Job) := job_deadline j1 ≤ job_deadline j2

}.

{

hep_job (j1 j2 : Job) := job_deadline j1 ≤ job_deadline j2

}.

In this section, we prove a few properties about EDF policy.

Consider any type of jobs with deadlines.

Consider any arrival sequence.

EDF is reflexive.

EDF is transitive.

Lemma EDF_is_transitive : transitive_job_priorities (EDF Job).

Proof. by move⇒ y x z; apply: leq_trans. Qed.

Proof. by move⇒ y x z; apply: leq_trans. Qed.

EDF is total.

Lemma EDF_is_total : total_job_priorities (EDF Job).

Proof. by move⇒ j1 j2; apply: leq_total. Qed.

End PropertiesOfEDF.

Proof. by move⇒ j1 j2; apply: leq_total. Qed.

End PropertiesOfEDF.

We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq
will be able to apply them automatically.

Global Hint Resolve

EDF_is_reflexive

EDF_is_transitive

EDF_is_total

: basic_rt_facts.

EDF_is_reflexive

EDF_is_transitive

EDF_is_total

: basic_rt_facts.