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 any type of periodic tasks ...
... and any task set [ts].
The hyperperiod of a task set is defined as the least common multiple
(LCM) of the periods of all tasks in the task set.
In this section we provide basic definitions concerning the hyperperiod
of all tasks in a task set.
Consider any type of periodic tasks ...
... and any type of jobs.
Consider any task set [ts] ...
... and any arrival sequence [arr_seq].
Let [O_max] denote the maximum offset of all tasks in [ts] ...
... and let [HP] denote the hyperperiod of all tasks in [ts].
We define a hyperperiod index based on an instant [t]
which lies in it. Note that we consider the first hyperperiod to start at time [O_max],
i.e., shifted by the maximum offset (and not at time zero as can also
be found sometimes in the literature)
Given an instant [t], we define the starting instant of the hyperperiod
that contains [t].
Given a job [j], we define the starting instant of the hyperperiod
in which [j] arrives.
Definition starting_instant_of_corresponding_hyperperiod (j : Job) :=
starting_instant_of_hyperperiod (job_arrival j).
starting_instant_of_hyperperiod (job_arrival j).
We define the sequence of jobs of a task [tsk] that arrive in a hyperperiod
given the starting instant [h] of the hyperperiod.
Definition jobs_in_hyperperiod (h : instant) (tsk : Task) :=
task_arrivals_between arr_seq tsk h (h + HP).
task_arrivals_between arr_seq tsk h (h + HP).
We define the index of a job [j] of task [tsk] in a hyperperiod starting at [h].
Definition job_index_in_hyperperiod (j : Job) (h : instant) (tsk : Task) :=
index j (jobs_in_hyperperiod h tsk).
index j (jobs_in_hyperperiod h tsk).
Given a job [j] of task [tsk] and the hyperperiod starting at [h], we define a
[corresponding_job_in_hyperperiod] which is the job that arrives in given hyperperiod
and has the same [job_index] as [j].
Definition corresponding_job_in_hyperperiod (j : Job) (h : instant) (tsk : Task) :=
nth j (jobs_in_hyperperiod h tsk) (job_index_in_hyperperiod j (starting_instant_of_corresponding_hyperperiod j) tsk).
End HyperperiodDefinitions.
nth j (jobs_in_hyperperiod h tsk) (job_index_in_hyperperiod j (starting_instant_of_corresponding_hyperperiod j) tsk).
End HyperperiodDefinitions.