Copied model/schedule/uni/basic/platform_tdma.v to restructuring/model/schedule/tdma.v

restructuring/model/schedule/tdma.v

@@ -78,11 +78,55 @@ Section TDMADefinitions.
   (* 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) :=
+  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)
+  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.
+
+Section TDMASchedule.
+
+  Context {Task : TaskType} {Job : JobType}.
+
+  Context `{JobArrival Job} `{JobCost Job} `{JobTask Job Task}.
+
+  (* Consider any job arrival sequence... *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (* ..., any uniprocessor ideal schedule ... *)
+  Variable sched : schedule (option Job).
+
+  (* ... and any sporadic task set. *)
+  Variable ts: {set Task}.
+
+  Context `{TDMAPolicy Task}.
+
+  (* In order to characterize a TDMA policy, we first define whether a job is executing its TDMA slot at time t. *)
+  Definition job_in_time_slot (job:Job) (t:instant):=
+    task_in_time_slot ts (job_task job) t.
+
+  (* We say that a TDMA policy is respected by the schedule iff
+       1. when a job is scheduled at time t, then the corresponding task
+          is also in its own time slot... *)
+  Definition sched_implies_in_slot j t:=
+    scheduled_at sched j t -> job_in_time_slot j t.
+
+  (* 2. when a job is backlogged at time t,the corresponding task
+          isn't in its own time slot or another previous job of the same task is scheduled *)
+  Definition backlogged_implies_not_in_slot_or_other_job_sched j t:=
+    backlogged sched j t ->
+    ~ job_in_time_slot j t \/
+    exists j_other, arrives_in arr_seq j_other/\
+                    job_arrival j_other < job_arrival j/\
+                    job_task j = job_task j_other/\
+                    scheduled_at sched j_other t.
+
+  Definition respects_TDMA_policy:=
+    forall (j:Job) (t:instant),
+      arrives_in arr_seq j ->
+      sched_implies_in_slot j t /\
+      backlogged_implies_not_in_slot_or_other_job_sched j t.
+End TDMASchedule.
\ No newline at end of file

restructuring/model/schedule/tdma_facts.v

@@ -39,9 +39,9 @@ Section TDMAFacts.
 
     (* Slot offset is less then cycle *)
     Lemma Offset_lt_cycle:
-      Task_slot_offset ts task < TDMA_cycle ts.
+      task_slot_offset ts task < TDMA_cycle ts.
     Proof.
-      rewrite /Task_slot_offset /TDMA_cycle big_mkcond.
+      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//=.
@@ -53,9 +53,9 @@ Section TDMAFacts.
     (* 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.
+      task_slot_offset ts task + task_time_slot task <= TDMA_cycle ts.
     Proof.
-      rewrite /Task_slot_offset /TDMA_cycle.
+      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)
@@ -94,11 +94,11 @@ Section TDMAFacts.
                                  tsk2 \in ts ->
                                           slot_order tsk1 tsk2 ->
                                           tsk1 != tsk2 ->
-                                          Task_slot_offset ts tsk2 >=
-                                          Task_slot_offset ts tsk1 + task_time_slot tsk1 .
+                                          task_slot_offset ts tsk2 >=
+                                          task_slot_offset ts tsk1 + task_time_slot tsk1 .
     Proof.
       intros* IN1 IN2 ORDER NEQ.
-      rewrite /Task_slot_offset big_mkcond addnC/=.
+      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.
@@ -117,15 +117,15 @@ Section TDMAFacts.
     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 ->
+                                            task_in_time_slot ts tsk1 t ->
+                                            task_in_time_slot ts tsk2 t ->
                                             tsk1 = tsk2.
     Proof.
       intros* IN1 SLOT1 IN2 SLOT2.
-      rewrite /Task_in_time_slot.
+      rewrite /task_in_time_slot.
       set cycle:=TDMA_cycle ts.
-      set O1:= Task_slot_offset ts tsk1.
-      set O2:= Task_slot_offset ts tsk2.
+      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).