Library rt.restructuring.model.arrival.sporadic
From rt.restructuring.behavior Require Export arrival_sequence.
From rt.restructuring.model Require Export task.
Section TaskMinInterArrivalTime.
Context {Task : TaskType}.
Variable (task_min_inter_arrival_time : duration).
Definition valid_task_min_inter_arrival_time :=
task_min_inter_arrival_time > 0.
Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.
Variable arr_seq : arrival_sequence Job.
Definition respects_sporadic_task_model (tsk : Task) (d : duration) :=
∀ (j j': Job),
j ≠ j' → (* Given two different jobs j and j' ... *)
arrives_in arr_seq j → (* ...that belong to the arrival sequence... *)
arrives_in arr_seq j' →
job_task j = tsk →
job_task j' = tsk → (* ... and that are spawned by the same task, ... *)
job_arrival j ≤ job_arrival j' → (* ... if the arrival of j precedes the arrival of j' ..., *)
(* then the arrival of j and the arrival of j' are separated by at least one period. *)
job_arrival j' ≥ job_arrival j + d.
End TaskMinInterArrivalTime.
(* Definition of a generic type of parameter for task
minimum inter arrival times *)
Class SporadicModel (Task : TaskType) :=
task_min_inter_arrival_time : Task → duration.
Section SporadicModel.
Context {Task : TaskType} `{SporadicModel Task}.
Variable ts : seq Task.
Definition valid_taskset_min_inter_arrival_times :=
∀ tsk : Task,
tsk \in ts →
task_min_inter_arrival_time tsk > 0.
Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.
Variable arr_seq : arrival_sequence Job.
(* Then, we define the sporadic task model as follows.*)
Definition taskset_respects_sporadic_task_model :=
∀ tsk,
tsk \in ts →
respects_sporadic_task_model arr_seq tsk (task_min_inter_arrival_time tsk).
End SporadicModel.
From rt.restructuring.model Require Export task.
Section TaskMinInterArrivalTime.
Context {Task : TaskType}.
Variable (task_min_inter_arrival_time : duration).
Definition valid_task_min_inter_arrival_time :=
task_min_inter_arrival_time > 0.
Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.
Variable arr_seq : arrival_sequence Job.
Definition respects_sporadic_task_model (tsk : Task) (d : duration) :=
∀ (j j': Job),
j ≠ j' → (* Given two different jobs j and j' ... *)
arrives_in arr_seq j → (* ...that belong to the arrival sequence... *)
arrives_in arr_seq j' →
job_task j = tsk →
job_task j' = tsk → (* ... and that are spawned by the same task, ... *)
job_arrival j ≤ job_arrival j' → (* ... if the arrival of j precedes the arrival of j' ..., *)
(* then the arrival of j and the arrival of j' are separated by at least one period. *)
job_arrival j' ≥ job_arrival j + d.
End TaskMinInterArrivalTime.
(* Definition of a generic type of parameter for task
minimum inter arrival times *)
Class SporadicModel (Task : TaskType) :=
task_min_inter_arrival_time : Task → duration.
Section SporadicModel.
Context {Task : TaskType} `{SporadicModel Task}.
Variable ts : seq Task.
Definition valid_taskset_min_inter_arrival_times :=
∀ tsk : Task,
tsk \in ts →
task_min_inter_arrival_time tsk > 0.
Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.
Variable arr_seq : arrival_sequence Job.
(* Then, we define the sporadic task model as follows.*)
Definition taskset_respects_sporadic_task_model :=
∀ tsk,
tsk \in ts →
respects_sporadic_task_model arr_seq tsk (task_min_inter_arrival_time tsk).
End SporadicModel.