# Library prosa.analysis.facts.tdma

Require Export prosa.model.schedule.tdma.
Require Import prosa.util.all.
In this section, we define the properties of TDMA and prove some basic lemmas.
Section TDMAFacts.
Context {Task : eqType}.
Consider any task set ts...
Variable ts : {set Task}.
... with a TDMA policy
Context `{TDMAPolicy Task}.
Section TimeSlotFacts.
Consider any task in ts
Variable task : Task.
Hypothesis H_task_in_ts : task \in ts.
Assume task_time_slot is valid time slot
Hypothesis time_slot_positive :
valid_time_slot ts.
Obviously, the TDMA cycle is greater or equal than any task time slot which is in TDMA cycle
Lemma TDMA_cycle_ge_each_time_slot :
TDMA_cycle ts ≥ task_time_slot task.
Proof.
rewrite /TDMA_cycle (big_rem task) //.
apply:leq_trans; last by exact: leq_addr.
by apply leqnn.
Qed.
Thus, a TDMA cycle is always positive
Lemma TDMA_cycle_positive :
TDMA_cycle ts > 0.
Proof.
move:time_slot_positive=>/(_ task H_task_in_ts)/leq_trans;apply;apply TDMA_cycle_ge_each_time_slot.
Qed.
Slot offset is less then cycle
Lemma Offset_lt_cycle :
task_slot_offset ts task < TDMA_cycle ts.
Proof.
rewrite /task_slot_offset /TDMA_cycle big_mkcond.
apply leq_ltn_trans with (n:=\sum_(prev_task <- ts )if prev_task!=task then task_time_slot prev_task else 0).
- apply leq_sum ⇒ i T. case (slot_order i task);auto.
- rewrite -big_mkcond (bigD1_seq task)?set_uniq//=.
by rewrite -subn_gt0 -addnBA // subnn addn0.
Qed.
For a task, the sum of its slot offset and its time slot is less then or equal to cycle.
Lemma Offset_add_slot_leq_cycle :
task_slot_offset ts task + task_time_slot task ≤ TDMA_cycle ts.
Proof.
rewrite /task_slot_offset /TDMA_cycle.
rewrite addnC (bigD1_seq task) //=; last by exact: (set_uniq ts).
rewrite leq_add2l big_mkcond.
replace (\sum_(i <- ts | i != task) task_time_slot i)
with (\sum_(i <- ts ) if i != task then task_time_slot i else 0).
+ apply leq_sum ⇒ i T; case (slot_order i task);auto.
+ by rewrite -big_mkcond.
Qed.
End TimeSlotFacts.
Now we prove that no two tasks share the same time slot at any time.
Section TimeSlotOrderFacts.
Consider any task in ts
Variable task : Task.
Hypothesis H_task_in_ts : task \in ts.
Assume task_time_slot is valid time slot
Hypothesis time_slot_positive :
valid_time_slot ts.
Assume that slot order is total, ...
Hypothesis slot_order_total :
total_slot_order ts.
... antisymmetric, ...
Hypothesis slot_order_antisymmetric :
antisymmetric_slot_order ts.
... and transitive.
Hypothesis slot_order_transitive :
transitive_slot_order.
Then, we can prove that the difference value between two offsets is at least a slot
Lemma relation_offset :
∀ tsk1 tsk2, tsk1 \in ts →
tsk2 \in ts →
slot_order tsk1 tsk2 →
tsk1 != tsk2 →
task_slot_offset ts tsk2 ≥
task_slot_offset ts tsk1 + task_time_slot tsk1 .
Proof.
move⇒ tsk1 tsk2 IN1 IN2 ORDER NEQ.
rewrite /task_slot_offset big_mkcond addnC/=.
replace (\sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk)
with (task_time_slot tsk1 + \sum_(tsk <- ts )if slot_order tsk tsk2 && (tsk != tsk1) && (tsk!=tsk2) then task_time_slot tsk else O).
- rewrite leq_add2l. apply leq_sum_seq ⇒ i IN T.
case (slot_order i tsk1)eqn:SI2;auto. case (i==tsk1)eqn:IT2;auto;simpl.
case (i==tsk2)eqn:IT1;simpl;auto.
+ by move/eqP in IT1;rewrite IT1 in SI2;apply slot_order_antisymmetric in ORDER;auto;apply ORDER in SI2;move/eqP in NEQ.
+ by rewrite (slot_order_transitive _ _ _ SI2 ORDER).
- symmetry. rewrite big_mkcond /=. rewrite→bigD1_seq with (j:=tsk1);auto;last by apply (set_uniq ts).
move/eqP /eqP in ORDER. move/eqP in NEQ. rewrite ORDER //=. apply /eqP.
have TS2: (tsk1 != tsk2) = true .
+ exact /eqP.
+ rewrite TS2.
rewrite eqn_add2l.
rewrite big_mkcond.
apply/eqP.
apply eq_bigr;auto ⇒ i T.
by case(i!=tsk1); case (slot_order i tsk2); case (i!=tsk2); auto.
Qed.
Then, we proved that no two tasks share the same time slot at any time.
Lemma task_in_time_slot_uniq :
∀ tsk1 tsk2 t,
tsk1 \in ts → task_time_slot tsk1 > 0 →
tsk2 \in ts → task_time_slot tsk2 > 0 →
task_in_time_slot ts tsk1 t →
task_in_time_slot ts tsk2 t →
tsk1 = tsk2.
Proof.
intros tsk1 tsk2 t IN1 SLOT1 IN2 SLOT2.
rewrite /task_in_time_slot.
set cycle := TDMA_cycle ts.
set O1 := task_slot_offset ts tsk1.
set O2 := task_slot_offset ts tsk2.
have CO1 : O1 < cycle by apply Offset_lt_cycle.
have CO2 : O2 < cycle by apply Offset_lt_cycle.
have C : cycle > 0 by apply (TDMA_cycle_positive tsk1).
have → : O1 %% cycle = O1 by apply modn_small, Offset_lt_cycle.
have → : O2 %% cycle = O2 by apply modn_small, Offset_lt_cycle.
have SO1 : O1 + task_time_slot tsk1 ≤ cycle by apply (Offset_add_slot_leq_cycle tsk1).
have SO2 : O2 + task_time_slot tsk2 ≤ cycle by apply (Offset_add_slot_leq_cycle tsk2).
repeat rewrite mod_elim; auto.
case (O1 ≤ t %% cycle) eqn:O1T; case (O2 ≤ t %% cycle) eqn:O2T; intros G1 G2; try lia.
rewrite ltn_subLR // in G1; rewrite ltn_subLR // in G2.
case (tsk1 == tsk2) eqn:NEQ; move/eqP in NEQ; auto.
destruct (slot_order_total tsk1 tsk2) as [order | order]; auto.
all: by apply relation_offset in order; fold O1 O2 in order; try lia; auto; apply/eqP; auto.
Qed.
End TimeSlotOrderFacts.
End TDMAFacts.