Library prosa.classic.model.arrival.jitter.task_arrival

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job.
Require Import prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.arrival.jitter.arrival_sequence.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path.

Module TaskArrivalWithJitter.

  Import ArrivalSequenceWithJitter SporadicTaskset.
  Export TaskArrival.

  Section NumberOfArrivals.

    Context {Task: eqType}.
    Context {Job: eqType}.
    Variable job_arrival: Job → time.
    Variable job_jitter: Job → time.
    Variable job_task: Job → Task.

    Variable arr_seq: arrival_sequence Job.

    Let arrivals_between := actual_arrivals_between job_arrival job_jitter arr_seq.

    Variable tsk: Task.

    Definition is_job_of_tsk := is_job_of_task job_task tsk.

    Definition actual_arrivals_of_task_between (t1 t2: time) :=
      [seq j <- arrivals_between t1 t2 | is_job_of_tsk j].

    Definition num_actual_arrivals_of_task (t1 t2: time) :=
      size (actual_arrivals_of_task_between t1 t2).

  End NumberOfArrivals.

  Section DistanceBetweenSporadicJobs.

    Context {Task: eqType}.
    Variable task_period: Task → time.

    Context {Job: eqType}.
    Variable job_arrival: Job → time.
    Variable job_jitter: Job → time.
    Variable job_task: Job → Task.

    Variable arr_seq: arrival_sequence Job.
    Hypothesis H_consistent_arrivals: arrival_times_are_consistent job_arrival arr_seq.
    Hypothesis H_no_duplicate_arrivals: arrival_sequence_is_a_set arr_seq.

    Hypothesis H_sporadic_jobs:
      sporadic_task_model task_period job_arrival job_task arr_seq.

    Let actual_job_arrival := actual_arrival job_arrival job_jitter.

    Variable tsk: Task.

    Variable t1 t2: time.

    Let arriving_jobs := actual_arrivals_of_task_between job_arrival job_jitter
                                                         job_task arr_seq tsk t1 t2.
    Let num_arrivals := num_actual_arrivals_of_task job_arrival job_jitter job_task arr_seq tsk t1 t2.

    Let by_arrival_time j j' := job_arrival j ≤ job_arrival j'.
    Let sorted_jobs := sort by_arrival_time arriving_jobs.

    Variable elem: Job.
    Let nth_job := nth elem sorted_jobs.

    Remark sorted_arrivals_properties_of_nth:
      ∀ idx,
        idx < num_arrivals →
        t1 ≤ actual_job_arrival (nth_job idx) < t2 ∧
        job_task (nth_job idx) = tsk ∧
        arrives_in arr_seq (nth_job idx).

    Lemma sorted_arrivals_current_differs_from_next:
      ∀ idx,
        idx < num_arrivals.-1 →
        nth_job idx ≠ nth_job idx.+1.

    Lemma sorted_arrivals_separated_by_period:
      ∀ idx,
        idx < num_arrivals.-1 →
        job_arrival (nth_job idx.+1) ≥ job_arrival (nth_job idx) + task_period tsk.

    Section FirstAndLastJobs.

      Hypothesis H_at_least_one_job:
        num_arrivals ≥ 1.

      Let j_first := nth_job 0.
      Let j_last := nth_job (num_arrivals.-1).
      Let a_first := job_arrival j_first.
      Let a_last := job_arrival j_last.

      Lemma sorted_arrivals_distance_from_first_job:
        ∀ idx,
          idx < num_arrivals →
          job_arrival (nth_job idx) ≥ a_first + idx × task_period tsk.

      Corollary sorted_arrivals_distance_between_first_and_last:
        a_last ≥ a_first + (num_arrivals-1) × task_period tsk.

    End FirstAndLastJobs.

  End DistanceBetweenSporadicJobs.

End TaskArrivalWithJitter.