Library rt.restructuring.model.arrival.sporadic

From rt.restructuring.behavior Require Export arrival_sequence.
From rt.restructuring.model Require Export task.

Section TaskMinInterArrivalTime.
  Context {Task : TaskType}.

  Variable (task_min_inter_arrival_time : duration).

  Definition valid_task_min_inter_arrival_time :=
    task_min_inter_arrival_time > 0.

  Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.

  Variable arr_seq : arrival_sequence Job.

  Definition respects_sporadic_task_model (tsk : Task) (d : duration) :=
    ∀ (j j': Job),
      j ≠ j' → (* Given two different jobs j and j' ... *)
      arrives_in arr_seq j → (* ...that belong to the arrival sequence... *)
      arrives_in arr_seq j' →
      job_task j = tsk →
      job_task j' = tsk → (* ... and that are spawned by the same task, ... *)
      job_arrival j ≤ job_arrival j' → (* ... if the arrival of j precedes the arrival of j' ...,  *)
      (* then the arrival of j and the arrival of j' are separated by at least one period. *)
      job_arrival j' ≥ job_arrival j + d.

End TaskMinInterArrivalTime.

(* Definition of a generic type of parameter for task
   minimum inter arrival times *)

Class SporadicModel (Task : TaskType) :=
  task_min_inter_arrival_time : Task → duration.

Section SporadicModel.
  Context {Task : TaskType} `{SporadicModel Task}.

  Variable ts : seq Task.

  Definition valid_taskset_min_inter_arrival_times :=
    ∀ tsk : Task,
      tsk \in ts →
      task_min_inter_arrival_time tsk > 0.

  Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.

  Variable arr_seq : arrival_sequence Job.

  (* Then, we define the sporadic task model as follows.*)
  Definition taskset_respects_sporadic_task_model :=
    ∀ tsk,
      tsk \in ts →
      respects_sporadic_task_model arr_seq tsk (task_min_inter_arrival_time tsk).

End SporadicModel.