Library prosa.analysis.facts.tdma

From mathcomp Require Import div.
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
Thus, a TDMA cycle is always positive
    Lemma TDMA_cycle_positive:
      TDMA_cycle ts > 0.

Slot offset is less then cycle
    Lemma Offset_lt_cycle:
      task_slot_offset ts task < TDMA_cycle ts.

For a task, the sum of its slot offset and its time slot is less then or equal to cycle.
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 .

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.

  End TimeSlotOrderFacts.

End TDMAFacts.