Commit c68e8cb0 authored by Maxime Lesourd's avatar Maxime Lesourd Committed by Björn Brandenburg

copied everything from model/policy_tdma.v

parent 45853287
From rt.restructuring.behavior Require Import task schedule.ideal.
From rt.util Require Export seqset list.
From mathcomp Require Export ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div.
(** In this section, we define the TDMA policy.*)
Section TDMAPolicy.
(* The TDMA policy is based on two properties.
(1) Each task has a fixed, reserved time slot for execution;
(2) These time slots are ordered in sequence to form a TDMA cycle, which repeats along the timeline.
An example of TDMA schedule is illustrated in the following.
| s1 | s2 |s3| s1 | s2 |s3|...
0 t
Variable Task: eqType.
(* With each task, we associate the duration of the corresponding TDMA slot. *)
Definition TDMA_slot := Task -> duration.
(* Moreover, within each TDMA cycle, task slots are ordered according to some relation.
(i.e, slot_order slot1 slot2 means that slot1 comes before slot2 in a TDMA cycle) *)
Definition TDMA_slot_order := rel Task.
End TDMAPolicy.
Class TDMAPolicy (T : TaskType) :=
{ task_time_slot : TDMA_slot T;
slot_order : TDMA_slot_order T }.
(* First, we define the properties of a valid TDMA policy. *)
Section ValidTDMAPolicy.
Context {Task : eqType}.
(* Consider any task set ts... *)
Variable ts : {set Task}.
(* ...and a TDMA policy. *)
Context `{TDMAPolicy Task}.
(* Time slot order must be transitive... *)
Definition transitive_slot_order := transitive slot_order.
(* ..., totally ordered over the task set... *)
Definition total_slot_order :=
total_over_list slot_order ts.
(* ... and antisymmetric over task set. *)
Definition antisymmetric_slot_order :=
antisymmetric_over_list slot_order ts.
(* A valid time slot must be positive *)
Definition valid_time_slot :=
forall tsk, tsk \in ts -> task_time_slot tsk > 0.
Definition valid_TDMAPolicy :=
transitive_slot_order /\ total_slot_order /\ antisymmetric_slot_order /\ valid_time_slot.
End ValidTDMAPolicy.
(** In this section, we define functions on a TDMA policy *)
Section TDMADefinitions.
Context {Task : eqType}.
(* Consider any task set ts... *)
Variable ts : {set Task}.
(* ...and a TDMA policy. *)
Context `{TDMAPolicy Task}.
(* We define the TDMA cycle as the sum of all the tasks' time slots *)
Definition TDMA_cycle:=
\sum_(tsk <- ts) task_time_slot tsk.
(* We define the function returning the slot offset for each task:
i.e., the distance between the start of the TDMA cycle and
the start of the task time slot *)
Definition Task_slot_offset (tsk : Task) :=
\sum_(prev_task <- ts | slot_order prev_task tsk && (prev_task != tsk)) task_time_slot prev_task.
(* The following function tests whether a task is in its time slot at instant t *)
Definition Task_in_time_slot (tsk : Task) (t:instant):=
((t + TDMA_cycle - (Task_slot_offset tsk)%% TDMA_cycle) %% TDMA_cycle)
< (task_time_slot tsk).
End TDMADefinitions.
From rt.restructuring.model Require Export schedule.tdma.
From rt.util Require Import 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.
rewrite /TDMA_cycle (big_rem task) //.
apply:leq_trans; last by exact: leq_addr.
by apply leqnn.
(* Thus, a TDMA cycle is always positive *)
Lemma TDMA_cycle_positive:
TDMA_cycle ts > 0.
move:time_slot_positive=>/(_ task H_task_in_ts)/leq_trans;apply;apply TDMA_cycle_ge_each_time_slot.
(* Slot offset is less then cycle *)
Lemma Offset_lt_cycle:
Task_slot_offset ts task < TDMA_cycle ts.
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 (bigD1_seq task)?set_uniq//=.
rewrite -subn_gt0 -addnBA. rewrite subnn addn0 //.
exact: time_slot_positive.
(* 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.
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).
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:
(* Then, we can prove that the difference value between two offsets is
at least a slot *)
Lemma relation_offset:
forall 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 .
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.
(* Then, we proved that no two tasks share the same time slot at any time. *)
Lemma task_in_time_slot_uniq:
forall 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.
intros* 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 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 ssromega.
apply ltn_subLR in G1;apply 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 ssromega;auto. by move/eqP in NEQ. apply /eqP;auto.
End TimeSlotOrderFacts.
End TDMAFacts.
\ No newline at end of file
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment