From eab40796e9a32b024994d4e3a7ff1f3097ca0b8b Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Wed, 27 Mar 2024 12:51:14 +0100
Subject: [PATCH] move busy interval definition
---
analysis/abstract/ideal/iw_instantiation.v | 8 ++++----
analysis/abstract/restricted_supply/iw_instantiation.v | 10 +++++-----
.../{busy_interval.v => busy_interval/classical.v} | 0
analysis/definitions/priority_inversion.v | 2 +-
analysis/definitions/sbf/busy.v | 2 +-
analysis/definitions/service_inversion/busy_prefix.v | 2 +-
analysis/definitions/workload/bounded.v | 2 +-
analysis/facts/busy_interval/arrival.v | 2 +-
analysis/facts/busy_interval/quiet_time.v | 2 +-
results/edf/rta/bounded_nps.v | 2 +-
results/fixed_priority/rta/bounded_nps.v | 2 +-
11 files changed, 17 insertions(+), 17 deletions(-)
rename analysis/definitions/{busy_interval.v => busy_interval/classical.v} (100%)
diff --git a/analysis/abstract/ideal/iw_instantiation.v b/analysis/abstract/ideal/iw_instantiation.v
index cad93d2d9..73f0c97ec 100644
--- a/analysis/abstract/ideal/iw_instantiation.v
+++ b/analysis/abstract/ideal/iw_instantiation.v
@@ -357,7 +357,7 @@ Section JLFPInstantiation.
(** We consider an arbitrary time interval <<[t1, t)>> that
starts with a quiet time. *)
Variable t1 t : instant.
- Hypothesis H_quiet_time : busy_interval.quiet_time arr_seq sched j t1.
+ Hypothesis H_quiet_time : classical.quiet_time arr_seq sched j t1.
(** As follows from lemma [cumulative_pred_served_eq_service],
the (abstract) instantiated function of interference is
@@ -389,15 +389,15 @@ Section JLFPInstantiation.
time in the _classical_ sense as [quiet_time_cl], and the
notion of quiet time in the _abstract_ sense as
[quiet_time_ab]. *)
- Let quiet_time_cl := busy_interval.quiet_time arr_seq sched.
+ Let quiet_time_cl := classical.quiet_time arr_seq sched.
Let quiet_time_ab := definitions.quiet_time sched.
(** Same for the two notions of a busy interval prefix ... *)
- Let busy_interval_prefix_cl := busy_interval.busy_interval_prefix arr_seq sched.
+ Let busy_interval_prefix_cl := classical.busy_interval_prefix arr_seq sched.
Let busy_interval_prefix_ab := definitions.busy_interval_prefix sched.
(** ... and the two notions of a busy interval. *)
- Let busy_interval_cl := busy_interval.busy_interval arr_seq sched.
+ Let busy_interval_cl := classical.busy_interval arr_seq sched.
Let busy_interval_ab := definitions.busy_interval sched.
(** Consider any job j of [tsk]. *)
diff --git a/analysis/abstract/restricted_supply/iw_instantiation.v b/analysis/abstract/restricted_supply/iw_instantiation.v
index 615646024..be5e08839 100644
--- a/analysis/abstract/restricted_supply/iw_instantiation.v
+++ b/analysis/abstract/restricted_supply/iw_instantiation.v
@@ -241,7 +241,7 @@ Section JLFPInstantiation.
(** We consider an arbitrary time interval <<[t1, t)>> that
starts with a (classic) quiet time. *)
Variable t1 t : instant.
- Hypothesis H_quiet_time : busy_interval.quiet_time arr_seq sched j t1.
+ Hypothesis H_quiet_time : classical.quiet_time arr_seq sched j t1.
(** As follows from lemma [cumulative_pred_served_eq_service],
the (abstract) instantiated function of interference is
@@ -281,15 +281,15 @@ Section JLFPInstantiation.
time in the _classical_ sense as [quiet_time_cl], and the
notion of quiet time in the _abstract_ sense as
[quiet_time_ab]. *)
- Let quiet_time_cl := busy_interval.quiet_time arr_seq sched.
+ Let quiet_time_cl := classical.quiet_time arr_seq sched.
Let quiet_time_ab := definitions.quiet_time sched.
(** Same for the two notions of a busy interval prefix ... *)
- Let busy_interval_prefix_cl := busy_interval.busy_interval_prefix arr_seq sched.
+ Let busy_interval_prefix_cl := classical.busy_interval_prefix arr_seq sched.
Let busy_interval_prefix_ab := definitions.busy_interval_prefix sched.
(** ... and the two notions of a busy interval. *)
- Let busy_interval_cl := busy_interval.busy_interval arr_seq sched.
+ Let busy_interval_cl := classical.busy_interval arr_seq sched.
Let busy_interval_ab := definitions.busy_interval sched.
(** Consider any job [j] of [tsk]. *)
@@ -454,7 +454,7 @@ Section JLFPInstantiation.
(** ... as well as notions of busy interval prefix. *)
Let busy_interval_prefix_ab := definitions.busy_interval_prefix sched.
- Let busy_interval_prefix_cl := busy_interval.busy_interval_prefix arr_seq sched.
+ Let busy_interval_prefix_cl := classical.busy_interval_prefix arr_seq sched.
(** We assume that the schedule is a work-conserving schedule in
the _classical_ sense, and later prove that the hypothesis
diff --git a/analysis/definitions/busy_interval.v b/analysis/definitions/busy_interval/classical.v
similarity index 100%
rename from analysis/definitions/busy_interval.v
rename to analysis/definitions/busy_interval/classical.v
diff --git a/analysis/definitions/priority_inversion.v b/analysis/definitions/priority_inversion.v
index e4c0914a0..1a3acda30 100644
--- a/analysis/definitions/priority_inversion.v
+++ b/analysis/definitions/priority_inversion.v
@@ -1,4 +1,4 @@
-Require Export prosa.analysis.definitions.busy_interval.
+Require Export prosa.analysis.definitions.busy_interval.classical.
Require Export prosa.analysis.facts.model.scheduled.
(** * Priority Inversion *)
diff --git a/analysis/definitions/sbf/busy.v b/analysis/definitions/sbf/busy.v
index dde4ed2e3..afede54d4 100644
--- a/analysis/definitions/sbf/busy.v
+++ b/analysis/definitions/sbf/busy.v
@@ -1,6 +1,6 @@
Require Export prosa.util.all.
Require Export prosa.analysis.definitions.sbf.pred.
-Require Export prosa.analysis.definitions.busy_interval.
+Require Export prosa.analysis.definitions.busy_interval.classical.
(** * SBF within Busy Interval *)
diff --git a/analysis/definitions/service_inversion/busy_prefix.v b/analysis/definitions/service_inversion/busy_prefix.v
index 424e1f997..21af50763 100644
--- a/analysis/definitions/service_inversion/busy_prefix.v
+++ b/analysis/definitions/service_inversion/busy_prefix.v
@@ -2,7 +2,7 @@ Require Export prosa.model.priority.classes.
Require Export prosa.analysis.facts.behavior.completion.
Require Export prosa.analysis.definitions.service.
Require Export prosa.analysis.definitions.service_inversion.pred.
-Require Export prosa.analysis.definitions.busy_interval.
+Require Export prosa.analysis.definitions.busy_interval.classical.
(** * Service Inversion Bounded *)
(** In this section, we define the notion of bounded cumulative
diff --git a/analysis/definitions/workload/bounded.v b/analysis/definitions/workload/bounded.v
index 2ca86d5e8..b8120624d 100644
--- a/analysis/definitions/workload/bounded.v
+++ b/analysis/definitions/workload/bounded.v
@@ -1,5 +1,5 @@
Require Export prosa.model.aggregate.workload.
-Require Export prosa.analysis.definitions.busy_interval.
+Require Export prosa.analysis.definitions.busy_interval.classical.
(** * Workload Bound in an Interval Starting with Quiet Time *)
(** In this section, we define the notion of a bound on the total
diff --git a/analysis/facts/busy_interval/arrival.v b/analysis/facts/busy_interval/arrival.v
index 5214ede3a..8b7f466ee 100644
--- a/analysis/facts/busy_interval/arrival.v
+++ b/analysis/facts/busy_interval/arrival.v
@@ -1,4 +1,4 @@
-Require Export prosa.analysis.definitions.busy_interval.
+Require Export prosa.analysis.definitions.busy_interval.classical.
(** In this module we collect some basic facts about arrival times in busy
windows. These are primarily useful for proof automation. *)
diff --git a/analysis/facts/busy_interval/quiet_time.v b/analysis/facts/busy_interval/quiet_time.v
index e0ae7fc0a..0b3953d0c 100644
--- a/analysis/facts/busy_interval/quiet_time.v
+++ b/analysis/facts/busy_interval/quiet_time.v
@@ -1,4 +1,4 @@
-Require Export prosa.analysis.definitions.busy_interval.
+Require Export prosa.analysis.definitions.busy_interval.classical.
Require Export prosa.analysis.definitions.carry_in.
(** In this module we collect some basic facts about quiet times. *)
diff --git a/results/edf/rta/bounded_nps.v b/results/edf/rta/bounded_nps.v
index 15ac234bb..1c2f83691 100644
--- a/results/edf/rta/bounded_nps.v
+++ b/results/edf/rta/bounded_nps.v
@@ -4,7 +4,7 @@ Require Export prosa.analysis.facts.busy_interval.pi_bound.
Require Export prosa.analysis.facts.busy_interval.arrival.
Require Export prosa.results.edf.rta.bounded_pi.
Require Export prosa.model.schedule.work_conserving.
-Require Export prosa.analysis.definitions.busy_interval.
+Require Export prosa.analysis.definitions.busy_interval.classical.
Require Export prosa.analysis.facts.blocking_bound.edf.
(** * RTA for EDF with Bounded Non-Preemptive Segments *)
diff --git a/results/fixed_priority/rta/bounded_nps.v b/results/fixed_priority/rta/bounded_nps.v
index 2f67d52b2..5daa8659f 100644
--- a/results/fixed_priority/rta/bounded_nps.v
+++ b/results/fixed_priority/rta/bounded_nps.v
@@ -1,7 +1,7 @@
Require Export prosa.analysis.facts.busy_interval.pi_bound.
Require Export prosa.results.fixed_priority.rta.bounded_pi.
Require Export prosa.model.schedule.work_conserving.
-Require Export prosa.analysis.definitions.busy_interval.
+Require Export prosa.analysis.definitions.busy_interval.classical.
Require Export prosa.analysis.definitions.blocking_bound.fp.
(** * RTA for FP-schedulers with Bounded Non-Preemptive Segments *)
--
GitLab