Require Export prosa.util.rel.

# The Arbitrary Arrival Curves Model

In the following, we define the notion of arbitrary arrival curves, which can be used to reason about the frequency of job arrivals. In contrast to the sporadic task model, the arbitrary arrival curves model is well-suited to expressing bursty and irregular arrival processes.

## Task Parameters for the Arrival Curves Model

The arrival curves model describes tasks by giving an upper bound and, optionally, a lower bound on the number of new job arrivals during any given interval. These bounds are typically called arrival curves.
We let max_arrivals tsk Δ denote a bound on the maximum number of arrivals of jobs of task tsk in any interval of length Δ.
Conversely, we let min_arrivals tsk Δ denote a bound on the minimum number of arrivals of jobs of task tsk in any interval of length Δ.
Alternatively, it is also possible to describe arbitrary arrival processes by specifying the minimum and maximum lengths of an interval in which a given number of jobs arrive. Such bounds are typically called minimum- and maximum-distance functions.
We let min_separation tsk N denote the minimal length of an interval in which exactly N jobs of task tsk arrive.
Conversely, we let max_separation tsk N denote the maximal length of an interval in which exactly N jobs of task tsk arrive.

## Parameter Semantics

In the following, we precisely define the semantics of the arrival curves model.
Section ArrivalCurves.

Consider any type of tasks ...

... and any type of jobs associated with these tasks.
Context {Job : JobType}.

Consider any job arrival sequence.
Variable arr_seq : arrival_sequence Job.

### Definition of Arrival Curves

First, what constitutes a valid arrival bound for a task?
Section ArrivalCurves.

We say that a given curve num_arrivals is a valid arrival curve for task tsk iff num_arrivals is a monotonic function that equals 0 for the empty interval delta = 0.
We say that max_arrivals is an upper arrival bound for task tsk iff, for any interval `[t1, t2)`, max_arrivals (t2 - t1) bounds the number of jobs of tsk that arrive in that interval.
We analogously define the lower arrival bound..

### Definition of Minimum Distance Bounds

Next, we define the semantics of minimum-distance bounds.
Section SeparationBound.

We say that a given function min_separation is a lower separation bound iff, for any number of jobs of task tsk, min_separation lower-bounds the minimum interval length in which that many jobs can arrive.
We analogously define in upper separation bounds.

## Model Validity

Based on the just-established semantics, we define the properties of a valid arrival curves model.
Consider any type of tasks ...

... and any type of jobs associated with these tasks.
Context {Job : JobType}.

Consider any job arrival sequence...
Variable arr_seq : arrival_sequence Job.

..and all kinds of arrival and separation curves.