PMF of pWCET

In this file, we define pWCET's probability mass function. The typeclass contains three elements: (1) a function called pWCET_pmf that takes a Task and a work as input and returns a value in R that is supposed to denote the "probability" of a task to take a certain value, (2) a proof term that pWCET_pmf is non negative for any task and any work value, and (3) a proof term that pWCET_pmf sums up to 1. It is important to note that even though R represents the set of real numbers, in the context of probability theory, probabilities are always represented by values between 0 and 1. Therefore, the pWCET_pmf function actually returns a value within the closed interval [0,1], representing the probability of a given Task completing after consuming work time units of processor service.

CDF of pWCET

Next, we define a more common form of pWCET as a CDF. Note that since pWCET_pmf is not an actual random variable, we cannot re-use the existing definition of CDF. Hence, we simply define pWCET_cdf tsk w0 as a sum of pWCET_pmf tsk w of all w ≤ w0.