Busy window concept
@sbozhko @mlesourd @bbb @xiaojie @fradet
We need a notion of busy interval for our first shot at CPA with FPP scheduling. There are two options (both exist in different parts of the library) for this, depending on whether one considers intervals of size 1 with no activation in them as busy intervals or not. The "usual definition" does not explicitly excludes this case, so was there a strong reason to add this condition? Note that using one definition or the other would imply adjusting proofs, but the changes do not appear to be huge.
A second comment on the definition of busy interval: it is introduced for JLFP, so at the job level, but the "usual definition" is for tasks. Our plan is to have a definition at the task level first, and then add the definition at the job level later. Regarding proofs, we believe that they should be factorizable by relying on structural properties of busy intervals.
Questions? Comments?