# Library prosa.model.schedule.tdma

From mathcomp Require Import div.
Require Export prosa.util.seqset.
Require Export prosa.util.rel.

# TDMA Scheduling

The TDMA scheduling 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
```

## Task Parameter for TDMA Scheduling

We define the TDMA policy as follows.
Section TDMAPolicy.

With each task, we associate the duration of the corresponding TDMA slot.

Moreover, within each TDMA cycle, task slots are ordered according to some relation (i.e, slot_order slot1 slot2 means that slot1 comes before slot2 in a TDMA cycle).

End TDMAPolicy.

We introduce slots and the slot order as task parameters.

## TDMA Policy Validity

First, we define the properties of a valid TDMA policy.
Section ValidTDMAPolicy.

...and a TDMA policy.

Time slot order must be transitive...
..., totally ordered over the task set...
Definition total_slot_order :=
total_over_list slot_order ts.

... and antisymmetric over task set.
A valid time slot must be positive

## TDMA Cycles, Sots, and Offsets

In this section, we define key TDMA concepts.

...and a TDMA policy.

We define the TDMA cycle as the sum of all the tasks' time slots
Definition TDMA_cycle:=

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.
The following function tests whether a task is in its time slot at instant t.

## TDMA Schedule Validity

Section TDMASchedule.

Context {PState : ProcessorState Job}.
Context {ja : JobArrival Job} {jc : JobCost Job}.

Consider any job arrival sequence...
Variable arr_seq : arrival_sequence Job.

..., any schedule ...
Variable sched : schedule PState.