Library prosa.classic.model.policy_tdma
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.time
prosa.classic.model.arrival.basic.task
prosa.classic.model.arrival.basic.job.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div.
Module PolicyTDMA.
Import Time.
Require Import prosa.classic.model.time
prosa.classic.model.arrival.basic.task
prosa.classic.model.arrival.basic.job.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div.
Module PolicyTDMA.
Import Time.
In this section, we define the TDMA policy.
Section TDMA.
Variable Task: eqType.
Definition TDMA_slot:= Task → duration.
Definition TDMA_slot_order:= rel Task.
End TDMA.
Variable Task: eqType.
Definition TDMA_slot:= Task → duration.
Definition TDMA_slot_order:= rel Task.
End TDMA.
In this section, we define the properties of TDMA and prove some basic lemmas.
Section PropertiesTDMA.
Context {Task:eqType}.
Variable ts: {set Task}.
Variable slot_order: TDMA_slot_order Task.
Section Relation.
Definition slot_order_is_transitive:= transitive slot_order.
Definition slot_order_is_total_over_task_set :=
total_over_list slot_order ts.
Definition slot_order_is_antisymmetric_over_task_set :=
antisymmetric_over_list slot_order ts.
End Relation.
Section TimeSlot.
Variable task: Task.
Hypothesis H_task_in_ts: task \in ts.
Variable task_time_slot: TDMA_slot Task.
Definition is_valid_time_slot:=
task_time_slot task > 0.
Definition TDMA_cycle:=
\sum_(tsk <- ts) task_time_slot tsk.
Definition Task_slot_offset:=
\sum_(prev_task <- ts | slot_order prev_task task && (prev_task != task)) task_time_slot prev_task.
Definition Task_in_time_slot (t:time):=
((t + TDMA_cycle - (Task_slot_offset)%% TDMA_cycle) %% TDMA_cycle)
< (task_time_slot task).
Section BasicLemmas.
Hypothesis time_slot_positive:
is_valid_time_slot.
Lemma TDMA_cycle_ge_each_time_slot:
TDMA_cycle ≥ task_time_slot task.
Proof.
rewrite /TDMA_cycle (big_rem task) //.
apply:leq_trans; last by exact: leq_addr.
by apply leqnn.
Qed.
Lemma TDMA_cycle_positive:
TDMA_cycle > 0.
Proof.
move:time_slot_positive. move/leq_trans;apply;apply TDMA_cycle_ge_each_time_slot.
Qed.
Lemma Offset_lt_cycle:
Task_slot_offset < TDMA_cycle.
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. intros× T. case (slot_order i task);auto.
- rewrite -big_mkcond. rewrite→ bigD1_seq with (j:=task);auto.
rewrite -subn_gt0 -addnBA. rewrite subnn addn0 //.
trivial. apply (set_uniq ts).
Qed.
Lemma Offset_add_slot_leq_cycle:
Task_slot_offset + task_time_slot task ≤ TDMA_cycle.
Proof.
rewrite /Task_slot_offset /TDMA_cycle.
rewrite addnC (bigD1_seq task) //=. rewrite leq_add2l.
rewrite 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. intros×T. case (slot_order i task);auto.
by rewrite -big_mkcond. apply (set_uniq ts).
Qed.
End BasicLemmas.
End TimeSlot.
Section InTimeSlotUniq.
Variable task_time_slot: TDMA_slot Task.
Hypothesis slot_order_total:
slot_order_is_total_over_task_set.
Hypothesis slot_order_antisymmetric:
slot_order_is_antisymmetric_over_task_set.
Hypothesis slot_order_transitive:
slot_order_is_transitive.
Lemma relation_offset:
∀ tsk1 tsk2, tsk1 \in ts → tsk2 \in ts →
slot_order tsk1 tsk2 → tsk1 != tsk2 →
Task_slot_offset tsk2 task_time_slot ≥ Task_slot_offset tsk1 task_time_slot + task_time_slot tsk1 .
Proof.
intros× 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. intros× 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 . apply /eqP;auto. rewrite TS2.
rewrite eqn_add2l. rewrite big_mkcond. apply/eqP. apply eq_bigr;auto.
intros× T. case(i!=tsk1);case (slot_order i tsk2);case (i!=tsk2) ;auto.
Qed.
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 tsk1 task_time_slot t →
Task_in_time_slot tsk2 task_time_slot t →
tsk1 = tsk2.
Proof.
intros× IN1 SLOT1 IN2 SLOT2.
rewrite /Task_in_time_slot.
set cycle:=TDMA_cycle task_time_slot.
set O1:= Task_slot_offset tsk1 task_time_slot.
set O2:= Task_slot_offset tsk2 task_time_slot.
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 GO1:O1 %% cycle = O1 by apply modn_small,Offset_lt_cycle. rewrite GO1.
have GO2:O2 %% cycle = O2 by apply modn_small,Offset_lt_cycle. rewrite GO2.
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 ssrlia.
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;apply relation_offset in order;
fold O1 O2 in order;try ssrlia;auto. by move/eqP in NEQ. apply /eqP;auto.
Qed.
End InTimeSlotUniq.
End PropertiesTDMA.
End PolicyTDMA.
Context {Task:eqType}.
Variable ts: {set Task}.
Variable slot_order: TDMA_slot_order Task.
Section Relation.
Definition slot_order_is_transitive:= transitive slot_order.
Definition slot_order_is_total_over_task_set :=
total_over_list slot_order ts.
Definition slot_order_is_antisymmetric_over_task_set :=
antisymmetric_over_list slot_order ts.
End Relation.
Section TimeSlot.
Variable task: Task.
Hypothesis H_task_in_ts: task \in ts.
Variable task_time_slot: TDMA_slot Task.
Definition is_valid_time_slot:=
task_time_slot task > 0.
Definition TDMA_cycle:=
\sum_(tsk <- ts) task_time_slot tsk.
Definition Task_slot_offset:=
\sum_(prev_task <- ts | slot_order prev_task task && (prev_task != task)) task_time_slot prev_task.
Definition Task_in_time_slot (t:time):=
((t + TDMA_cycle - (Task_slot_offset)%% TDMA_cycle) %% TDMA_cycle)
< (task_time_slot task).
Section BasicLemmas.
Hypothesis time_slot_positive:
is_valid_time_slot.
Lemma TDMA_cycle_ge_each_time_slot:
TDMA_cycle ≥ task_time_slot task.
Proof.
rewrite /TDMA_cycle (big_rem task) //.
apply:leq_trans; last by exact: leq_addr.
by apply leqnn.
Qed.
Lemma TDMA_cycle_positive:
TDMA_cycle > 0.
Proof.
move:time_slot_positive. move/leq_trans;apply;apply TDMA_cycle_ge_each_time_slot.
Qed.
Lemma Offset_lt_cycle:
Task_slot_offset < TDMA_cycle.
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. intros× T. case (slot_order i task);auto.
- rewrite -big_mkcond. rewrite→ bigD1_seq with (j:=task);auto.
rewrite -subn_gt0 -addnBA. rewrite subnn addn0 //.
trivial. apply (set_uniq ts).
Qed.
Lemma Offset_add_slot_leq_cycle:
Task_slot_offset + task_time_slot task ≤ TDMA_cycle.
Proof.
rewrite /Task_slot_offset /TDMA_cycle.
rewrite addnC (bigD1_seq task) //=. rewrite leq_add2l.
rewrite 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. intros×T. case (slot_order i task);auto.
by rewrite -big_mkcond. apply (set_uniq ts).
Qed.
End BasicLemmas.
End TimeSlot.
Section InTimeSlotUniq.
Variable task_time_slot: TDMA_slot Task.
Hypothesis slot_order_total:
slot_order_is_total_over_task_set.
Hypothesis slot_order_antisymmetric:
slot_order_is_antisymmetric_over_task_set.
Hypothesis slot_order_transitive:
slot_order_is_transitive.
Lemma relation_offset:
∀ tsk1 tsk2, tsk1 \in ts → tsk2 \in ts →
slot_order tsk1 tsk2 → tsk1 != tsk2 →
Task_slot_offset tsk2 task_time_slot ≥ Task_slot_offset tsk1 task_time_slot + task_time_slot tsk1 .
Proof.
intros× 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. intros× 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 . apply /eqP;auto. rewrite TS2.
rewrite eqn_add2l. rewrite big_mkcond. apply/eqP. apply eq_bigr;auto.
intros× T. case(i!=tsk1);case (slot_order i tsk2);case (i!=tsk2) ;auto.
Qed.
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 tsk1 task_time_slot t →
Task_in_time_slot tsk2 task_time_slot t →
tsk1 = tsk2.
Proof.
intros× IN1 SLOT1 IN2 SLOT2.
rewrite /Task_in_time_slot.
set cycle:=TDMA_cycle task_time_slot.
set O1:= Task_slot_offset tsk1 task_time_slot.
set O2:= Task_slot_offset tsk2 task_time_slot.
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 GO1:O1 %% cycle = O1 by apply modn_small,Offset_lt_cycle. rewrite GO1.
have GO2:O2 %% cycle = O2 by apply modn_small,Offset_lt_cycle. rewrite GO2.
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 ssrlia.
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;apply relation_offset in order;
fold O1 O2 in order;try ssrlia;auto. by move/eqP in NEQ. apply /eqP;auto.
Qed.
End InTimeSlotUniq.
End PropertiesTDMA.
End PolicyTDMA.