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.
Variable Task: eqType.
Definition TDMA_slot:= Task → duration.
Definition TDMA_slot_order:= rel Task.
End TDMA.
Variable Task: eqType.
Definition TDMA_slot:= Task → duration.
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}.
Variable ts: {set Task}.
Variable slot_order: TDMA_slot_order Task.
Section Relation.
Definition slot_order_is_transitive:= transitive slot_order.
Definition slot_order_is_total_over_task_set :=
total_over_list slot_order ts.
Definition slot_order_is_antisymmetric_over_task_set :=
antisymmetric_over_list slot_order ts.
End Relation.
Section TimeSlot.
Variable task: Task.
Hypothesis H_task_in_ts: task \in ts.
Variable task_time_slot: TDMA_slot Task.
Definition is_valid_time_slot:=
task_time_slot task > 0.
Definition TDMA_cycle:=
\sum_(tsk <- ts) task_time_slot tsk.
Definition Task_slot_offset:=
\sum_(prev_task <- ts | slot_order prev_task task && (prev_task != task)) task_time_slot prev_task.
Definition Task_in_time_slot (t:time):=
((t + TDMA_cycle - (Task_slot_offset)%% TDMA_cycle) %% TDMA_cycle)
< (task_time_slot task).
Section BasicLemmas.
Hypothesis time_slot_positive:
is_valid_time_slot.
Lemma TDMA_cycle_ge_each_time_slot:
TDMA_cycle ≥ task_time_slot task.
Lemma TDMA_cycle_positive:
TDMA_cycle > 0.
Lemma Offset_lt_cycle:
Task_slot_offset < TDMA_cycle.
Lemma Offset_add_slot_leq_cycle:
Task_slot_offset + task_time_slot task ≤ TDMA_cycle.
End BasicLemmas.
End TimeSlot.
Section InTimeSlotUniq.
Variable task_time_slot: TDMA_slot Task.
Hypothesis slot_order_total:
slot_order_is_total_over_task_set.
Hypothesis slot_order_antisymmetric:
slot_order_is_antisymmetric_over_task_set.
Hypothesis slot_order_transitive:
slot_order_is_transitive.
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 .
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}.
Variable ts: {set Task}.
Variable slot_order: TDMA_slot_order Task.
Section Relation.
Definition slot_order_is_transitive:= transitive slot_order.
Definition slot_order_is_total_over_task_set :=
total_over_list slot_order ts.
Definition slot_order_is_antisymmetric_over_task_set :=
antisymmetric_over_list slot_order ts.
End Relation.
Section TimeSlot.
Variable task: Task.
Hypothesis H_task_in_ts: task \in ts.
Variable task_time_slot: TDMA_slot Task.
Definition is_valid_time_slot:=
task_time_slot task > 0.
Definition TDMA_cycle:=
\sum_(tsk <- ts) task_time_slot tsk.
Definition Task_slot_offset:=
\sum_(prev_task <- ts | slot_order prev_task task && (prev_task != task)) task_time_slot prev_task.
Definition Task_in_time_slot (t:time):=
((t + TDMA_cycle - (Task_slot_offset)%% TDMA_cycle) %% TDMA_cycle)
< (task_time_slot task).
Section BasicLemmas.
Hypothesis time_slot_positive:
is_valid_time_slot.
Lemma TDMA_cycle_ge_each_time_slot:
TDMA_cycle ≥ task_time_slot task.
Lemma TDMA_cycle_positive:
TDMA_cycle > 0.
Lemma Offset_lt_cycle:
Task_slot_offset < TDMA_cycle.
Lemma Offset_add_slot_leq_cycle:
Task_slot_offset + task_time_slot task ≤ TDMA_cycle.
End BasicLemmas.
End TimeSlot.
Section InTimeSlotUniq.
Variable task_time_slot: TDMA_slot Task.
Hypothesis slot_order_total:
slot_order_is_total_over_task_set.
Hypothesis slot_order_antisymmetric:
slot_order_is_antisymmetric_over_task_set.
Hypothesis slot_order_transitive:
slot_order_is_transitive.
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 .
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.