Restructure task arrivals

restructuring/analysis/basic_facts/task_arrivals.v

+From rt.restructuring.model Require Export arrival.task_arrivals.
+
+(* In this file we provide basic properties related to tasks on arrival sequences. *)
+Section TaskArrivals.
+
+  (* Consider any type of job associated with any type of tasks. *)
+  Context {Job : JobType}.
+  Context {Task : TaskType}.
+  Context `{JobTask Job Task}.
+
+  (* Consider any job arrival sequence. *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (* Let tsk be any task. *)
+  Variable tsk : Task.
+
+  (* We show that the number of arrivals of task can be split into disjoint intervals. *) 
+  Lemma num_arrivals_of_task_cat:
+    forall t t1 t2,
+      t1 <= t <= t2 ->
+      number_of_task_arrivals arr_seq tsk t1 t2 =
+      number_of_task_arrivals arr_seq tsk t1 t + number_of_task_arrivals arr_seq tsk t t2.
+  Proof.
+    move => t t1 t2 /andP [GE LE].
+    rewrite /number_of_task_arrivals /task_arrivals_between /arrivals_between. 
+    rewrite (@big_cat_nat _ _ _ t) //=.
+      by rewrite filter_cat size_cat.
+  Qed.
+
+End TaskArrivals.
\ No newline at end of file

restructuring/model/schedule/task_schedule.v → restructuring/analysis/task_schedule.v

@@ -37,7 +37,7 @@ Section ScheduleOfTask.
       else false.
 
     (* ...which also corresponds to the instantaneous service it receives. *)
-    Definition task_service_at (t: instant) := task_scheduled_at t.
+    Definition task_service_at (t : instant) := task_scheduled_at t.
 
     (* Based on the notion of instantaneous service, we define the
        cumulative service received by tsk during any interval [t1, t2)... *)

restructuring/model/arrival/arrival_curves.v

 From rt.util Require Import all.
 From rt.restructuring.behavior Require Export arrival_sequence.
-From rt.restructuring.model Require Export task_arrivals.
+From rt.restructuring.model Require Import task_arrivals.
 
 (* In this section, we define the notion of arrival curves, which
    can be used to reason about the frequency of job arrivals. *)
 Section ArrivalCurves.
 
-  Context {Task: TaskType}.
-  Context {Job: JobType}.
+  (* Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+
+  (*  ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
   Context `{JobTask Job Task}.
 
-  (* Consider any job arrival sequence. *)
-  Variable arr_seq: arrival_sequence Job.
+ (* Consider any job arrival sequence. *)
+  Variable arr_seq : arrival_sequence Job.
 
   (* First, we define what constitutes an arrival bound for a task. *)
   Section ArrivalCurves.
 
-    (* We say that num_arrivals is a valid arrival curve for task tsk iff *)
-    (* [num_arrivals] is a monotonic function that equals 0 for the empty *)
-    (* interval delta = 0. *)
-    Definition valid_arrival_curve (tsk: Task) (num_arrivals: duration -> nat) :=
+    (* We say that num_arrivals is a valid arrival curve for task tsk iff
+       [num_arrivals] is a monotonic function that equals 0 for the empty 
+       interval delta = 0. *)
+    Definition valid_arrival_curve (tsk : Task) (num_arrivals : duration -> nat) :=
       num_arrivals 0 = 0 /\
       monotone num_arrivals leq.
 
     (* We say that max_arrivals is an upper arrival bound for tsk iff, for any interval [t1, t2),
-     [max_arrivals (t2 - t1)] bounds the number of jobs of tsk that arrive in that interval. *)
-    Definition respects_max_arrivals (tsk: Task) (max_arrivals: duration -> nat) :=
-      forall (t1 t2: instant),
+       [max_arrivals (t2 - t1)] bounds the number of jobs of tsk that arrive in that interval. *)
+    Definition respects_max_arrivals (tsk : Task) (max_arrivals : duration -> nat) :=
+      forall (t1 t2 : instant),
         t1 <= t2 ->
