# Library prosa.model.task.arrivals

In this module, we provide basic definitions concerning the job
arrivals of a given task.

Consider any type of job associated with any type of tasks.

Context {Job : JobType}.

Context {Task : TaskType}.

Context `{JobTask Job Task}.

Context `{JobArrival Job}.

Context `{JobCost Job}.

Context {Task : TaskType}.

Context `{JobTask Job Task}.

Context `{JobArrival Job}.

Context `{JobCost Job}.

Consider any job arrival sequence ...

... and any task.

First, we construct the list of jobs of task tsk that arrive
in a given half-open interval

`[t1, t2)`

.
Definition task_arrivals_between (t1 t2 : instant) :=

[seq j <- arrivals_between arr_seq t1 t2 | job_of_task tsk j].

[seq j <- arrivals_between arr_seq t1 t2 | job_of_task tsk j].

Definition task_arrivals_at (tsk : Task) (t : instant) :=

[seq j <- arrivals_at arr_seq t | job_of_task tsk j].

[seq j <- arrivals_at arr_seq t | job_of_task tsk j].

... and finally count the number of job arrivals.

... and also count the cost of job arrivals.

Definition cost_of_task_arrivals (t1 t2 : instant) :=

\sum_(j <- task_arrivals_between t1 t2) job_cost j.

End TaskArrivals.

\sum_(j <- task_arrivals_between t1 t2) job_cost j.

End TaskArrivals.

In this section we introduce a few definitions
regarding arrivals of a particular task prior to a job.

Consider any type of jobs associated with any type of tasks.

Context {Job : JobType}.

Context {Task : TaskType}.

Context `{JobTask Job Task}.

Context `{JobArrival Job}.

Context {Task : TaskType}.

Context `{JobTask Job Task}.

Context `{JobArrival Job}.

Consider any arrival sequence of jobs ...

... and any job j.

We first define a sequence of jobs of a task
that arrive before or at job_arrival j.

Definition task_arrivals_up_to_job_arrival :=

task_arrivals_up_to arr_seq (job_task j) (job_arrival j).

task_arrivals_up_to arr_seq (job_task j) (job_arrival j).

Next, we define a sequence of jobs of a task
that arrive strictly before job_arrival j.

Definition task_arrivals_before_job_arrival :=

task_arrivals_before arr_seq (job_task j) (job_arrival j).

task_arrivals_before arr_seq (job_task j) (job_arrival j).

Finally, we define a sequence of jobs of a task
that arrive at job_arrival j.

Definition task_arrivals_at_job_arrival :=

task_arrivals_at arr_seq (job_task j) (job_arrival j).

End PriorArrivals.

task_arrivals_at arr_seq (job_task j) (job_arrival j).

End PriorArrivals.

In this section, we define the notion of a job's index.

Consider any type of tasks, ...

... any type of jobs associated with the tasks, ...

... and any arrival sequence.

Given a job j, we define a concept of job index as the number
of jobs of the same task as j that arrived before or at the
same instant as j. Please note that job indices start from zero.

Definition job_index (j : Job) :=

index j (task_arrivals_up_to_job_arrival arr_seq j).

End JobIndex.

index j (task_arrivals_up_to_job_arrival arr_seq j).

End JobIndex.

In this section we define the notion of a previous job
for any job with a positive job_index.

Consider any type of jobs associated with any type of tasks.

Context {Job : JobType}.

Context {Task : TaskType}.

Context `{JobTask Job Task}.

Context `{JobArrival Job}.

Context {Task : TaskType}.

Context `{JobTask Job Task}.

Context `{JobArrival Job}.

Consider any job arrival sequence.

Variable arr_seq : arrival_sequence Job.

Let task_arrivals_up_to_job_arrival j := task_arrivals_up_to_job_arrival arr_seq j.

Let prev_index j := job_index arr_seq j - 1.

Let task_arrivals_up_to_job_arrival j := task_arrivals_up_to_job_arrival arr_seq j.

Let prev_index j := job_index arr_seq j - 1.

Definition prev_job (j : Job) := nth j (task_arrivals_up_to_job_arrival j) (prev_index j).

End PreviousJob.

End PreviousJob.