generalize definition of busy interval

The definition of busy interval can be generalized
to an arbitrary processor state model without
affecting other parts of the project.

analysis/definitions/busy_interval.v

@@ -13,12 +13,16 @@ Section BusyIntervalJLFP.
   Context `{JobArrival Job}.
   Context `{JobCost Job}.    
 
-  (** Consider any arrival sequence with consistent arrivals. *)
+  (** Consider any kind of processor state model. *)
+  Context {PState : Type}.
+  Context `{ProcessorState Job PState}.  
+
+  (** Consider any arrival sequence with consistent arrivals ... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
   
-  (** Next, consider any ideal uniprocessor schedule of this arrival sequence. *)
-  Variable sched : schedule (ideal.processor_state Job).
+  (** ... and a schedule of this arrival sequence. *)
+  Variable sched : schedule PState.
   
   (** Assume a given JLFP policy. *)
   Context `{JLFP_policy Job}. 
@@ -89,4 +93,4 @@ Section BusyIntervalJLFP.
 
   End DecidableQuietTime.
 
-End BusyIntervalJLFP.
\ No newline at end of file
+End BusyIntervalJLFP.