# Library prosa.analysis.definitions.hyperperiod

From mathcomp Require Import div.
Require Export prosa.util.lcmseq.

In this file we define the notion of a hyperperiod for periodic tasks.
Section Hyperperiod.

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.
Definition hyperperiod : duration := lcml (map task_period ts).

End Hyperperiod.

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.
Context {Job : JobType}.
Context `{JobArrival Job}.

Consider any task set ts ...

... and any arrival sequence arr_seq.
Variable arr_seq : arrival_sequence Job.

Let O_max denote the maximum offset of all tasks in ts ...

... and let HP denote the hyperperiod of all tasks in ts.
Let HP := hyperperiod 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)
Definition hyperperiod_index (t : instant) :=
(t - O_max) %/ HP.

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.
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).

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).

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.