Library probsa.rt.model.assumptions.pr_respects_policy

From prosa.model Require Export schedule.priority_driven.

From probsa.rt.behavior Require Export job arrival_sequence schedule.

Section PrRespectsPolicyAtPreemptionPoint.

  Context {Ω} {μ : measure Ω}.

  Context {Task : TaskType}
          {FP : FP_policy Task}.

  Context {Job : finType}
          {job_cost : JobCostRV Job Ω μ}
          {job_arrival : JobArrivalRV Job Ω μ}
          {job_task : JobTask Job Task}.

  Variable sched : pr_schedule μ (ideal.processor_state Job).

  Let JobReadyRV :=
    ∀ (ω : Ω),
      @JobReady
        Job (ideal.processor_state Job)
        (fun j ⇒ odflt0 (job_cost j) ω) (fun j ⇒ odflt0 (job_arrival j) ω).

  Definition pr_respects_policy_at_preemption_point
             (job_ready : JobReadyRV) (job_preemptable : JobPreemptable Job) :=
    ∀ (ω : Ω),
      @respects_policy_at_preemption_point
        _ _ _ job_preemptable (job_ready ω) (arr_seq ω) (sched ω) _.

End PrRespectsPolicyAtPreemptionPoint.