# Library prosa.analysis.facts.periodic.max_inter_arrival

Require Export prosa.analysis.facts.periodic.arrival_separation.

## Periodic Task Model respects the Task Max Inter-Arrival model.

In this section, we show that the periodic task model respects the task max inter-arrival model (i.e. consecutive jobs of a task are separated at most by a certain duration specified by the task_max_inter_arrival_time parameter).
Section PeriodicTasksRespectMaxInterArrivalModel.
Consider any type of periodic tasks, ...
Context {Task : TaskType} `{PeriodicModel Task}.
... any type of jobs associated with the tasks, ...
Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.
... and any arrival sequence.
Variable arr_seq : arrival_sequence Job.
By using each task's period as its maximum inter-arrival time, ...
Global Instance max_inter_eq_period : TaskMaxInterArrival Task :=
{
task_max_inter_arrival_time := task_period
}.
... we observe that for any task tsk, task_max_inter_arrival_time tsk is positive, ...
Remark valid_period_is_valid_max_inter_arrival_time :
∀ tsk, valid_period tsk → positive_task_max_inter_arrival_time tsk.
... and show that the periodic model respects the task max inter-arrival model.
Remark periodic_model_respects_max_inter_arrival_model :
∀ tsk,
valid_period tsk →
respects_periodic_task_model arr_seq tsk →
valid_task_max_inter_arrival_time arr_seq tsk.
End PeriodicTasksRespectMaxInterArrivalModel.