Library probsa.rt.model.assumptions.pr_work_conserving
From prosa.model Require Export schedule.work_conserving.
From probsa.rt.behavior Require Export job schedule arrival_sequence.
Section PrWorkConservation.
Context {Ω} {μ : measure Ω}.
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}
{job_arrival : JobArrivalRV Job Ω μ}.
Context {PState : ProcessorState Job}.
Variable sched : pr_schedule μ PState.
From probsa.rt.behavior Require Export job schedule arrival_sequence.
Section PrWorkConservation.
Context {Ω} {μ : measure Ω}.
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}
{job_arrival : JobArrivalRV Job Ω μ}.
Context {PState : ProcessorState Job}.
Variable sched : pr_schedule μ PState.
A probabilistic job readiness model is a family of (deterministic)
readiness models indexed by outcomes ω : Ω. For each outcome, we
instantiate the job cost and arrival time by evaluating the corresponding
random variables and defaulting to 0 if undefined (via odflt0). Since
job costs and arrivals are random variables with codomain option nat, we
use odflt0 to extract concrete values, treating None as 0.
Let JobReadyRV :=
∀ (ω : Ω),
JobReady
Job PState
(jc := sample0_costs ω)
(ja := sample0_arrivals ω).
∀ (ω : Ω),
JobReady
Job PState
(jc := sample0_costs ω)
(ja := sample0_arrivals ω).
We lift the deterministic property work_conserving to the probabilistic
setting by requiring it to hold for every outcome ω.
Definition pr_work_conserving (job_ready : JobReadyRV) :=
∀ ω, @work_conserving Job _ _ _ (job_ready ω) (arr_seq ω) (sched ω).
End PrWorkConservation.
∀ ω, @work_conserving Job _ _ _ (job_ready ω) (arr_seq ω) (sched ω).
End PrWorkConservation.