move busy interval definition

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]. *)

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

analysis/definitions/priority_inversion.v

-Require Export prosa.analysis.definitions.busy_interval.
+Require Export prosa.analysis.definitions.busy_interval.classical.
 Require Export prosa.analysis.facts.model.scheduled.
 
 (** * Priority Inversion *)

analysis/definitions/sbf/busy.v

 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 *)
 

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

analysis/definitions/workload/bounded.v

 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

analysis/facts/busy_interval/arrival.v

-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. *)

analysis/facts/busy_interval/quiet_time.v

-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. *)

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 *)

results/fixed_priority/rta/bounded_nps.v

 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 *)