add notion of hyperperiod for periodic tasks

analysis/definitions/hyperperiod.v

+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. *)
+Section Hyperperiod.
+
+  (** Consider periodic tasks. *)
+  Context {Task : TaskType} `{PeriodicModel Task}.
+
+  (** Consider any task set [ts]... *)
+  Variable ts : TaskSet Task.
+
+  (** ... and any task [tsk] that belongs to this task set. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts : tsk \in 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).        
+
+  (** 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 : 
+    exists k, hyperperiod = k * task_period tsk.
+  Proof.
+    apply lcm_seq_is_mult_of_all_ints.
+    apply map_f.
+    by apply H_tsk_in_ts.
+  Qed.
+
+End Hyperperiod.
+

scripts/wordlist.pws

@@ -48,3 +48,4 @@ runtime
 bursty
 TODO
 mathcomp
+hyperperiod

util/lcmseq.v

+From mathcomp Require Export ssreflect seq div ssrbool ssrnat eqtype ssrfun.
+
+(** A function to calculate the least common multiple 
+    of all integers in a sequence [xs], denoted by [lcml xs]  **)
+Definition lcml (xs : seq nat) : nat := foldr lcmn 1 xs.
+
+(** Any integer [a] that is contained in the sequence [xs] divides [lcml xs]. **)
+Lemma int_divides_lcm_in_seq : 
+  forall (a : nat) (xs : seq nat), a %| lcml (a :: xs).
+Proof.
+  intros.
+  rewrite /lcml.
+  induction xs.
+  - rewrite /foldr.
+    now apply dvdn_lcml.
+  - rewrite -cat1s.
+    rewrite foldr_cat /foldr.
+    by apply dvdn_lcml.
+Qed.
+
+(** Also, [lcml xs1] divides [lcml xs2] if [xs2] contains one extra element as compared to [xs1]. *)
+Lemma lcm_seq_divides_lcm_super : 
+  forall (x : nat) (xs : seq nat), 
+  lcml xs %| lcml (x :: xs).
+Proof.
+  intros.
+  rewrite /lcml.
+  induction xs; first by auto.
+  rewrite -cat1s foldr_cat /foldr.
+  by apply dvdn_lcmr.
+Qed.
+
+(** All integers in a sequence [xs] divide [lcml xs]. *)
+Lemma lcm_seq_is_mult_of_all_ints : 
+  forall (sq : seq nat) (a : nat), a \in sq -> exists k, lcml sq = k * a. 
+Proof.
+  intros xs x IN.
+  induction xs as [ | z sq IH_DIVIDES]; first by easy.
+  rewrite in_cons in IN.
+  move : IN => /orP [/eqP EQ | IN].
+  + apply /dvdnP.
+    rewrite EQ /lcml.
+    by apply int_divides_lcm_in_seq.
+  + move : (IH_DIVIDES IN) => [k EQ].
+    exists ((foldr lcmn 1 (z :: sq)) %/ (foldr lcmn 1 sq) * k).
+    rewrite -mulnA -EQ divnK /lcml //.
+    by apply lcm_seq_divides_lcm_super.
+Qed.