Library prosa.analysis.definitions.hyperperiod
Require Export prosa.model.task.arrival.periodic.
Require Export prosa.util.lcmseq.
From mathcomp Require Import div.
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.