Library prosa.analysis.facts.sporadic.arrival_sequence

Job Arrival Sequence in the Sporadic Model

In this file, we prove basic facts about a task's arrival sequence in the sporadic task model.
Section SporadicArrivals.

Consider sporadic tasks ...
  Context {Task : TaskType} `{SporadicModel Task}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.

Consider any unique arrival sequence with consistent arrivals, ...
... and any sporadic task tsk to be analyzed.
  Variable tsk : Task.

Assume all tasks have valid minimum inter-arrival times, valid offsets, and respect the sporadic task model.
Consider any two jobs from the arrival sequence that stem from task tsk.
  Variable j1 j2 : Job.
  Hypothesis H_j1_from_arrival_sequence: arrives_in arr_seq j1.
  Hypothesis H_j2_from_arrival_sequence: arrives_in arr_seq j2.
  Hypothesis H_j1_task: job_task j1 = tsk.
  Hypothesis H_j2_task: job_task j2 = tsk.

We show that a sporadic task with valid min inter-arrival time cannot have more than one job arriving at any time.
We show that no jobs of the task tsk other than j1 arrive at the same time as j1, and thus the task arrivals at job arrival j1 consists only of job j1.
We show that no jobs of the task tsk other than j1 arrive at the same time as j1, and thus the task arrivals at job arrival j1 consists only of job j1.
  Lemma only_j_at_job_arrival_j:
     t,
      job_arrival j1 = t
      task_arrivals_at arr_seq tsk t = [::j1].

We show that a job j1 is the first job that arrives in task arrivals at job_arrival j1 by showing that the index of job j1 in task_arrivals_at_job_arrival arr_seq j1 is 0.
We observe that for any job j the arrival time of prev_job j is strictly less than the arrival time of j in context of periodic tasks.
We show that task arrivals at job_arrival j1 is the same as task arrivals that arrive between job_arrival j1 and job_arrival j1 + 1.
We show that the task arrivals up to the previous job j1 concatenated with the sequence ::j1 (the sequence containing only the job j1) is same as task arrivals up to job_arrival j1.