Library prosa.classic.model.schedule.uni.basic.platform_tdma

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.task
                prosa.classic.model.arrival.basic.job prosa.classic.model.priority
                prosa.classic.model.arrival.basic.task_arrival
                prosa.classic.model.schedule.uni.schedule.
Require Import prosa.classic.model.policy_tdma.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.

Module Platform_TDMA.

  Import Job UniprocessorSchedule div.
  Export PolicyTDMA.

  Section Properties.

    Context {sporadic_task: eqType}.
    Context {Job: eqType}.
    Variable job_arrival: Job → time.
    Variable job_cost: Job → time.
    Variable job_deadline: Job → time.
    Variable job_task: Job → sporadic_task.

    Variable arr_seq: arrival_sequence Job.

    Variable sched: schedule Job.

    Variable ts: {set sporadic_task}.

    Variable time_slot: TDMA_slot sporadic_task.

    Variable slot_order: TDMA_slot_order sporadic_task.

    Let job_in_time_slot (job:Job) (t:instant):=
        Task_in_time_slot ts slot_order (job_task job) time_slot t.

    Definition sched_implies_in_slot j t:=
      (scheduled_at sched j t → job_in_time_slot j t).

    Definition backlogged_implies_not_in_slot_or_other_job_sched j t:=
      (backlogged job_arrival job_cost sched j t →
        ¬ job_in_time_slot j t ∨
        (∃ j_other, arrives_in arr_seq j_other∧
                         job_arrival j_other < job_arrival j∧
                         job_task j = job_task j_other∧
                         scheduled_at sched j_other t)).

    Definition Respects_TDMA_policy:=
      ∀ (j:Job) (t:time),
        arrives_in arr_seq j →
        sched_implies_in_slot j t ∧ backlogged_implies_not_in_slot_or_other_job_sched j t.

  End Properties.

End Platform_TDMA.