Library rt.restructuring.model.aggregate.task_arrivals
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 task 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].
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
arrived up to time t, ...
...and the list of jobs of task 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 in which all jobs
come from a given task set.
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.