Library rt.model.policy_tdma

Require Import rt.util.all.
Require Import rt.model.time

Module PolicyTDMA.

  Import Time.

In this section, we define the TDMA policy.
  Section TDMA.
    (* 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. *)
    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}.

    (* Consider any task set ts... *)
    Variable ts: {set Task}.

    (* ...and any slot order (i.e, slot_order slot1 slot2 means that slot1 comes before slot2 in a TDMA cycle). *)
    Variable slot_order: TDMA_slot_order Task.

    (* First, we define the properties of a valid time slot order. *)
    Section Relation.
      (* Time slot order must transitive... *)
      Definition slot_order_is_transitive:= transitive slot_order.

      (* ..., totally ordered over the task set... *)
      Definition slot_order_is_total_over_task_set :=
        total_over_list slot_order ts.

      (* ... and antisymmetric over task set. *)
      Definition slot_order_is_antisymmetric_over_task_set :=
        antisymmetric_over_list slot_order ts.

    End Relation.

    (* Next, we define some properties of task time slots *)
    Section TimeSlot.

      (* Consider any task in task set ts*)
      Variable task: Task.
      Hypothesis H_task_in_ts: task \in ts.

      (* Consider any TDMA slot assignment for these tasks *)
      Variable task_time_slot: TDMA_slot Task.

      (* A valid time slot must be positive *)
      Definition is_valid_time_slot:=
        task_time_slot task > 0.

      (* 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:=
        \sum_(prev_task <- ts | slot_order prev_task task && (prev_task != task)) 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 (t:time):=
       ((t + TDMA_cycle - (Task_slot_offset)%% TDMA_cycle) %% TDMA_cycle)
        < (task_time_slot task).

      Section BasicLemmas.

        (* Assume task_time_slot is valid time slot*)
        Hypothesis time_slot_positive:

        (* 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 task_time_slot task.

        (* Thus, a TDMA cycle is always positive *)
        Lemma TDMA_cycle_positive:
          TDMA_cycle > 0.

        (* Slot offset is less then cycle *)
        Lemma Offset_lt_cycle:
          Task_slot_offset < TDMA_cycle.

        (* 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 + task_time_slot task TDMA_cycle.

      End BasicLemmas.

    End TimeSlot.

    (* In this section, we prove that no two tasks share the same time slot at any time. *)
    Section InTimeSlotUniq.

      (* Consider any TDMA slot assignment for these tasks *)
      Variable task_time_slot: TDMA_slot Task.

      (* Assume that slot order is total... *)
      Hypothesis slot_order_total:

      (*..., antisymmetric... *)
      Hypothesis slot_order_antisymmetric:

      (*... 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:
         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 .

      (* 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 tsk1 task_time_slot t
        Task_in_time_slot tsk2 task_time_slot t
        tsk1 = tsk2.

    End InTimeSlotUniq.

  End PropertiesTDMA.

End PolicyTDMA.