Library prosa.analysis.definitions.hyperperiod
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.model.task.arrival.periodic.
Require Export prosa.util.lcmseq.
From mathcomp Require Import div.
In this file we define the notion of a hyperperiod for periodic tasks.
Consider periodic tasks.
Consider any task set [ts]...
... and any task [tsk] that belongs to this task set.
The hyperperiod of a task set is defined as the least common multiple
(LCM) of the periods of all tasks in the task set.
Consequently, a task set's hyperperiod is an integral multiple
of each task's period in the task set.
Lemma hyperperiod_int_mult_of_any_task :
∃ k, hyperperiod = k × task_period tsk.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 264)
Task : TaskType
H : PeriodicModel Task
ts : TaskSet Task
tsk : Task
H_tsk_in_ts : tsk \in ts
============================
exists k : nat, hyperperiod = k * task_period tsk
----------------------------------------------------------------------------- *)
Proof.
apply lcm_seq_is_mult_of_all_ints.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 265)
Task : TaskType
H : PeriodicModel Task
ts : TaskSet Task
tsk : Task
H_tsk_in_ts : tsk \in ts
============================
task_period tsk \in [seq task_period i | i <- ts]
----------------------------------------------------------------------------- *)
apply map_f.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 266)
Task : TaskType
H : PeriodicModel Task
ts : TaskSet Task
tsk : Task
H_tsk_in_ts : tsk \in ts
============================
tsk \in ts
----------------------------------------------------------------------------- *)
by apply H_tsk_in_ts.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End Hyperperiod.
∃ k, hyperperiod = k × task_period tsk.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 264)
Task : TaskType
H : PeriodicModel Task
ts : TaskSet Task
tsk : Task
H_tsk_in_ts : tsk \in ts
============================
exists k : nat, hyperperiod = k * task_period tsk
----------------------------------------------------------------------------- *)
Proof.
apply lcm_seq_is_mult_of_all_ints.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 265)
Task : TaskType
H : PeriodicModel Task
ts : TaskSet Task
tsk : Task
H_tsk_in_ts : tsk \in ts
============================
task_period tsk \in [seq task_period i | i <- ts]
----------------------------------------------------------------------------- *)
apply map_f.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 266)
Task : TaskType
H : PeriodicModel Task
ts : TaskSet Task
tsk : Task
H_tsk_in_ts : tsk \in ts
============================
tsk \in ts
----------------------------------------------------------------------------- *)
by apply H_tsk_in_ts.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End Hyperperiod.