Library probsa.rt.model.assumptions.pr_must_be_ready
From probsa.rt.behavior Require Export job schedule.
Section PrMustBeReadyToExecture.
Context {Ω} {μ : measure Ω}.
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}
{job_arrival : JobArrivalRV Job Ω μ}.
Context {PState : ProcessorState Job}.
Variable sched : pr_schedule μ PState.
Section PrMustBeReadyToExecture.
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 jobs_must_be_ready_to_execute to the
probabilistic setting by requiring it to hold for every outcome ω.
Definition pr_jobs_must_be_ready_to_execute (job_ready : JobReadyRV) :=
∀ (ω : Ω),
@jobs_must_be_ready_to_execute _ _ (sched ω) _ _ (job_ready ω).
End PrMustBeReadyToExecture.
∀ (ω : Ω),
@jobs_must_be_ready_to_execute _ _ (sched ω) _ _ (job_ready ω).
End PrMustBeReadyToExecture.