-        size (task_arrivals_between arr_seq tsk t1 t2) <= max_arrivals (t2 - t1).
+        number_of_task_arrivals arr_seq tsk t1 t2 <= max_arrivals (t2 - t1).
 
-    (* We define in the same way lower arrival bounds *)
-    Definition respects_min_arrivals (tsk: Task) (min_arrivals: duration -> nat) :=
-      forall (t1 t2: instant),
+    (* We define in the same way lower arrival bounds. *)
+    Definition respects_min_arrivals (tsk : Task) (min_arrivals : duration -> nat) :=
+      forall (t1 t2 : instant),
         t1 <= t2 ->
-        min_arrivals (t2 - t1) <= size (task_arrivals_between arr_seq tsk t1 t2).
+        min_arrivals (t2 - t1) <= number_of_task_arrivals arr_seq tsk t1 t2.
 
   End ArrivalCurves.
 
@@ -43,60 +46,68 @@ Section ArrivalCurves.
     (* Then, we say that min_separation is a lower separation bound iff, for any number of jobs
        of tsk, min_separation lower-bounds the minimum interval length in which that number
        of jobs can be spawned. *)
-    Definition respects_min_separation tsk (min_separation: nat -> duration) :=
+    Definition respects_min_separation (tsk : Task) (min_separation: nat -> duration) :=
       forall t1 t2,
           t1 <= t2 ->
-          min_separation (size (task_arrivals_between arr_seq tsk t1 t2)) <= t2 - t1.
+          min_separation (number_of_task_arrivals arr_seq tsk t1 t2) <= t2 - t1.
 
     (* We define in the same way upper separation bounds *)
-    Definition respects_max_separation tsk (max_separation: nat -> duration):=
+    Definition respects_max_separation (tsk : Task) (max_separation: nat -> duration):=
       forall t1 t2,
         t1 <= t2 ->
-        t2 - t1 <= max_separation (size (task_arrivals_between arr_seq tsk t1 t2)).
+        t2 - t1 <= max_separation (number_of_task_arrivals arr_seq tsk t1 t2).
 
   End SeparationBound.
 
 End ArrivalCurves.
 
 (* We define generic classes for arrival curves  *)
-Class MaxArrivals (Task: TaskType) := max_arrivals: Task -> duration -> nat.
+Class MaxArrivals (Task : TaskType) := max_arrivals : Task -> duration -> nat.
 
-Class MinArrivals (Task: TaskType) := min_arrivals: Task -> duration -> nat.
+Class MinArrivals (Task : TaskType) := min_arrivals : Task -> duration -> nat.
 
-Class MaxSeparation (Task: TaskType) := max_separation: Task -> nat -> duration.
+Class MaxSeparation (Task : TaskType) := max_separation : Task -> nat -> duration.
 
-Class MinSeparation (Task: TaskType) := min_separation: Task -> nat -> duration.
+Class MinSeparation (Task : TaskType) := min_separation : Task -> nat -> duration.
 
 Section ArrivalCurvesModel.
 
