Library prosa.model.priority.edf
EDF Priority Policy
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.
EDF is total.
We add the above lemmas into a "Hint Database" basic_facts, so Coq
will be able to apply them automatically.
Hint Resolve
EDF_is_reflexive
EDF_is_transitive
EDF_is_total
: basic_facts.
EDF_is_reflexive
EDF_is_transitive
EDF_is_total
: basic_facts.