Library probsa.rt.behavior.job

From prosa.behavior Require Export job.

From probsa.probability Require Export nrvar.

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].

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].

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].

Derived Notions

In this section, we define a few notions based on job parameters.
Section DerivedNotions.

  Context {Ω} {μ : measure Ω}.

  Context {Job : JobType}
          {job_arrival : JobArrivalRV Job Ω μ}
          {job_cost : JobCostRV Job Ω μ}
          {job_deadline : JobDeadlineRV Job Ω μ}.

Function sample_arrivals maps an evolution ω to a deterministic function that maps jobs to their arrival times (or None, if a job does not arrive in ω).
  Definition sample_arrivals (ω : Ω) : Job → option instant :=
    fun j ⇒ job_arrival j ω.

Similarly, we define the function sample_costs that maps an evolution ω to a deterministic function that maps jobs to their costs (or None, if a job does not arrive in ω).
  Definition sample_costs (ω : Ω) : Job → option work :=
    fun j ⇒ job_cost j ω.

Similarly, we define the function sample_deadlines that maps an evolution ω to a deterministic function that maps jobs to their deadlines (or None, if a job does not arrive in ω).
  Definition sample_deadlines (ω : Ω) : Job → option instant :=
    fun j ⇒ job_deadline j ω.

For contexts requiring concrete values rather than options, we provide sample0_arrivals, sample0_costs and sample0_deadlines, which default to 0 when a job does not arrive in the given evolution.
  Definition sample0_arrivals (ω : Ω) : Job → instant :=
    fun j ⇒ odflt 0%nat (job_arrival j ω).

  Definition sample0_costs (ω : Ω) : Job → work :=
    fun j ⇒ odflt 0%nat (job_cost j ω).

  Definition sample0_deadlines (ω : Ω) : Job → instant :=
    fun j ⇒ odflt 0%nat (job_deadline j ω).

End DerivedNotions.