Library probsa.rt.analysis.completion

(* --------------------------------- Prosa ---------------------------------- *)
From prosa Require Export analysis.facts.behavior.completion.

(* --------------------------------- ProBsa --------------------------------- *)
From probsa.rt.behavior Require Export job schedule service.

(* ---------------------------------- Main ---------------------------------- *)

Probabilistic Completion is Monotone

Section CompletionLemmas.

Consider a probability space (Ω, μ), ...

Context {Ω} {μ : measure Ω}.

... and any type of jobs. Assume that the jobs have probabilistic costs defined by job_cost.

Context {Job : JobType}
{job_cost : JobCostRV Job Ω μ}.

Consider any schedule sched.

  Context {PState : ProcessorState Job}.
  Variable sched : pr_schedule μ PState.

  Lemma completion_monotone :
    ∀ (j : Job) (t1 t2 : instant) (ω : Ω ),
      (t1 ≤ t2)%nat →
      pr_completed_by sched j t1 ω →
      pr_completed_by sched j t2 ω.

Given two time instants t1 and t2 such that t1 ≤ t2, we show that the probability that a job j is completed by t1 is smaller than or equal to the probability that the same job j is completed by time t2.

  Lemma completion_monotone_prob :
    ∀ (j : Job) (t1 t2 : instant),
      (t1 ≤ t2)%nat →
      ℙ <μ >{[pr_completed_by sched j t1 ]} ≤ ℙ <μ >{[pr_completed_by sched j t2 ]}.

End CompletionLemmas.