Library rt.restructuring.model.schedule.priority_based.preemptive

From rt.restructuring.behavior Require Export schedule ready arrival_sequence.
From rt.restructuring.model Require Export priorities.

(* We now define what it means for a schedule to respect a priority *)
(* We only define it for a JLDP policy since the definitions for JLDP and JLFP are the same
   and can be used through the conversions *)
Section Priority.
  Context {Job: JobType} {Task: TaskType}.
  Context `{JobCost Job} `{JobArrival Job}.

  Context `{JLDP_policy Job}.

  Variable arr_seq : arrival_sequence Job.

  Context {PState : Type}.
  Context `{ProcessorState Job PState}.

  Context `{JobReady PState Job}.

  Variable sched : schedule PState.

  Definition respects_preemptive_priorities :=
    ∀ j j_hp t,
      arrives_in arr_seq j →
      backlogged sched j t →
      scheduled_at sched j_hp t →
      hep_job_at t j_hp j.
End Priority.