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.
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].
... and also count the number of job arrivals.
Definition number_of_task_arrivals (t1 t2 : instant) :=
size (task_arrivals_between t1 t2).
End TaskArrivals.
size (task_arrivals_between t1 t2).
End TaskArrivals.