diff --git a/analysis/abstract/ideal_jlfp_rta.v b/analysis/abstract/ideal_jlfp_rta.v
index 3e53ea8575c32db13775af0b3524d2803a315781..c27b606f69b2b0b223533f948a31b44c0f6b3281 100644
--- a/analysis/abstract/ideal_jlfp_rta.v
+++ b/analysis/abstract/ideal_jlfp_rta.v
@@ -525,7 +525,7 @@ Section JLFPInstantiation.
(** Based on that, we prove that the concept of busy interval obtained by instantiating the abstract
definition of busy interval coincides with the conventional definition of busy interval. *)
- Lemma instantiated_busy_interval_equivalent_edf_busy_interval:
+ Lemma instantiated_busy_interval_equivalent_busy_interval:
forall t1 t2,
busy_interval_cl j t1 t2 <-> busy_interval_ab j t1 t2.
Proof.
diff --git a/classic/model/schedule/uni/limited/edf/response_time_bound.v b/classic/model/schedule/uni/limited/edf/response_time_bound.v
index 1fe0594a048466a218a5f3a9d3ecc91e4d603860..ad183a638a8d341815723923555ca2a120a660d9 100644
--- a/classic/model/schedule/uni/limited/edf/response_time_bound.v
+++ b/classic/model/schedule/uni/limited/edf/response_time_bound.v
@@ -239,7 +239,7 @@ Module AbstractRTAforEDFwithArrivalCurves.
by subst s; rewrite /scheduled_at SCHED.
}
{ exfalso; clear HYP1 HYP2.
- eapply instantiated_busy_interval_equivalent_edf_busy_interval in BUSY; try done; first last.
+ eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; try done; first last.
{ by rewrite /JLFP_is_reflexive /reflexive /EDF /Priority.EDF. }
{ by apply job_task. }
have EQ:= not_quiet_implies_not_idle
@@ -268,7 +268,7 @@ Module AbstractRTAforEDFwithArrivalCurves.
job_arrival job_cost job_task arr_seq sched tsk interference interfering_workload.
Proof.
intros j t1 t2 ARR TSK POS BUSY.
- eapply instantiated_busy_interval_equivalent_edf_busy_interval in BUSY; try done; first last.
+ eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; try done; first last.
{ by rewrite /JLFP_is_reflexive /reflexive /EDF /Priority.EDF. }
{ by apply job_task. }
eapply all_jobs_have_completed_equiv_workload_eq_service; eauto 2.
@@ -310,7 +310,7 @@ Module AbstractRTAforEDFwithArrivalCurves.
move: EX => [t1 [t2 [H1 [H2 GGG]]]].
exists t1, t2; split; first by done.
split; first by done.
- eapply instantiated_busy_interval_equivalent_edf_busy_interval; eauto 2.
+ eapply instantiated_busy_interval_equivalent_busy_interval; eauto 2.
by unfold JLFP_is_reflexive, reflexive, EDF, Priority.EDF.
Qed.
@@ -354,7 +354,7 @@ Module AbstractRTAforEDFwithArrivalCurves.
- by rewrite ltnW.
}
{ apply H_priority_inversion_is_bounded; try done.
- eapply instantiated_busy_interval_equivalent_edf_busy_interval in BUSY; try done.
+ eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; try done.
{ by move: BUSY => [PREF _]. }
{ by apply job_task. }
{ by rewrite /JLFP_is_reflexive /reflexive /EDF /Priority.EDF. }
diff --git a/classic/model/schedule/uni/limited/fixed_priority/response_time_bound.v b/classic/model/schedule/uni/limited/fixed_priority/response_time_bound.v
index 9809247d093cb939a57bd35dd3b7e88fcbfa8669..72cf994a61e1e6fb071b4e5822f0cf4735c39765 100644
--- a/classic/model/schedule/uni/limited/fixed_priority/response_time_bound.v
+++ b/classic/model/schedule/uni/limited/fixed_priority/response_time_bound.v
@@ -214,7 +214,7 @@ Module AbstractRTAforFPwithArrivalCurves.
- by subst s; rewrite /scheduled_at SCHED.
}
{ exfalso; clear HYP1 HYP2.
- eapply instantiated_busy_interval_equivalent_edf_busy_interval in BUSY; try done; first last.
+ eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; try done; first last.
{ by intros x; apply H_priority_is_reflexive. }
{ by apply job_task. }
have EQ:= not_quiet_implies_not_idle
@@ -244,7 +244,7 @@ Module AbstractRTAforFPwithArrivalCurves.
job_arrival job_cost job_task arr_seq sched tsk interference interfering_workload.
Proof.
intros j t1 t2 ARR TSK POS BUSY.
- eapply instantiated_busy_interval_equivalent_edf_busy_interval in BUSY; first last; try by done.
+ eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; first last; try by done.
{ by intros x; apply H_priority_is_reflexive. }
{ by apply job_task. }
eapply all_jobs_have_completed_equiv_workload_eq_service; eauto 2; intros s ARRs TSKs.
@@ -280,7 +280,7 @@ Module AbstractRTAforFPwithArrivalCurves.
move: EX => [t1 [t2 [H1 [H2 GGG]]]].
exists t1, t2; split; first by done.
split; first by done.
- eapply instantiated_busy_interval_equivalent_edf_busy_interval; eauto 2.
+ eapply instantiated_busy_interval_equivalent_busy_interval; eauto 2.
by intros x; apply H_priority_is_reflexive.
Qed.
@@ -308,7 +308,7 @@ Module AbstractRTAforFPwithArrivalCurves.
move: NCOMPL => /negP COMPL; apply: COMPL.
by rewrite /is_response_time_bound_of_job /completed_by ZERO.
}
- eapply instantiated_busy_interval_equivalent_edf_busy_interval in BUSY; first last; try done.
+ eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; first last; try done.
{ by intros x; apply H_priority_is_reflexive. }
{ by apply job_task. }
have T123 := cumulative_task_interference_split.
diff --git a/classic/model/schedule/uni/limited/jlfp_instantiation.v b/classic/model/schedule/uni/limited/jlfp_instantiation.v
index cce15b2a71d3d5a15499df62662e2d7e43e302f4..e6785217027c314ce3a1a2803c3fc1437584df08 100644
--- a/classic/model/schedule/uni/limited/jlfp_instantiation.v
+++ b/classic/model/schedule/uni/limited/jlfp_instantiation.v
@@ -732,7 +732,7 @@ Module JLFPInstantiation.
(* Based on that, we prove that the concept of busy interval obtained by instantiating the abstract
definition of busy interval coincides with the conventional definition of busy interval. *)
- Lemma instantiated_busy_interval_equivalent_edf_busy_interval:
+ Lemma instantiated_busy_interval_equivalent_busy_interval:
forall t1 t2,
busy_interval job_arrival job_cost arr_seq sched higher_eq_priority j t1 t2 <->
AbstractRTADefinitions.busy_interval job_arrival job_cost sched interference interfering_workload j t1 t2.
diff --git a/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
index b2690aadfdaf25dee3e1f536c0014eb1a38eb9aa..6e4edffa51c2ba0a49cb970a611e4a37213f679f 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -224,7 +224,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
move => /andP [HYP1 HYP2].
ideal_proc_model_sched_case_analysis_eq sched t jo.
{ exfalso; clear HYP1 HYP2.
- eapply instantiated_busy_interval_equivalent_edf_busy_interval in BUSY; eauto 2 with basic_facts.
+ eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; eauto 2 with basic_facts.
move: BUSY => [PREF _].
by eapply not_quiet_implies_not_idle; eauto 2 with basic_facts. }
{ clear EqSched_jo; move: Sched_jo; rewrite scheduled_at_def; move => /eqP EqSched_jo.
@@ -256,7 +256,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
unfold EDF in *.
intros j t1 t2 ARR TSK POS BUSY.
move: H_sched_valid => [CARR MBR].
- eapply instantiated_busy_interval_equivalent_edf_busy_interval in BUSY; eauto 2 with basic_facts.
+ eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; eauto 2 with basic_facts.
eapply all_jobs_have_completed_equiv_workload_eq_service; eauto 2 with basic_facts.
intros s INs TSKs.
rewrite /arrivals_between in INs.
@@ -288,7 +288,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
{ by intros; rewrite {2}H_fixed_point; apply total_workload_le_total_rbf''. }
exists t1, t2; split; first by done.
split; first by done.
- by eapply instantiated_busy_interval_equivalent_edf_busy_interval; eauto 2 with basic_facts.
+ by eapply instantiated_busy_interval_equivalent_busy_interval; eauto 2 with basic_facts.
Qed.
(** Next, we prove that IBF is indeed an interference bound. *)
@@ -344,7 +344,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
+ by rewrite /is_priority_inversion leq_addr.
+ by rewrite ltnW.
- apply H_priority_inversion_is_bounded; try done.
- eapply instantiated_busy_interval_equivalent_edf_busy_interval in H_busy_interval; eauto 2 with basic_facts.
+ eapply instantiated_busy_interval_equivalent_busy_interval in H_busy_interval; eauto 2 with basic_facts.
by move: H_busy_interval => [PREF _].
Qed.
diff --git a/results/fixed_priority/rta/bounded_pi.v b/results/fixed_priority/rta/bounded_pi.v
index 9da4b56238612ffb3426e0c88b714820a23b1e6d..b96b9251549b9dd300b762b84bc17c59b5e810d8 100644
--- a/results/fixed_priority/rta/bounded_pi.v
+++ b/results/fixed_priority/rta/bounded_pi.v
@@ -199,7 +199,7 @@ Section AbstractRTAforFPwithArrivalCurves.
* by exfalso.
* by subst s; rewrite scheduled_at_def //; apply eqprop_to_eqbool.
+ exfalso; clear HYP1 HYP2.
- eapply instantiated_busy_interval_equivalent_edf_busy_interval in BUSY; eauto with basic_facts.
+ eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; eauto with basic_facts.
by move: BUSY => [PREF _]; eapply not_quiet_implies_not_idle;
eauto 2 using eqprop_to_eqbool with basic_facts.
- move: (HYP); rewrite scheduled_at_def; move => /eqP HYP2; apply/negP.
@@ -219,7 +219,7 @@ Section AbstractRTAforFPwithArrivalCurves.
Proof.
intros j t1 t2 ARR TSK POS BUSY.
move: H_sched_valid => [CARR MBR].
- eapply instantiated_busy_interval_equivalent_edf_busy_interval in BUSY; eauto with basic_facts.
+ eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; eauto with basic_facts.
eapply all_jobs_have_completed_equiv_workload_eq_service; eauto with basic_facts.
intros s ARRs TSKs.
move: (BUSY) => [[_ [QT _]] _].
@@ -247,7 +247,7 @@ Section AbstractRTAforFPwithArrivalCurves.
{ by intros; rewrite {2}H_fixed_point leq_add //; apply total_workload_le_total_rbf'. }
exists t1, t2; split; first by done.
split; first by done.
- by eapply instantiated_busy_interval_equivalent_edf_busy_interval; eauto 2 with basic_facts.
+ by eapply instantiated_busy_interval_equivalent_busy_interval; eauto 2 with basic_facts.
Qed.
(** Next, we prove that IBF is indeed an interference bound.
@@ -271,7 +271,7 @@ Section AbstractRTAforFPwithArrivalCurves.
move: H_sched_valid => [CARR MBR].
move: (posnP (@job_cost _ Cost j)) => [ZERO|POS].
{ by exfalso; rewrite /completed_by ZERO in NCOMPL. }
- eapply instantiated_busy_interval_equivalent_edf_busy_interval in BUSY; eauto 2 with basic_facts.
+ eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; eauto 2 with basic_facts.
rewrite /interference; erewrite cumulative_task_interference_split; eauto 2 with basic_facts; last first.
{ move: BUSY => [[_ [_ [_ /andP [GE LT]]]] _].
by eapply arrived_between_implies_in_arrivals; eauto 2. }