Library probsa.rt.analysis.independent.task_workload

From probsa.rt.model Require Export events workload.

Section PrTaskWorkloadIndependence.

  Context {Ω} {μ : measure Ω}.

  Context {Task : TaskType}
          {D : TaskDeadline Task}.

  Context {Job : finType}
          {job_cost : JobCostRV Job Ω μ}
          {job_arrival : JobArrivalRV Job Ω μ}
          {job_task : JobTask Job Task}.

  Variable ts : seq Task.
  Hypothesis H_ts_uniq : uniq ts.
  Hypothesis H_jobs_from_ts : ∀ (j : Job), job_task j \in ts.

  Variable tsk : Task.
  Hypothesis H_tsk_in_ts : tsk \in ts.

  Hypothesis H_arrival_sequence_uniq : pr_arrival_sequence_uniq.
  Hypothesis H_arrivals_consistent : arr_seq_job_arrival_consistent.

  Let ξpart := partition_on_ξ μ : Ω_partition.
  Hypothesis job_costs_cond_independent :
    ∀ (ξ : I ξpart) `{!PosProb μ (ξpart ◁{ξ })},
      independent
        [seq mkRvar (restrict μ (ξpart ◁{ξ })) (job_cost j) | j <- index_enum Job].

  Variable ξ : I ξpart.
  Context {ρ : PosProb μ (ξpart ◁{ξ })}.

For a task tsk ∈ ts, let [t1 tsk, t2 tsk) denote a time interval for each task in ts ...

Variable (t1 t2 : Task → instant).

... and let pr_task_workload tsk denote the task's conditional workload (w.r.t. the arrival sequence ξ) in the interval.

  Let pr_task_workload (tsk : Task) :=
    mkRvar _ (pr_workload_of_task tsk (t1 tsk) (t2 tsk))
    : rvar (restrict μ (ξpart ◁{ξ })) [eqType of work].

Then probabilistic workloads pr_task_workload ⋅ of distinct tasks in the corresponding intervals are independent.

Lemma pr_task_workload_independence :
independent [seq pr_task_workload tsk | tsk <- ts].

End PrTaskWorkloadIndependence.