Library prosa.analysis.facts.periodic.arrival_times

Require Export prosa.model.task.arrival.periodic_as_sporadic.
Require Export prosa.analysis.facts.periodic.max_inter_arrival.
Require Export prosa.analysis.facts.model.offset.

In this module, we'll prove the known arrival times of jobs that stem from periodic tasks.

Section PeriodicArrivalTimes.

Consider periodic tasks with an offset ...

  Context {Task : TaskType}.
  Context `{TaskOffset Task}.
  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 periodic task tsk with a valid offset and period.

    Variable tsk : Task.
    Hypothesis H_valid_offset: valid_offset arr_seq tsk.
    Hypothesis H_valid_period: valid_period tsk.
    Hypothesis H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk.

We show that the nth job j of task tsk arrives at the instant task_offset tsk + n × task_period tsk.

  Lemma periodic_arrival_times:
    ∀ n (j : Job),
      arrives_in arr_seq j →
      job_task j = tsk →
      job_index arr_seq j = n →
      job_arrival j = task_offset tsk + n × task_period tsk.

We show that for every job j of task tsk there exists a number n such that j arrives at the instant task_offset tsk + n × task_period tsk.

  Lemma job_arrival_times:
    ∀ j,
      arrives_in arr_seq j →
      job_task j = tsk →
      ∃ n , job_arrival j = task_offset tsk + n × task_period tsk.

If a job j of task tsk arrives at task_offset tsk + n × task_period tsk then the job_index of j is equal to n.

  Lemma job_arr_index:
    ∀ n j,
      arrives_in arr_seq j →
      job_task j = tsk →
      job_arrival j = task_offset tsk + n × task_period tsk →
      job_index arr_seq j = n.

End PeriodicArrivalTimes.