Library prosa.analysis.facts.tdma

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

Lemma TDMA_cycle_ge_each_time_slot:
TDMA_cycle ts ≥ task_time_slot task.

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.

    Lemma Offset_add_slot_leq_cycle:
      task_slot_offset ts task + task_time_slot task ≤ TDMA_cycle 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:
      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.