Library probsa.rt.behavior.service

(* --------------------------------- ProBsa --------------------------------- *)
From probsa.rt.behavior Require Export job schedule.

(* --------------------------------- Main ----------------------------------- *)

Probabilistic Service

Section Service.

  Context {Ω} {μ : measure Ω}.
  Context {Job : JobType}
          {job_cost : JobCostRV Job Ω μ}.
  Context {PState : ProcessorState Job}.

  Variable pr_sched : pr_schedule μ PState.

  Definition pr_service (j : Job) (t : instant) : nrvar μ :=
    mkRvar μ (fun ω:Ω ⇒ service (pr_sched ω) j t).

A job j is completed by time t in a scenario ω iff job_cost j = None, or job_cost j ω ≤ pr_service j t ω.

Definition pr_completed_by (j : Job) (t : instant) : rvar μ [eqType of bool ] :=
job_cost j ⟨<=⟩ pr_service j t.

Since pr_completed_by _ _ is a random variable with a codomain in booleans, it can be viewed as a predicate on Ω. Hence, to define that a job j completes at time t, we use a notation similar to the set-theoretic -- X ∩ Y denotes a subset of Ω that satisfies both X and Y.

Definition pr_completes_at (j : Job) (t : instant) : rvar μ [eqType of bool ] :=
(!pr_completed_by j t .-1 ) ∩ (pr_completed_by j t ).

End Service.