Library prosa.model.task.arrival.sporadic_as_curve

Arrival Curve for Sporadic Tasks
Any analysis that supports arbitrary arrival curves can also be used to analyze sporadic tasks. We establish this link below.
Consider any type of sporadic tasks.
  Context {Task : TaskType} `{SporadicModel Task}.

The bound on the maximum number of arrivals in a given interval max_sporadic_arrivals is in fact a valid arrival curve, which we note with the following arrival-curve declaration.
  Global Program Instance MaxArrivalsSporadic : MaxArrivals Task := max_sporadic_arrivals.

It remains to be shown that max_sporadic_arrivals satisfies all expectations placed on arrival curves. First, we observe that the bound is structurally sound.
For convenience, we lift the preceding observation to the level of entire task sets.
Next, we note that it is indeed an arrival bound. To this end, consider any type of jobs stemming from these tasks ...
  Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.

... and any well-formed arrival sequence of such jobs.
We establish the validity of the defined curve.
  Section Validity.

Let tsk denote any valid sporadic task to be analyzed.
We observe that max_sporadic_arrivals is indeed an upper bound on the maximum number of arrivals.
For convenience, we lift the preceding observation to the level of entire task sets.
We add the lemmas into the "Hint Database" basic_rt_facts so that they become available for proof automation.
Global Hint Resolve
  sporadic_arrival_curve_valid
  sporadic_task_sets_arrival_curve_valid
  sporadic_arrival_curve_respects_max_arrivals
  sporadic_task_sets_respects_max_arrivals
  : basic_rt_facts.