Library rt.restructuring.model.schedule.tdma.tdma_facts
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.
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.