Library probsa.rt.model.abort_readiness
Consider any kind of jobs...
... and any kind of processor state.
Suppose jobs have an arrival time and a cost.
Context `{JobArrival Job} `{JobCost Job} `{JobDeadline Job}.
Global Program Instance abort_ready_instance : JobReady Job PState :=
{
job_ready sched j t := pending sched j t && (t < job_deadline j)%nat
}.
End BasicReadinessWithJobAbortion.
From probsa.rt.behavior Require Export job.
Section ProbBasicReadinessWithJobAbortion.
Context {Ω} {μ : measure Ω}.
Global Program Instance abort_ready_instance : JobReady Job PState :=
{
job_ready sched j t := pending sched j t && (t < job_deadline j)%nat
}.
End BasicReadinessWithJobAbortion.
From probsa.rt.behavior Require Export job.
Section ProbBasicReadinessWithJobAbortion.
Context {Ω} {μ : measure Ω}.
Consider any kind of jobs...
... and any kind of processor state.
Suppose jobs have an arrival time and a cost.
Context {job_arrival : JobArrivalRV Job Ω μ}
{job_cost : JobCostRV Job Ω μ}
{job_deadline : JobDeadlineRV Job Ω μ}.
Definition pr_abort_ready_instance : (∀ ω : Ω, JobReady Job PState) :=
fun (ω : Ω) ⇒
@abort_ready_instance
_ _
(sample0_arrivals ω)
(sample0_costs ω)
(sample0_deadlines ω).
End ProbBasicReadinessWithJobAbortion.
{job_cost : JobCostRV Job Ω μ}
{job_deadline : JobDeadlineRV Job Ω μ}.
Definition pr_abort_ready_instance : (∀ ω : Ω, JobReady Job PState) :=
fun (ω : Ω) ⇒
@abort_ready_instance
_ _
(sample0_arrivals ω)
(sample0_costs ω)
(sample0_deadlines ω).
End ProbBasicReadinessWithJobAbortion.