diff --git a/restructuring/analysis/basic_facts/task_arrivals.v b/restructuring/analysis/basic_facts/task_arrivals.v
new file mode 100644
index 0000000000000000000000000000000000000000..ac264c7d6a39db10c90cf916529a3ba3748abbfa
--- /dev/null
+++ b/restructuring/analysis/basic_facts/task_arrivals.v
@@ -0,0 +1,30 @@
+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
diff --git a/restructuring/model/schedule/task_schedule.v b/restructuring/analysis/task_schedule.v
similarity index 96%
rename from restructuring/model/schedule/task_schedule.v
rename to restructuring/analysis/task_schedule.v
index 0a5ef66ec6862d1cdcce23b7fee0bc1e3a4dbe8f..8bc83c0f00f96e58d8d09171c0874a0248fdcf2a 100644
--- a/restructuring/model/schedule/task_schedule.v
+++ b/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)... *)
diff --git a/restructuring/model/arrival/arrival_curves.v b/restructuring/model/arrival/arrival_curves.v
index ea918a5b745712e785d131df1ae717c6f656ed30..e33d68c96fc4d8ef3b7a4cfa7cf1e0942a208a0b 100644
--- a/restructuring/model/arrival/arrival_curves.v
+++ b/restructuring/model/arrival/arrival_curves.v
@@ -1,40 +1,43 @@
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
diff --git a/restructuring/model/task_arrivals.v b/restructuring/model/arrival/task_arrivals.v
similarity index 74%
rename from restructuring/model/task_arrivals.v
rename to restructuring/model/arrival/task_arrivals.v
index 1f5905db06d4278c59b6258b42f4485377ec5424..428f2ede03e36a9f7668f1d01113cb9074c2e240 100644
--- a/restructuring/model/task_arrivals.v
+++ b/restructuring/model/arrival/task_arrivals.v
@@ -1,39 +1,43 @@
-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.