Library prosa.classic.implementation.apa.arrival_sequence

(* We can reuse the.apa definition of periodic arrival sequence. *)
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.arrival_sequence prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.implementation.apa.task prosa.classic.implementation.apa.job.
From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq div.

Module ConcreteArrivalSequence.

  Import Job ArrivalSequence ConcreteTask ConcreteJob SporadicTaskset TaskArrival.

  Section PeriodicArrivals.

    Context {num_cpus: nat}.
    Variable ts: concrete_taskset num_cpus.

    (* At any time t, we release Some job of tsk if t is a multiple of the period,
       otherwise we release None. *)
    Definition add_job (arr: time) (tsk: @concrete_task num_cpus) : option (@concrete_job _) :=
      if task_period tsk %| arr then
        Some (Build_concrete_job (arr %/ task_period tsk) arr (task_cost tsk) (task_deadline tsk) tsk)
      else
        None.

    (* The arrival sequence at any time t is simply the partial map of add_job. *)
    Definition periodic_arrival_sequence (t: time) := pmap (add_job t) ts.

  End PeriodicArrivals.

  Section Proofs.

    Context {num_cpus: nat}.

    (* Let ts be any concrete task set with valid parameters. *)
    Variable ts: concrete_taskset num_cpus.
    Hypothesis H_valid_task_parameters:
      valid_sporadic_taskset task_cost task_period task_deadline ts.

    (* Regarding the periodic arrival sequence built from ts, we prove that...*)
    Let arr_seq := periodic_arrival_sequence ts.

    (* ... arrival times are consistent, ... *)
    Theorem periodic_arrivals_are_consistent:
      arrival_times_are_consistent job_arrival arr_seq.

    (* ... every job comes from the task set, ... *)
    Theorem periodic_arrivals_all_jobs_from_taskset:
      ∀ j,
        arrives_in arr_seq j →
        job_task j \in ts.

    (* ..., jobs have valid parameters, ... *)
    Theorem periodic_arrivals_valid_job_parameters:
      ∀ j,
        arrives_in arr_seq j →
        valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.

    (* ... job arrivals satisfy the sporadic task model, ... *)
    Theorem periodic_arrivals_are_sporadic:
      sporadic_task_model task_period job_arrival job_task arr_seq.

    (* ... and the arrival sequence has no duplicate jobs. *)
    Theorem periodic_arrivals_is_a_set:
      arrival_sequence_is_a_set arr_seq.

  End Proofs.

End ConcreteArrivalSequence.