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.
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], ...
...and the list of jobs of task [tsk] that arrive strictly
before time [t], ...
... 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.