# Library prosa.classic.implementation.uni.jitter.arrival_sequence

Require Import prosa.classic.util.all.
prosa.classic.implementation.uni.jitter.job.
From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq div.

Module ConcreteArrivalSequence.

Section PeriodicArrivals.

(* At any time t, we release Some job of tsk if t is a multiple of the period,
otherwise we release None. *)

if task_period tsk %| arr_time then
Some (Build_concrete_job (arr_time %/ task_period tsk) arr_time
else
None.

(* The arrival sequence at any time t is simply the partial map of add_job. *)
Definition periodic_arrival_sequence (t: time) := pmap (add_job t) ts.

End PeriodicArrivals.

Section Proofs.

(* Let ts be any concrete task set with valid parameters. *)

(* Regarding the periodic arrival sequence built from ts, we prove that...*)
Let arr_seq := periodic_arrival_sequence ts.

(* ... arrival times are consistent, ... *)
Theorem periodic_arrivals_are_consistent:
arrival_times_are_consistent job_arrival arr_seq.
Proof.
movej t ARRj.
rewrite /arrives_at mem_pmap in ARRj.
move: ARRj ⇒ /mapP ARRj; destruct ARRj as [tsk IN SOME].
by unfold add_job in *; desf.
Qed.

(* ... every job comes from the task set, ... *)
j,
arrives_in arr_seq j
Proof.
movej [t ARRj].
rewrite mem_pmap in ARRj.
move: ARRj ⇒ /mapP ARRj; destruct ARRj as [tsk IN SOME].
by unfold add_job in *; desf.
Qed.

Proof.
movej j' /eqP DIFF [arr ARR] [arr' ARR'] SAMEtsk LE.
rewrite eqE /= /job_eqdef negb_and /= SAMEtsk eq_refl orbF in DIFF.
rewrite 2!mem_pmap in ARR ARR'.
move: ARR ARR' ⇒ /mapP [tsk_j INj SOMEj] /mapP [tsk_j' INj' SOMEj'].
unfold add_job in SOMEj, SOMEj'; desf; simpl in *;
move: Heq0 Heq ⇒ /dvdnP [k DIV] /dvdnP [k' DIV'].
{
rewrite DIV DIV' -mulSnr.
rewrite leq_eqVlt in LE; move: LE ⇒ /orP [/eqP EQ | LESS].
{
exfalso; move: DIFF ⇒ /negP DIFF; apply DIFF.
by subst; rewrite EQ !eq_refl.
}
subst; rewrite leq_mul2r; apply/orP; right.
by rewrite ltn_mul2r in LESS; move: LESS ⇒ /andP [_ LT].
}
Qed.

(* ... and the arrival sequence has no duplicate jobs. *)
Theorem periodic_arrivals_is_a_set:
arrival_sequence_is_a_set arr_seq.
Proof.
intros t.
unfold arr_seq, periodic_arrival_sequence.
apply (pmap_uniq) with (g := job_task); last by destruct ts.
by unfold add_job, ocancel; intro tsk; desf.
Qed.

(* We also show that job costs are bounded by task costs... *)
j,
arrives_in arr_seq j
Proof.
intros j [t ARRj].
rewrite mem_pmap in ARRj.
move: ARRj ⇒ /mapP [tsk_j INj SOMEj].
by unfold add_job in SOMEj; desf.
Qed.