Library prosa.classic.model.policy_tdma
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.time
prosa.classic.model.arrival.basic.task
prosa.classic.model.arrival.basic.job.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div.
Module PolicyTDMA.
Import Time.
Require Import prosa.classic.model.time
prosa.classic.model.arrival.basic.task
prosa.classic.model.arrival.basic.job.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div.
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.
(* 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:
is_valid_time_slot.
(* 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:
slot_order_is_total_over_task_set.
(*..., antisymmetric... *)
Hypothesis slot_order_antisymmetric:
slot_order_is_antisymmetric_over_task_set.
(*... and transitive. *)
Hypothesis slot_order_transitive:
slot_order_is_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.
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:
is_valid_time_slot.
(* 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:
slot_order_is_total_over_task_set.
(*..., antisymmetric... *)
Hypothesis slot_order_antisymmetric:
slot_order_is_antisymmetric_over_task_set.
(*... and transitive. *)
Hypothesis slot_order_transitive:
slot_order_is_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.