Library rt.restructuring.model.aggregate.task_arrivals
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.10.1 (October 2019)
----------------------------------------------------------------------------- *)
From rt.restructuring.model Require Export task.
In this file we provide basic definitions related to tasks on arrival sequences.
Consider any type of job associated with any type of tasks.
Consider any job arrival sequence.
Let tsk be any task.
We define the sequence of jobs of tsk arriving at time t.
Definition task_arrivals_at (t : instant) : seq Job :=
[seq j <- arrivals_at arr_seq t | job_task j == tsk].
[seq j <- arrivals_at arr_seq t | job_task j == tsk].
By concatenation, we construct the list of jobs of tsk that arrived in the
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 tsk that arrived up to time t, ...
...and the list of jobs of tsk that arrived 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 Definitions.
size (task_arrivals_between t1 t2).
End Definitions.
We define a predicate for arrival sequences for which jobs come from a taskset.
Definition arrivals_come_from_taskset (ts : seq Task) :=
∀ j, arrives_in arr_seq j → job_task j \in ts.
End TaskArrivals.
∀ j, arrives_in arr_seq j → job_task j \in ts.
End TaskArrivals.