# Library prosa.implementation.definitions.maximal_arrival_sequence

Require Export prosa.util.supremum.

# A Maximal Arrival Sequence

In this section, we propose a concrete instantiation of an arrival sequence. Given an arbitrary arrival curve, the defined arrival sequence tries to generate as many jobs as possible at any time instant by adopting a greedy strategy: at each time t, the arrival sequence contains the maximum possible number of jobs that does not violate the given arrival curve's constraints.
Consider any type of tasks ...

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

Let max_arrivals denote any function that takes a task and an interval length and returns the associated number of job arrivals of the task.

In this section, we define a procedure that computes the maximal number of jobs that can be released at a given instant without violating the corresponding arrival curve.
Section NumberOfJobs.

First, we introduce a function that computes the sum of all elements in a given list's suffix of length n.
Definition suffix_sum xs n := \sum_(size xs - n t < size xs) nth 0 xs t.

Let the arrival prefix arr_prefix be a sequence of natural numbers, where nth xs t denotes the number of jobs that arrive at time t. Then, given an arrival curve max_arrivals and an arrival prefix arr_prefix, we define a function that computes the number of jobs that can be additionally released without violating the arrival curve.
The high-level idea is as follows. Let us assume that the length of the arrival prefix is Δ. To preserve the sub-additive property, one needs to go through all suffixes of the arrival prefix and pick the minimum.
Further, we define the function next_max_arrival to handle a special case: when the arrival prefix is empty, the function returns the value of the arrival curve with a window length of 1. Otherwise, it returns the number the number of jobs that can additionally be generated.
Definition next_max_arrival (arr_prefix : seq nat) :=
match jobs_remaining arr_prefix with
| Nonemax_arrivals tsk 1
| Some nn
end.

Next, we define a function that extends by one a given arrival prefix...
... and a function that generates a maximal arrival prefix of size t, starting from an empty arrival prefix.
Definition maximal_arrival_prefix (t : nat) :=
iter t.+1 extend_arrival_prefix [::].

Finally, we define a function that returns the maximal number of jobs that can be released at time t; this definition assumes that at each time instant prior to time t the maximal number of jobs were released.
Definition max_arrivals_at t := nth 0 (maximal_arrival_prefix t) t.

End NumberOfJobs.

Consider a function that generates n concrete jobs of the given task at the given time instant.
The maximal arrival sequence of task set ts at time t is a concatenation of sequences of generated jobs for each task.