Library prosa.model.priority.edf
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.model.priority.classes.
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.
Lemma EDF_is_reflexive : reflexive_priorities.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 40)
Job : JobType
H : JobDeadline Job
arr_seq : arrival_sequence Job
============================
reflexive_priorities
----------------------------------------------------------------------------- *)
Proof. by intros t j; unfold hep_job_at, JLFP_to_JLDP, hep_job, EDF.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 40)
Job : JobType
H : JobDeadline Job
arr_seq : arrival_sequence Job
============================
reflexive_priorities
----------------------------------------------------------------------------- *)
Proof. by intros t j; unfold hep_job_at, JLFP_to_JLDP, hep_job, EDF.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
EDF is transitive.
Lemma EDF_is_transitive : transitive_priorities.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 45)
Job : JobType
H : JobDeadline Job
arr_seq : arrival_sequence Job
============================
transitive_priorities
----------------------------------------------------------------------------- *)
Proof. by intros t y x z; apply leq_trans.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 45)
Job : JobType
H : JobDeadline Job
arr_seq : arrival_sequence Job
============================
transitive_priorities
----------------------------------------------------------------------------- *)
Proof. by intros t y x z; apply leq_trans.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
EDF is total.
Lemma EDF_is_total : total_priorities.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 50)
Job : JobType
H : JobDeadline Job
arr_seq : arrival_sequence Job
============================
total_priorities
----------------------------------------------------------------------------- *)
Proof. by move⇒ t j1 j2; apply leq_total.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End PropertiesOfEDF.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 50)
Job : JobType
H : JobDeadline Job
arr_seq : arrival_sequence Job
============================
total_priorities
----------------------------------------------------------------------------- *)
Proof. by move⇒ t j1 j2; apply leq_total.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End PropertiesOfEDF.
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.