Library probsa.rt.model.pRBF

From prosa.model Require Import task.arrival.curves.

From probsa.probability Require Export pmf.


Section ProbRBF.

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

  Definition to_distrib (pWCET : ProbWCET Task) : Task → distrib [countType of nat] :=
    fun tsk ⇒
      match pWCET with
      | Build_ProbWCET pmf pos sum1 ⇒
          mkDistrib [countType of work] (pmf tsk) (pos tsk) (sum1 tsk)
      end.

  Definition pRBF (tsk : Task) (Δ : duration) : distrib [countType of work] :=
    ⨁_{i < α tsk Δ} to_distrib pWCET_pmf tsk.

End ProbRBF.