-  Context {Task: TaskType} {Job: JobType}.
+  (* Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+
+  (*  ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
   Context `{JobTask Job Task}.
 
-  Context `{MaxArrivals Task} `{MinArrivals Task} `{MaxSeparation Task} `{MinSeparation Task}.
+  (* Consider any job arrival sequence... *)
+  Variable arr_seq : arrival_sequence Job.
 
-  Variable ts: seq Task.
+  (* ..and all the classes of arrival curves. *) 
+  Context `{MaxArrivals Task}
+          `{MinArrivals Task}
+          `{MaxSeparation Task}
+          `{MinSeparation Task}.
+
+  (* Let ts be an arbitrary task set. *)
+  Variable ts : seq Task.
 
   (* We say that arrivals is a valid arrival curve for a taskset if it is valid for any task
      in the taskset *)
   Definition valid_taskset_arrival_curve (arrivals : Task -> duration -> nat) :=
-    forall tsk,
-      tsk \in ts ->
-      valid_arrival_curve tsk (arrivals tsk).
-
-  Variable arr_seq: arrival_sequence Job.
+    forall (tsk : Task), tsk \in ts -> valid_arrival_curve tsk (arrivals tsk).
 
   (* We say that max_arrivals is an arrival bound for taskset ts *)
   (* iff max_arrival is an arrival bound for any task from ts. *)
   Definition taskset_respects_max_arrivals :=
-    forall (tsk: Task), tsk \in ts -> respects_max_arrivals arr_seq tsk (max_arrivals tsk).
+    forall (tsk : Task), tsk \in ts -> respects_max_arrivals arr_seq tsk (max_arrivals tsk).
 
   Definition taskset_respects_min_arrivals :=
-    forall (tsk: Task), tsk \in ts -> respects_min_arrivals arr_seq tsk (min_arrivals tsk).
+    forall (tsk : Task), tsk \in ts -> respects_min_arrivals arr_seq tsk (min_arrivals tsk).
 
   Definition taskset_respects_max_separation :=
-    forall (tsk: Task), tsk \in ts -> respects_max_separation arr_seq tsk (max_separation tsk).
+    forall (tsk : Task), tsk \in ts -> respects_max_separation arr_seq tsk (max_separation tsk).
 
   Definition taskset_respects_min_separation :=
-    forall (tsk: Task), tsk \in ts -> respects_min_separation arr_seq tsk (min_separation tsk).
+    forall (tsk : Task), tsk \in ts -> respects_min_separation arr_seq tsk (min_separation tsk).
 
 End ArrivalCurvesModel.
\ No newline at end of file

restructuring/model/task_arrivals.v → restructuring/model/arrival/task_arrivals.v

-From rt.restructuring.behavior Require Export arrival_sequence.
 From rt.restructuring.model Require Export task.
 
-(* In this file we provide basic definitions related to tasks on arrival sequences *)
+(* In this file we provide basic definitions related to tasks on arrival sequences. *)
 Section TaskArrivals.
 
   (* Consider any type of job associated with any type of tasks. *)
-  Context {Job: JobType}.
-  Context {Task: TaskType}.
+  Context {Job : JobType}.
+  Context {Task : TaskType}.
   Context `{JobTask Job Task}.
 
   (* Consider any job arrival sequence. *)
-  Variable arr_seq: arrival_sequence Job.
+  Variable arr_seq : arrival_sequence Job.
 
   Section Definitions.
 
     (* Let tsk be any task. *)
     Variable tsk : Task.
 
-    (* We define the sequence of jobs of tsk arriving at time t *)
+    (* We define the sequence of jobs of tsk arriving at time t. *)
     Definition task_arrivals_at (t : instant) : seq Job :=
       [seq j <- arrivals_at arr_seq t | job_task j == tsk].
 
     (* By concatenation, we construct the list of jobs of tsk that arrived in the
-     interval [t1, t2). *)
+       interval [t1, t2). *)
     Definition task_arrivals_between (t1 t2 : instant) :=
       [seq j <- arrivals_between arr_seq t1 t2 | job_task j == tsk].
 
     (* Based on that, we define the list of jobs of tsk that arrived up to time t, ...*)
     Definition task_arrivals_up_to (t : instant) := task_arrivals_between 0 t.+1.
 
-    (* ...and the list of jobs of tsk that arrived strictly before time t. *)
+    (* ...and the list of jobs of tsk that arrived strictly before time t ... *)
     Definition task_arrivals_before (t : instant) := task_arrivals_between 0 t.
+
+    (* ... and also count the number of job arrivals. *)
+    Definition number_of_task_arrivals (t1 t2 : instant) :=
+      size (task_arrivals_between t1 t2).
+    
   End Definitions.
 
-  (* We define a predicate for arrival sequences for which jobs come from a taskset *)
+  (* We define a predicate for arrival sequences for which jobs come from a taskset. *)
   Definition arrivals_come_from_taskset (ts : seq Task) :=
     forall j, arrives_in arr_seq j -> job_task j \in ts.