Library probsa.rt.behavior.job
(* --------------------------------- Prosa ---------------------------------- *)
From prosa.behavior Require Export job.
(* --------------------------------- ProBsa --------------------------------- *)
From probsa.probability Require Export nrvar.
(* ---------------------------------- Main ---------------------------------- *)
From prosa.behavior Require Export job.
(* --------------------------------- ProBsa --------------------------------- *)
From probsa.probability Require Export nrvar.
(* ---------------------------------- Main ---------------------------------- *)
Probabilistic Parameters of a Job
Definition of a generic type of parameter relating jobs to a probabilistic (discrete) cost. Note that if a job j does not arrive in a scenario ω : Ω, then job_cost j ω = None.
Class JobCostRV (Job : JobType) (Ω : countType) (μ : measure Ω) :=
job_cost : Job → rvar μ [eqType of option instant].
job_cost : Job → rvar μ [eqType of option instant].
Definition of a generic type of parameter relating jobs to a
probabilistic arrival time. Note that if a job j does not arrive
in a scenario ω : Ω, then job_arrival j ω = None.
Class JobArrivalRV (Job : JobType) (Ω : countType) (μ : measure Ω) :=
job_arrival : Job → rvar μ [eqType of option instant].
job_arrival : Job → rvar μ [eqType of option instant].
Definition of a generic type of parameter relating jobs to a
probabilistic deadline. Note that if a job j does not arrive
in a scenario ω : Ω, then job_deadline j ω = None.
Class JobDeadlineRV (Job : JobType) (Ω : countType) (μ : measure Ω) :=
job_deadline : Job → rvar μ [eqType of option instant].
job_deadline : Job → rvar μ [eqType of option instant].
Section DerivedNotions.
Context {Ω} {μ : measure Ω}.
Context {Job : JobType}
{job_arrival : JobArrivalRV Job Ω μ}
{job_cost : JobCostRV Job Ω μ}.
Context {Ω} {μ : measure Ω}.
Context {Job : JobType}
{job_arrival : JobArrivalRV Job Ω μ}
{job_cost : JobCostRV Job Ω μ}.
Function compute_arrivals maps an evolution ω to a
deterministic function that maps jobs to their arrival times (or
None, if a job does not arrive in ω).
Similarly, we define function compute_costs that maps an
evolution ω to a deterministic function that maps jobs to
their costs (or None, if a job does not arrive in ω).