Library probsa.rt.model.assumptions.pr_cost

From probsa.rt.model Require Export pRBF events.
From probsa.rt.analysis Require Export nth_cost.

Section PrCostAssumptions.

  Context {Ω} {μ : measure Ω}.

  Context {Task : TaskType}
          {pWCET_pmf : ProbWCET Task}.

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

We say that job costs are independent iff the costs of all jobs form a jointly independent collection of random variables.
  Definition job_costs_independent :=
    independent [seq job_cost j | j <- index_enum Job].

We say that job costs are bounded by pWCET iff the cost of any job of any task tsk is stochastically dominated by the pWCET of that task.
  Definition job_costs_bounded_by_pWCET :=
    ∀ (tsk : Task) (i : nat),
      nth_cost tsk i ⪯ to_distrib pWCET_pmf tsk.

We say that job costs are identically distributed iff jobs of the same task have identically distributed costs.
  Definition job_costs_identically_distributed :=
    ∀ j1 j2,
      job_task j1 = job_task j2 →
      odflt0 (job_cost j1) ⪯ odflt0 (job_cost j2).

We say that job costs are conditionally independent iff job costs remain jointly independent when conditioned on a fixed arrival sequence ξ. This means that knowing the arrival pattern doesn't introduce dependencies between the execution times of different jobs.
  Definition job_costs_independent_cond_arr_seq :=
    let ξpart := partition_on_ξ μ : Ω_partition in
    ∀ (ξ : I ξpart) `(!PosProb μ (ξpart◁{ξ})),
      independent [seq mkRvar (restrict μ (ξpart◁{ξ})) (job_cost j) | j <- index_enum Job].

We say that job costs are independent of the probabilistic arrival sequence iff for any fixed arrival pattern ξ, the random variable yielding the sequence of job costs [seq job_cost j ω | j <- jobs] is independent of the indicator random variable for whether the arrival sequence equals ξ (i.e., ξpart◁{ξ} ω, which is true when ω has arrival pattern ξ, false otherwise). That is, knowing which arrival pattern occurred doesn't tell us anything about the job costs, and vice versa.
  Definition job_costs_independent_of_arrival_sequence :=
    let ξpart := partition_on_ξ μ : Ω_partition in
    ∀ (ξ : I ξpart) `(!PosProb μ (ξpart◁{ξ})) (jobs : seq Job),
      indep2
        (mkRvar μ (fun ω ⇒ [seq job_cost j ω | j <- jobs]))
        (mkRvar μ (fun ω ⇒ ξpart◁{ξ} ω)).

We say that conditional job costs are bounded by pWCET iff the conditional cost of any job (given a fixed arrival sequence ξ) is stochastically dominated by the task's pWCET distribution. This is the conditioned version of job_costs_bounded_by_pWCET, ensuring the bound holds regardless of which arrival pattern occurs.
  Definition conditional_cost_bounded_by_pWCET :=
    ∀ (j : Job) (tsk : Task),
      job_of_task tsk j →
      let ξpart := partition_on_ξ μ : Ω_partition in
      ∀ (ξ : I ξpart) `(!PosProb μ (ξpart◁{ξ})),
        mkRvar (restrict μ (ξpart◁{ξ})) [eta odflt0 (job_cost j)] ⪯ to_distrib pWCET_pmf tsk.

End PrCostAssumptions.