Library prosa.classic.implementation.uni.jitter.arrival_sequence

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

Module ConcreteArrivalSequence.

  Import Job ArrivalSequence ConcreteTask ConcreteJob SporadicTaskset TaskArrival.

  Section PeriodicArrivals.

    Variable ts: concrete_taskset.

    Definition add_job (arr_time: time) (tsk: concrete_task) :=
      if task_period tsk %| arr_time then
        Some (Build_concrete_job (arr_time %/ task_period tsk) arr_time
                                 (task_cost tsk) (task_deadline tsk) tsk)
      else
        None.

    Definition periodic_arrival_sequence (t: time) := pmap (add_job t) ts.

  End PeriodicArrivals.

  Section Proofs.

    Variable ts: concrete_taskset.

    Let arr_seq := periodic_arrival_sequence ts.

    Theorem periodic_arrivals_are_consistent:
      arrival_times_are_consistent job_arrival arr_seq.

    Theorem periodic_arrivals_all_jobs_from_taskset:
      ∀ j,
        arrives_in arr_seq j →
        job_task j \in ts.

    Theorem periodic_arrivals_are_sporadic:
      sporadic_task_model task_period job_arrival job_task arr_seq.

    Theorem periodic_arrivals_is_a_set:
      arrival_sequence_is_a_set arr_seq.

    Theorem periodic_arrivals_job_cost_le_task_cost:
      ∀ j,
        arrives_in arr_seq j →
        job_cost j ≤ task_cost (job_task j).

    Theorem periodic_arrivals_job_deadline_eq_task_deadline:
      ∀ j,
        arrives_in arr_seq j →
        job_deadline j = task_deadline (job_task j).

  End Proofs.

End ConcreteArrivalSequence.