Library prosa.classic.implementation.global.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.
Require Import prosa.classic.model.schedule.global.jitter.job.
Require Import prosa.classic.implementation.global.jitter.task prosa.classic.implementation.global.jitter.job.
From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq div.

Module ConcreteArrivalSequence.

  Import JobWithJitter ArrivalSequence ConcreteTask ConcreteJob SporadicTaskset TaskArrival.

  Section PeriodicArrivals.

    Variable ts: concrete_taskset.

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

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

  End PeriodicArrivals.

  Section Proofs.

    Variable ts: concrete_taskset.
    Hypothesis H_valid_task_parameters:
      valid_sporadic_taskset task_cost task_period task_deadline ts.

    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_valid_job_parameters:
      ∀ j,
        arrives_in arr_seq j →
        valid_sporadic_job_with_jitter task_cost task_deadline task_jitter job_cost job_deadline job_task job_jitter j.

    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.

  End Proofs.

End ConcreteArrivalSequence.