# Library prosa.analysis.facts.periodic.arrival_separation

Require Export prosa.model.task.arrival.periodic_as_sporadic.

Require Export prosa.analysis.facts.sporadic.arrival_times.

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.

Consider periodic tasks with an offset ...

... and any type of jobs associated with these tasks.

Consider any unique arrival sequence with consistent arrivals, ...

Variable arr_seq : arrival_sequence Job.

Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.

Hypothesis H_uniq_arrseq: arrival_sequence_uniq arr_seq.

Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.

Hypothesis H_uniq_arrseq: arrival_sequence_uniq arr_seq.

... and any task tsk that is to be analyzed.

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.

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.

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.

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.

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.

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.

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.

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.

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.

∃ n,

n > 0 ∧

job_arrival j2 = job_arrival j1 + n × task_period tsk.

End ArrivalSeparationWithGivenIndexDifference.

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.

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.

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.

∃ n,

n > 0 ∧

job_arrival j2 = job_arrival j1 + n × task_period tsk.

End JobArrivalSeparation.