Library prosa.classic.implementation.apa.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.

    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.

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

  End PeriodicArrivals.

  Section Proofs.

    Context {num_cpus: nat}.

    Variable ts: concrete_taskset num_cpus.
    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 task_cost task_deadline job_cost job_deadline job_task 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.