Library prosa.model.task.arrival.task_max_inter_arrival
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.model.task.concept.
Require Export prosa.model.task.arrivals.
Task Max Inter-Arrival
In the following section, we define two properties that a task must satisfy
for its maximum inter-arrival time to be valid.
Consider any type of tasks, ...
... any type of jobs associated with the tasks, ...
... and any arrival sequence.
Firstly, the task maximum inter-arrival time for a task is positive.
Definition positive_task_max_inter_arrival_time (tsk : Task) :=
task_max_inter_arrival_time tsk > 0.
task_max_inter_arrival_time tsk > 0.
Secondly, for any job [j] (with a positive [job_index]) of a task [tsk],
there exists a job [j'] of task [tsk] that arrives before [j]
with [j] not arriving any later than the task maximum inter-arrival
time of [tsk] after [j'].
Definition arr_sep_task_max_inter_arrival (tsk : Task) :=
∀ (j : Job),
arrives_in arr_seq j →
job_task j = tsk →
job_index arr_seq j > 0 →
∃ (j' : Job),
j ≠ j' ∧
arrives_in arr_seq j' ∧
job_task j' = tsk ∧
job_arrival j' ≤ job_arrival j ≤ job_arrival j' + task_max_inter_arrival_time tsk.
∀ (j : Job),
arrives_in arr_seq j →
job_task j = tsk →
job_index arr_seq j > 0 →
∃ (j' : Job),
j ≠ j' ∧
arrives_in arr_seq j' ∧
job_task j' = tsk ∧
job_arrival j' ≤ job_arrival j ≤ job_arrival j' + task_max_inter_arrival_time tsk.
Finally, we say that the maximum inter-arrival time of a task [tsk] is
valid iff it satisfies the above two properties.
Definition valid_task_max_inter_arrival_time (tsk: Task) :=
positive_task_max_inter_arrival_time tsk ∧
arr_sep_task_max_inter_arrival tsk.
positive_task_max_inter_arrival_time tsk ∧
arr_sep_task_max_inter_arrival tsk.
A task set is said to respect the task max inter-arrival model iff all tasks
in the task set have valid task max inter-arrival times as defined above.
Definition taskset_respects_task_max_inter_arrival_model (ts : TaskSet Task) :=
∀ tsk,
tsk \in ts →
valid_task_max_inter_arrival_time tsk.
End ValidTaskMaxInterArrival.
∀ tsk,
tsk \in ts →
valid_task_max_inter_arrival_time tsk.
End ValidTaskMaxInterArrival.