Library prosa.analysis.facts.periodic.arrival_separation

Require Export prosa.model.task.arrival.periodic_as_sporadic.
Require Export prosa.analysis.facts.sporadic.arrival_times.

In this section we show that the separation between job arrivals of a periodic task is some multiple of their corresponding task's period.
Section JobArrivalSeparation.

Consider periodic tasks with an offset ...
  Context {Task : TaskType}.
  Context `{PeriodicModel Task}.

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

Consider any unique arrival sequence with consistent arrivals, ...
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

... and any task tsk that is to be analyzed.
  Variable tsk : Task.

Assume all tasks have a valid period and respect the periodic task model.
  Hypothesis H_periodic_model: respects_periodic_task_model arr_seq tsk.
  Hypothesis H_valid_period: valid_period tsk.

In this section we show that two consecutive jobs of a periodic task have their arrival times separated by their task's period.
  Section ConsecutiveJobSeparation.

Consider any two consecutive jobs j1 and j2 of task tsk.
    Variable j1 : Job.
    Variable j2 : Job.
    Hypothesis H_j1_from_arr_seq: arrives_in arr_seq j1.
    Hypothesis H_j2_from_arr_seq: arrives_in arr_seq j2.
    Hypothesis H_j1_of_task: job_task j1 = tsk.
    Hypothesis H_j2_of_task: job_task j2 = tsk.
    Hypothesis H_consecutive_jobs: job_index arr_seq j2 = job_index arr_seq j1 + 1.

We show that if job j1 and j2 are consecutive jobs with j2 arriving after j1, then their arrival times are separated by their task's period.
    Lemma consecutive_job_separation:
      job_arrival j2 = job_arrival j1 + task_period tsk.

  End ConsecutiveJobSeparation.

In this section we show that for two unequal jobs of a task, there exists a non-zero multiple of their task's period which separates their arrival times.
  Section ArrivalSeparationWithGivenIndexDifference.

Consider any two consecutive jobs j1 and j2 of task tsk that stem from the arrival sequence.
    Variable j1 j2 : Job.
    Hypothesis H_j1_from_arr_seq: arrives_in arr_seq j1.
    Hypothesis H_j2_from_arr_seq: arrives_in arr_seq j2.
    Hypothesis H_j1_of_task: job_task j1 = tsk.
    Hypothesis H_j2_of_task: job_task j2 = tsk.

We'll assume that job j1 arrives before j2 and that their indices differ by an integer k.
    Variable k : nat.
    Hypothesis H_index_difference_k: job_index arr_seq j1 + k = job_index arr_seq j2 .
    Hypothesis H_job_arrival_lt: job_arrival j1 < job_arrival j2.

We prove that arrival of unequal jobs of a task tsk are separated by a non-zero multiple of task_period tsk provided their index differs by a number k.
    Lemma job_arrival_separation_when_index_diff_is_k:
      ∃ n,
        n > 0 ∧
        job_arrival j2 = job_arrival j1 + n × task_period tsk.

  End ArrivalSeparationWithGivenIndexDifference.

Consider any two distinct jobs j1 and j2 of task tsk that stem from the arrival sequence.
  Variable j1 j2 : Job.
  Hypothesis H_j1_neq_j2: j1 ≠ j2.
  Hypothesis H_j1_from_arr_seq: arrives_in arr_seq j1.
  Hypothesis H_j2_from_arr_seq: arrives_in arr_seq j2.
  Hypothesis H_j1_of_task: job_task j1 = tsk.
  Hypothesis H_j2_of_task: job_task j2 = tsk.

Without loss of generality, we assume that job j1 arrives before job j2.
  Hypothesis H_j1_before_j2: job_arrival j1 ≤ job_arrival j2.

We generalize the above lemma to show that any two unequal jobs of task tsk are separated by a non-zero multiple of task_period tsk.
  Lemma job_sep_periodic:
    ∃ n,
      n > 0 ∧
      job_arrival j2 = job_arrival j1 + n × task_period tsk.

End JobArrivalSeparation.