Library prosa.analysis.facts.periodic.max_inter_arrival
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.analysis.facts.periodic.arrival_separation.
Periodic Task Model respects the Task Max Inter-Arrival model.
Consider any type of periodic tasks, ...
... any type of jobs associated with the tasks, ...
... and any arrival sequence.
By using each task's period as its maximum inter-arrival time, ...
Global Instance max_inter_eq_period : TaskMaxInterArrival Task :=
{
task_max_inter_arrival_time := task_period
}.
{
task_max_inter_arrival_time := task_period
}.
... we observe that for any task [tsk],
[task_max_inter_arrival_time tsk] is positive, ...
Remark valid_period_is_valid_max_inter_arrival_time:
∀ tsk, valid_period tsk → positive_task_max_inter_arrival_time tsk.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 41)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
============================
forall tsk : Task,
valid_period tsk -> positive_task_max_inter_arrival_time tsk
----------------------------------------------------------------------------- *)
Proof. trivial.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ tsk, valid_period tsk → positive_task_max_inter_arrival_time tsk.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 41)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
============================
forall tsk : Task,
valid_period tsk -> positive_task_max_inter_arrival_time tsk
----------------------------------------------------------------------------- *)
Proof. trivial.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
... and show that the periodic model respects the task max inter-arrival model.
Remark periodic_model_respects_max_inter_arrival_model:
∀ tsk,
valid_period tsk →
respects_periodic_task_model arr_seq tsk →
valid_task_max_inter_arrival_time arr_seq tsk.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 58)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
============================
forall tsk : Task,
valid_period tsk ->
respects_periodic_task_model arr_seq tsk ->
valid_task_max_inter_arrival_time arr_seq tsk
----------------------------------------------------------------------------- *)
Proof.
intros tsk VALID_PERIOD PERIODIC.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 61)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
tsk : Task
VALID_PERIOD : valid_period tsk
PERIODIC : respects_periodic_task_model arr_seq tsk
============================
valid_task_max_inter_arrival_time arr_seq tsk
----------------------------------------------------------------------------- *)
split; first by apply VALID_PERIOD ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 64)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
tsk : Task
VALID_PERIOD : valid_period tsk
PERIODIC : respects_periodic_task_model arr_seq tsk
============================
arr_sep_task_max_inter_arrival arr_seq tsk
----------------------------------------------------------------------------- *)
intros j ARR TSK IND.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 69)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
tsk : Task
VALID_PERIOD : valid_period tsk
PERIODIC : respects_periodic_task_model arr_seq tsk
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
IND : 0 < job_index arr_seq j
============================
exists 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
----------------------------------------------------------------------------- *)
specialize (PERIODIC j); feed_n 3 PERIODIC ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 89)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
tsk : Task
VALID_PERIOD : valid_period tsk
j : Job
PERIODIC : exists j' : Job,
arrives_in arr_seq j' /\
job_index arr_seq j' = job_index arr_seq j - 1 /\
job_task j' = tsk /\
job_arrival j = job_arrival j' + task_period tsk
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
IND : 0 < job_index arr_seq j
============================
exists 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
----------------------------------------------------------------------------- *)
move : PERIODIC ⇒ [j' [ARR' [IND' [TSK' ARRJ']]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 159)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
tsk : Task
VALID_PERIOD : valid_period tsk
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
IND : 0 < job_index arr_seq j
j' : Job
ARR' : arrives_in arr_seq j'
IND' : job_index arr_seq j' = job_index arr_seq j - 1
TSK' : job_task j' = tsk
ARRJ' : job_arrival j = job_arrival j' + task_period tsk
============================
exists j'0 : Job,
j <> j'0 /\
arrives_in arr_seq j'0 /\
job_task j'0 = tsk /\
job_arrival j'0 <= job_arrival j <=
job_arrival j'0 + task_max_inter_arrival_time tsk
----------------------------------------------------------------------------- *)
∃ j'; repeat split ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 163)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
tsk : Task
VALID_PERIOD : valid_period tsk
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
IND : 0 < job_index arr_seq j
j' : Job
ARR' : arrives_in arr_seq j'
IND' : job_index arr_seq j' = job_index arr_seq j - 1
TSK' : job_task j' = tsk
ARRJ' : job_arrival j = job_arrival j' + task_period tsk
============================
j <> j'
subgoal 2 (ID 319) is:
job_arrival j' <= job_arrival j <=
job_arrival j' + task_max_inter_arrival_time tsk
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 163)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
tsk : Task
VALID_PERIOD : valid_period tsk
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
IND : 0 < job_index arr_seq j
j' : Job
ARR' : arrives_in arr_seq j'
IND' : job_index arr_seq j' = job_index arr_seq j - 1
TSK' : job_task j' = tsk
ARRJ' : job_arrival j = job_arrival j' + task_period tsk
============================
j <> j'
----------------------------------------------------------------------------- *)
case: (boolP (j == j')) ⇒ [/eqP EQ|NEQ].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 388)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
tsk : Task
VALID_PERIOD : valid_period tsk
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
IND : 0 < job_index arr_seq j
j' : Job
ARR' : arrives_in arr_seq j'
IND' : job_index arr_seq j' = job_index arr_seq j - 1
TSK' : job_task j' = tsk
ARRJ' : job_arrival j = job_arrival j' + task_period tsk
EQ : j = j'
============================
j <> j'
subgoal 2 (ID 387) is:
j <> j'
----------------------------------------------------------------------------- *)
- have EQ_IND : (job_index arr_seq j' = job_index arr_seq j) by apply f_equal ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 421)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
tsk : Task
VALID_PERIOD : valid_period tsk
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
IND : 0 < job_index arr_seq j
j' : Job
ARR' : arrives_in arr_seq j'
IND' : job_index arr_seq j' = job_index arr_seq j - 1
TSK' : job_task j' = tsk
ARRJ' : job_arrival j = job_arrival j' + task_period tsk
EQ : j = j'
EQ_IND : job_index arr_seq j' = job_index arr_seq j
============================
j <> j'
subgoal 2 (ID 387) is:
j <> j'
----------------------------------------------------------------------------- *)
now exfalso; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 387)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
tsk : Task
VALID_PERIOD : valid_period tsk
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
IND : 0 < job_index arr_seq j
j' : Job
ARR' : arrives_in arr_seq j'
IND' : job_index arr_seq j' = job_index arr_seq j - 1
TSK' : job_task j' = tsk
ARRJ' : job_arrival j = job_arrival j' + task_period tsk
NEQ : j != j'
============================
j <> j'
----------------------------------------------------------------------------- *)
- now apply /eqP.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 319)
subgoal 1 (ID 319) is:
job_arrival j' <= job_arrival j <=
job_arrival j' + task_max_inter_arrival_time tsk
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 319)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
tsk : Task
VALID_PERIOD : valid_period tsk
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
IND : 0 < job_index arr_seq j
j' : Job
ARR' : arrives_in arr_seq j'
IND' : job_index arr_seq j' = job_index arr_seq j - 1
TSK' : job_task j' = tsk
ARRJ' : job_arrival j = job_arrival j' + task_period tsk
============================
job_arrival j' <= job_arrival j <=
job_arrival j' + task_max_inter_arrival_time tsk
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 319)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
tsk : Task
VALID_PERIOD : valid_period tsk
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
IND : 0 < job_index arr_seq j
j' : Job
ARR' : arrives_in arr_seq j'
IND' : job_index arr_seq j' = job_index arr_seq j - 1
TSK' : job_task j' = tsk
ARRJ' : job_arrival j = job_arrival j' + task_period tsk
============================
job_arrival j' <= job_arrival j <=
job_arrival j' + task_max_inter_arrival_time tsk
----------------------------------------------------------------------------- *)
have NZ_PERIOD : (task_period tsk > 0) by apply VALID_PERIOD.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 712)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
tsk : Task
VALID_PERIOD : valid_period tsk
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
IND : 0 < job_index arr_seq j
j' : Job
ARR' : arrives_in arr_seq j'
IND' : job_index arr_seq j' = job_index arr_seq j - 1
TSK' : job_task j' = tsk
ARRJ' : job_arrival j = job_arrival j' + task_period tsk
NZ_PERIOD : 0 < task_period tsk
============================
job_arrival j' <= job_arrival j <=
job_arrival j' + task_max_inter_arrival_time tsk
----------------------------------------------------------------------------- *)
rewrite /max_inter_eq_period /task_max_inter_arrival_time ARRJ'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 720)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
tsk : Task
VALID_PERIOD : valid_period tsk
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
IND : 0 < job_index arr_seq j
j' : Job
ARR' : arrives_in arr_seq j'
IND' : job_index arr_seq j' = job_index arr_seq j - 1
TSK' : job_task j' = tsk
ARRJ' : job_arrival j = job_arrival j' + task_period tsk
NZ_PERIOD : 0 < task_period tsk
============================
job_arrival j' <= job_arrival j' + task_period tsk <=
job_arrival j' + task_period tsk
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End PeriodicTasksRespectMaxInterArrivalModel.
∀ tsk,
valid_period tsk →
respects_periodic_task_model arr_seq tsk →
valid_task_max_inter_arrival_time arr_seq tsk.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 58)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
============================
forall tsk : Task,
valid_period tsk ->
respects_periodic_task_model arr_seq tsk ->
valid_task_max_inter_arrival_time arr_seq tsk
----------------------------------------------------------------------------- *)
Proof.
intros tsk VALID_PERIOD PERIODIC.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 61)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
tsk : Task
VALID_PERIOD : valid_period tsk
PERIODIC : respects_periodic_task_model arr_seq tsk
============================
valid_task_max_inter_arrival_time arr_seq tsk
----------------------------------------------------------------------------- *)
split; first by apply VALID_PERIOD ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 64)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
tsk : Task
VALID_PERIOD : valid_period tsk
PERIODIC : respects_periodic_task_model arr_seq tsk
============================
arr_sep_task_max_inter_arrival arr_seq tsk
----------------------------------------------------------------------------- *)
intros j ARR TSK IND.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 69)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
tsk : Task
VALID_PERIOD : valid_period tsk
PERIODIC : respects_periodic_task_model arr_seq tsk
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
IND : 0 < job_index arr_seq j
============================
exists 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
----------------------------------------------------------------------------- *)
specialize (PERIODIC j); feed_n 3 PERIODIC ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 89)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
tsk : Task
VALID_PERIOD : valid_period tsk
j : Job
PERIODIC : exists j' : Job,
arrives_in arr_seq j' /\
job_index arr_seq j' = job_index arr_seq j - 1 /\
job_task j' = tsk /\
job_arrival j = job_arrival j' + task_period tsk
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
IND : 0 < job_index arr_seq j
============================
exists 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
----------------------------------------------------------------------------- *)
move : PERIODIC ⇒ [j' [ARR' [IND' [TSK' ARRJ']]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 159)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
tsk : Task
VALID_PERIOD : valid_period tsk
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
IND : 0 < job_index arr_seq j
j' : Job
ARR' : arrives_in arr_seq j'
IND' : job_index arr_seq j' = job_index arr_seq j - 1
TSK' : job_task j' = tsk
ARRJ' : job_arrival j = job_arrival j' + task_period tsk
============================
exists j'0 : Job,
j <> j'0 /\
arrives_in arr_seq j'0 /\
job_task j'0 = tsk /\
job_arrival j'0 <= job_arrival j <=
job_arrival j'0 + task_max_inter_arrival_time tsk
----------------------------------------------------------------------------- *)
∃ j'; repeat split ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 163)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
tsk : Task
VALID_PERIOD : valid_period tsk
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
IND : 0 < job_index arr_seq j
j' : Job
ARR' : arrives_in arr_seq j'
IND' : job_index arr_seq j' = job_index arr_seq j - 1
TSK' : job_task j' = tsk
ARRJ' : job_arrival j = job_arrival j' + task_period tsk
============================
j <> j'
subgoal 2 (ID 319) is:
job_arrival j' <= job_arrival j <=
job_arrival j' + task_max_inter_arrival_time tsk
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 163)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
tsk : Task
VALID_PERIOD : valid_period tsk
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
IND : 0 < job_index arr_seq j
j' : Job
ARR' : arrives_in arr_seq j'
IND' : job_index arr_seq j' = job_index arr_seq j - 1
TSK' : job_task j' = tsk
ARRJ' : job_arrival j = job_arrival j' + task_period tsk
============================
j <> j'
----------------------------------------------------------------------------- *)
case: (boolP (j == j')) ⇒ [/eqP EQ|NEQ].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 388)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
tsk : Task
VALID_PERIOD : valid_period tsk
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
IND : 0 < job_index arr_seq j
j' : Job
ARR' : arrives_in arr_seq j'
IND' : job_index arr_seq j' = job_index arr_seq j - 1
TSK' : job_task j' = tsk
ARRJ' : job_arrival j = job_arrival j' + task_period tsk
EQ : j = j'
============================
j <> j'
subgoal 2 (ID 387) is:
j <> j'
----------------------------------------------------------------------------- *)
- have EQ_IND : (job_index arr_seq j' = job_index arr_seq j) by apply f_equal ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 421)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
tsk : Task
VALID_PERIOD : valid_period tsk
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
IND : 0 < job_index arr_seq j
j' : Job
ARR' : arrives_in arr_seq j'
IND' : job_index arr_seq j' = job_index arr_seq j - 1
TSK' : job_task j' = tsk
ARRJ' : job_arrival j = job_arrival j' + task_period tsk
EQ : j = j'
EQ_IND : job_index arr_seq j' = job_index arr_seq j
============================
j <> j'
subgoal 2 (ID 387) is:
j <> j'
----------------------------------------------------------------------------- *)
now exfalso; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 387)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
tsk : Task
VALID_PERIOD : valid_period tsk
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
IND : 0 < job_index arr_seq j
j' : Job
ARR' : arrives_in arr_seq j'
IND' : job_index arr_seq j' = job_index arr_seq j - 1
TSK' : job_task j' = tsk
ARRJ' : job_arrival j = job_arrival j' + task_period tsk
NEQ : j != j'
============================
j <> j'
----------------------------------------------------------------------------- *)
- now apply /eqP.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 319)
subgoal 1 (ID 319) is:
job_arrival j' <= job_arrival j <=
job_arrival j' + task_max_inter_arrival_time tsk
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 319)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
tsk : Task
VALID_PERIOD : valid_period tsk
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
IND : 0 < job_index arr_seq j
j' : Job
ARR' : arrives_in arr_seq j'
IND' : job_index arr_seq j' = job_index arr_seq j - 1
TSK' : job_task j' = tsk
ARRJ' : job_arrival j = job_arrival j' + task_period tsk
============================
job_arrival j' <= job_arrival j <=
job_arrival j' + task_max_inter_arrival_time tsk
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 319)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
tsk : Task
VALID_PERIOD : valid_period tsk
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
IND : 0 < job_index arr_seq j
j' : Job
ARR' : arrives_in arr_seq j'
IND' : job_index arr_seq j' = job_index arr_seq j - 1
TSK' : job_task j' = tsk
ARRJ' : job_arrival j = job_arrival j' + task_period tsk
============================
job_arrival j' <= job_arrival j <=
job_arrival j' + task_max_inter_arrival_time tsk
----------------------------------------------------------------------------- *)
have NZ_PERIOD : (task_period tsk > 0) by apply VALID_PERIOD.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 712)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
tsk : Task
VALID_PERIOD : valid_period tsk
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
IND : 0 < job_index arr_seq j
j' : Job
ARR' : arrives_in arr_seq j'
IND' : job_index arr_seq j' = job_index arr_seq j - 1
TSK' : job_task j' = tsk
ARRJ' : job_arrival j = job_arrival j' + task_period tsk
NZ_PERIOD : 0 < task_period tsk
============================
job_arrival j' <= job_arrival j <=
job_arrival j' + task_max_inter_arrival_time tsk
----------------------------------------------------------------------------- *)
rewrite /max_inter_eq_period /task_max_inter_arrival_time ARRJ'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 720)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
tsk : Task
VALID_PERIOD : valid_period tsk
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
IND : 0 < job_index arr_seq j
j' : Job
ARR' : arrives_in arr_seq j'
IND' : job_index arr_seq j' = job_index arr_seq j - 1
TSK' : job_task j' = tsk
ARRJ' : job_arrival j = job_arrival j' + task_period tsk
NZ_PERIOD : 0 < task_period tsk
============================
job_arrival j' <= job_arrival j' + task_period tsk <=
job_arrival j' + task_period tsk
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End PeriodicTasksRespectMaxInterArrivalModel.