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.
\sum_(j <- task_arrivals_between t1 t2) job_cost j.
In the following, suppose there is a deadline associated with each job.
We define the list of jobs of task tsk that arrive in
a given half-open interval
[t1, t2) and that also have a deadline
within the closed interval [t1, t2], ...
Definition task_arrivals_with_deadline_within (t1 t2 : instant) :=
[seq j <- arrivals_between arr_seq t1 t2 | job_of_task tsk j & job_deadline j ≤ t2].
[seq j <- arrivals_between arr_seq t1 t2 | job_of_task tsk j & job_deadline j ≤ t2].
... and similarly define the count of such jobs.
Definition number_of_task_arrivals_with_deadline_within (t1 t2 : instant) :=
size (task_arrivals_with_deadline_within t1 t2).
End TaskArrivals.
size (task_arrivals_with_deadline_within t1 t2).
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.