# Library prosa.implementation.definitions.maximal_arrival_sequence

# A Maximal Arrival Sequence

Consider any type of tasks ...

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

Context {Job : JobType}.

Context `{JobTask Job Task}.

Context `{JobArrival Job}.

Context `{JobCost Job}.

Context `{JobTask Job Task}.

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.

Let tsk be any task.

First, we introduce a function that computes the sum of all elements in
a given list's suffix of length n.

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.

Definition jobs_remaining (arr_prefix : seq nat) :=

supremum leq [seq (max_arrivals tsk Δ.+1 - suffix_sum arr_prefix Δ) | Δ <- iota 0 (size arr_prefix).+1].

supremum leq [seq (max_arrivals tsk Δ.+1 - suffix_sum arr_prefix Δ) | Δ <- iota 0 (size arr_prefix).+1].

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

| None ⇒ max_arrivals tsk 1

| Some n ⇒ n

end.

match jobs_remaining arr_prefix with

| None ⇒ max_arrivals tsk 1

| Some n ⇒ n

end.

Next, we define a function that extends by one a given arrival prefix...

Definition extend_arrival_prefix (arr_prefix : seq nat) :=

arr_prefix ++ [:: next_max_arrival arr_prefix ].

arr_prefix ++ [:: next_max_arrival arr_prefix ].

... and a function that generates a maximal arrival prefix
of size t, starting from an empty 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.

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.

Definition concrete_arrival_sequence (ts : seq Task) (t : instant) :=

\cat_(tsk <- ts) generate_jobs_at tsk (max_arrivals_at tsk t) t.

End MaximalArrivalSequence.

\cat_(tsk <- ts) generate_jobs_at tsk (max_arrivals_at tsk t) t.

End MaximalArrivalSequence.