Library prosa.classic.model.arrival.basic.task_arrival
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.arrival_sequence prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path bigop.
Module TaskArrival.
Import ArrivalSequence SporadicTaskset.
Section ArrivalModels.
Context {Task: eqType}.
Variable task_period: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_task: Job → Task.
Variable arr_seq: arrival_sequence Job.
Definition sporadic_task_model :=
∀ (j j': Job),
j ≠ j' →
arrives_in arr_seq j →
arrives_in arr_seq j' →
job_task j = job_task j' →
job_arrival j ≤ job_arrival j' →
job_arrival j' ≥ job_arrival j + task_period (job_task j).
End ArrivalModels.
Section NumberOfArrivals.
Context {Task: eqType}.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_task: Job → Task.
Variable arr_seq: arrival_sequence Job.
Let arrivals_between := jobs_arrived_between arr_seq.
Variable tsk: Task.
Definition is_job_of_task (j: Job) := job_task j == tsk.
Definition arrivals_of_task_between (t1 t2: time) :=
[seq j <- arrivals_between t1 t2 | is_job_of_task j].
Definition arrivals_of_task_before (t: time) :=
arrivals_of_task_between 0 t.
Definition num_arrivals_of_task (t1 t2: time) :=
size (arrivals_of_task_between t1 t2).
Section Lemmas.
Lemma num_arrivals_of_task_cat:
∀ t t1 t2,
t1 ≤ t ≤ t2 →
num_arrivals_of_task t1 t2 = num_arrivals_of_task t1 t + num_arrivals_of_task t t2.
End Lemmas.
End NumberOfArrivals.
Section DistanceBetweenSporadicJobs.
Context {Task: eqType}.
Variable task_period: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_task: Job → Task.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_consistent_arrivals: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_no_duplicate_arrivals: arrival_sequence_is_a_set arr_seq.
Hypothesis H_sporadic_jobs:
sporadic_task_model task_period job_arrival job_task arr_seq.
Variable tsk: Task.
Variable t1 t2: time.
Let arriving_jobs := arrivals_of_task_between job_task arr_seq tsk t1 t2.
Let num_arrivals := num_arrivals_of_task job_task arr_seq tsk t1 t2.
Let by_arrival_time (j j': Job) := job_arrival j ≤ job_arrival j'.
Let sorted_jobs := sort by_arrival_time arriving_jobs.
Variable elem: Job.
Let nth_job := nth elem sorted_jobs.
Remark sorted_arrivals_properties_of_nth:
∀ idx,
idx < num_arrivals →
t1 ≤ job_arrival (nth_job idx) < t2 ∧
job_task (nth_job idx) = tsk ∧
arrives_in arr_seq (nth_job idx).
Lemma sorted_arrivals_current_differs_from_next:
∀ idx,
idx < num_arrivals.-1 →
nth_job idx ≠ nth_job idx.+1.
Lemma sorted_arrivals_separated_by_period:
∀ idx,
idx < num_arrivals.-1 →
job_arrival (nth_job idx.+1) ≥ job_arrival (nth_job idx) + task_period tsk.
Section FirstAndLastJobs.
Hypothesis H_at_least_one_job:
num_arrivals ≥ 1.
Let j_first := nth_job 0.
Let j_last := nth_job (num_arrivals.-1).
Let a_first := job_arrival j_first.
Let a_last := job_arrival j_last.
Lemma sorted_arrivals_distance_from_first_job:
∀ idx,
idx < num_arrivals →
job_arrival (nth_job idx) ≥ a_first + idx × task_period tsk.
Corollary sorted_arrivals_distance_between_first_and_last:
a_last ≥ a_first + (num_arrivals-1) × task_period tsk.
End FirstAndLastJobs.
End DistanceBetweenSporadicJobs.
End TaskArrival.
Require Import prosa.classic.model.arrival.basic.arrival_sequence prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path bigop.
Module TaskArrival.
Import ArrivalSequence SporadicTaskset.
Section ArrivalModels.
Context {Task: eqType}.
Variable task_period: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_task: Job → Task.
Variable arr_seq: arrival_sequence Job.
Definition sporadic_task_model :=
∀ (j j': Job),
j ≠ j' →
arrives_in arr_seq j →
arrives_in arr_seq j' →
job_task j = job_task j' →
job_arrival j ≤ job_arrival j' →
job_arrival j' ≥ job_arrival j + task_period (job_task j).
End ArrivalModels.
Section NumberOfArrivals.
Context {Task: eqType}.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_task: Job → Task.
Variable arr_seq: arrival_sequence Job.
Let arrivals_between := jobs_arrived_between arr_seq.
Variable tsk: Task.
Definition is_job_of_task (j: Job) := job_task j == tsk.
Definition arrivals_of_task_between (t1 t2: time) :=
[seq j <- arrivals_between t1 t2 | is_job_of_task j].
Definition arrivals_of_task_before (t: time) :=
arrivals_of_task_between 0 t.
Definition num_arrivals_of_task (t1 t2: time) :=
size (arrivals_of_task_between t1 t2).
Section Lemmas.
Lemma num_arrivals_of_task_cat:
∀ t t1 t2,
t1 ≤ t ≤ t2 →
num_arrivals_of_task t1 t2 = num_arrivals_of_task t1 t + num_arrivals_of_task t t2.
End Lemmas.
End NumberOfArrivals.
Section DistanceBetweenSporadicJobs.
Context {Task: eqType}.
Variable task_period: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_task: Job → Task.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_consistent_arrivals: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_no_duplicate_arrivals: arrival_sequence_is_a_set arr_seq.
Hypothesis H_sporadic_jobs:
sporadic_task_model task_period job_arrival job_task arr_seq.
Variable tsk: Task.
Variable t1 t2: time.
Let arriving_jobs := arrivals_of_task_between job_task arr_seq tsk t1 t2.
Let num_arrivals := num_arrivals_of_task job_task arr_seq tsk t1 t2.
Let by_arrival_time (j j': Job) := job_arrival j ≤ job_arrival j'.
Let sorted_jobs := sort by_arrival_time arriving_jobs.
Variable elem: Job.
Let nth_job := nth elem sorted_jobs.
Remark sorted_arrivals_properties_of_nth:
∀ idx,
idx < num_arrivals →
t1 ≤ job_arrival (nth_job idx) < t2 ∧
job_task (nth_job idx) = tsk ∧
arrives_in arr_seq (nth_job idx).
Lemma sorted_arrivals_current_differs_from_next:
∀ idx,
idx < num_arrivals.-1 →
nth_job idx ≠ nth_job idx.+1.
Lemma sorted_arrivals_separated_by_period:
∀ idx,
idx < num_arrivals.-1 →
job_arrival (nth_job idx.+1) ≥ job_arrival (nth_job idx) + task_period tsk.
Section FirstAndLastJobs.
Hypothesis H_at_least_one_job:
num_arrivals ≥ 1.
Let j_first := nth_job 0.
Let j_last := nth_job (num_arrivals.-1).
Let a_first := job_arrival j_first.
Let a_last := job_arrival j_last.
Lemma sorted_arrivals_distance_from_first_job:
∀ idx,
idx < num_arrivals →
job_arrival (nth_job idx) ≥ a_first + idx × task_period tsk.
Corollary sorted_arrivals_distance_between_first_and_last:
a_last ≥ a_first + (num_arrivals-1) × task_period tsk.
End FirstAndLastJobs.
End DistanceBetweenSporadicJobs.
End TaskArrival.