Library prosa.analysis.facts.periodic.max_inter_arrival

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).
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, ...
... and show that the periodic model respects the task max inter-arrival model.