# Library prosa.model.task.arrival.curves

# The Arbitrary Arrival Curves Model

## Task Parameters for the Arrival Curves Model

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

Consider any type of tasks ...

... and any type of jobs associated with these tasks.

Consider any job arrival sequence.

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.

Definition valid_arrival_curve (tsk : Task) (num_arrivals : duration → nat) :=

num_arrivals 0 = 0 ∧

monotone num_arrivals leq.

num_arrivals 0 = 0 ∧

monotone num_arrivals leq.

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.

Definition respects_max_arrivals (tsk : Task) (max_arrivals : duration → nat) :=

∀ (t1 t2 : instant),

t1 ≤ t2 →

number_of_task_arrivals arr_seq tsk t1 t2 ≤ max_arrivals (t2 - t1).

∀ (t1 t2 : instant),

t1 ≤ t2 →

number_of_task_arrivals arr_seq tsk t1 t2 ≤ max_arrivals (t2 - t1).

We analogously define the lower arrival bound..

Definition respects_min_arrivals (tsk : Task) (min_arrivals : duration → nat) :=

∀ (t1 t2 : instant),

t1 ≤ t2 →

min_arrivals (t2 - t1) ≤ number_of_task_arrivals arr_seq tsk t1 t2.

End ArrivalCurves.

∀ (t1 t2 : instant),

t1 ≤ t2 →

min_arrivals (t2 - t1) ≤ number_of_task_arrivals arr_seq tsk t1 t2.

End ArrivalCurves.

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.

Definition respects_min_separation (tsk : Task) (min_separation: nat → duration) :=

∀ t1 t2,

t1 ≤ t2 →

min_separation (number_of_task_arrivals arr_seq tsk t1 t2) ≤ t2 - t1.

∀ t1 t2,

t1 ≤ t2 →

min_separation (number_of_task_arrivals arr_seq tsk t1 t2) ≤ t2 - t1.

We analogously define in upper separation bounds.

Definition respects_max_separation (tsk : Task) (max_separation: nat → duration):=

∀ t1 t2,

t1 ≤ t2 →

t2 - t1 ≤ max_separation (number_of_task_arrivals arr_seq tsk t1 t2).

End SeparationBound.

End ArrivalCurves.

∀ t1 t2,

t1 ≤ t2 →

t2 - t1 ≤ max_separation (number_of_task_arrivals arr_seq tsk t1 t2).

End SeparationBound.

End ArrivalCurves.

## Model Validity

Consider any type of tasks ...

... and any type of jobs associated with these tasks.

Consider any job arrival sequence...

..and all kinds of arrival and separation curves.

Let ts be an arbitrary task set.

We say that arrivals is a valid arrival curve for a task set
if it is valid for any task in the task set

Definition valid_taskset_arrival_curve (arrivals : Task → duration → nat) :=

∀ (tsk : Task), tsk \in ts → valid_arrival_curve tsk (arrivals tsk).

∀ (tsk : Task), tsk \in ts → valid_arrival_curve tsk (arrivals tsk).

Finally, we lift the per-task semantics of the respective arrival and
separation curves to the entire task set.

Definition taskset_respects_max_arrivals :=

∀ (tsk : Task), tsk \in ts → respects_max_arrivals arr_seq tsk (max_arrivals tsk).

Definition taskset_respects_min_arrivals :=

∀ (tsk : Task), tsk \in ts → respects_min_arrivals arr_seq tsk (min_arrivals tsk).

Definition taskset_respects_max_separation :=

∀ (tsk : Task), tsk \in ts → respects_max_separation arr_seq tsk (max_separation tsk).

Definition taskset_respects_min_separation :=

∀ (tsk : Task), tsk \in ts → respects_min_separation arr_seq tsk (min_separation tsk).

End ArrivalCurvesModel.