Library prosa.model.task.arrivals
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.model.task.concept.
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_task j == tsk].
[seq j <- arrivals_between arr_seq t1 t2 | job_task j == tsk].
Based on that, we define the list of jobs of task [tsk] that
arrive up to and including time [t], ...
... the list of jobs of task [tsk] that arrive strictly
before time [t], ...
... the list of jobs of task [tsk] that arrive exactly at an instant [t], ...
Definition task_arrivals_at (tsk : Task) (t : instant) :=
[seq j <- arrivals_at arr_seq t | job_task j == tsk].
[seq j <- arrivals_at arr_seq t | job_task j == tsk].
... 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.
For any job [j] with a positive [job_index] we define the notion
of a previous job.
Definition prev_job (j : Job) := nth j (task_arrivals_up_to_job_arrival j) (prev_index j).
End PreviousJob.
End PreviousJob.