Built with Alectryon, running Coq+SerAPI v8.19.0+0.19.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing,default]
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 ... *) Context {Task : TaskType} `{PeriodicModel Task}. (** ... and any task set [ts]. *) Variable ts : TaskSet Task. (** 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. *) Section HyperperiodDefinitions. (** Consider any type of periodic tasks ... *) Context {Task : TaskType}. Context `{TaskOffset Task}. Context `{PeriodicModel Task}. (** ... and any type of jobs. *) Context {Job : JobType}. Context `{JobTask Job Task}. Context `{JobArrival Job}. (** Consider any task set [ts] ... *) Variable ts : TaskSet Task. (** ... and any arrival sequence [arr_seq]. *) Variable arr_seq : arrival_sequence Job. (** Let [O_max] denote the maximum offset of all tasks in [ts] ... *) Let O_max := max_task_offset 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]. *) Definition starting_instant_of_hyperperiod (t : instant) := hyperperiod_index t * HP + O_max. (** 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). (** 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]. *) 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.