Library prosa.classic.implementation.uni.basic.tdma_rta_example

Require Import prosa.classic.util.all prosa.classic.util.find_seq
               .
Require Import prosa.classic.model.arrival.basic.job
               prosa.classic.model.arrival.basic.arrival_sequence
               prosa.classic.model.schedule.uni.basic.platform_tdma
               prosa.classic.model.arrival.basic.task prosa.classic.model.policy_tdma.
Require Import prosa.classic.model.schedule.uni.schedule prosa.classic.model.schedule.uni.schedulability.
Require Import prosa.classic.model.priority
               prosa.classic.analysis.uni.basic.tdma_rta_theory
               prosa.classic.analysis.uni.basic.tdma_wcrt_analysis.
Require Import prosa.classic.implementation.job prosa.classic.implementation.task
               prosa.classic.implementation.arrival_sequence
               prosa.classic.implementation.uni.basic.schedule_tdma.

From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.

Module ResponseTimeAnalysisExemple.

  Import Job ArrivalSequence UniprocessorSchedule SporadicTaskset Schedulability Priority
         ResponseTimeAnalysisTDMA PolicyTDMA Platform_TDMA.
  Import ConcreteJob ConcreteTask ConcreteArrivalSequence BigOp
         ConcreteSchedulerTDMA WCRT_OneJobTDMA.

  Section ExampleTDMA.

    Context {Job: eqType}.

    Let tsk1 := {| task_id := 1; task_cost := 1; task_period := 16; task_deadline := 15|}.
    Let tsk2 := {| task_id := 2; task_cost := 1; task_period := 8; task_deadline := 5|}.
    Let tsk3 := {| task_id := 3; task_cost := 1; task_period := 9; task_deadline := 6|}.

    Let time_slot1 := 1.
    Let time_slot2 := 4.
    Let time_slot3 := 3.

    Program Let ts := Build_set [:: tsk1; tsk2; tsk3] _.

    Let slot_seq := [::(tsk1,time_slot1);(tsk2,time_slot2);(tsk3,time_slot3)].

    Fact ts_has_valid_parameters:
      valid_sporadic_taskset task_cost task_period task_deadline ts.

    Let arr_seq := periodic_arrival_sequence ts.

    Fact job_arrival_times_are_consistent:
      arrival_times_are_consistent job_arrival arr_seq.

    Definition time_slot task:=
      if task \in (map fst slot_seq) then
      let n:= find (fun tsk ⇒ tsk==task)(map fst slot_seq) in
       nth n (map snd slot_seq) n else 0.

    Fact valid_time_slots:
      ∀ tsk, tsk \in ts →
        is_valid_time_slot tsk time_slot.

    Definition slot_order task1 task2:=
      task_id task1 ≥ task_id task2.

    Let sched:=
      scheduler_tdma job_arrival job_cost job_task arr_seq ts time_slot slot_order.

    Let job_in_time_slot t j:=
      Task_in_time_slot ts slot_order (job_task j) time_slot t.

    Fact slot_order_total:
      slot_order_is_total_over_task_set ts slot_order.

    Fact slot_order_transitive:
      slot_order_is_transitive slot_order.

    Fact slot_order_antisymmetric:
      slot_order_is_antisymmetric_over_task_set ts slot_order.

    Fact respects_TDMA_policy:
      Respects_TDMA_policy job_arrival job_cost job_task arr_seq sched ts time_slot slot_order.

    Fact job_cost_le_task_cost:
      ∀ j : concrete_job_eqType,
      arrives_in arr_seq j →
      job_cost_le_task_cost task_cost job_cost job_task j.

    Let tdma_claimed_bound task:=
      WCRT task_cost time_slot ts task.
    Let tdma_valid_bound task := is_valid_tdma_bound task_deadline task (tdma_claimed_bound task).

    Fact valid_tdma_bounds:
      ∀ tsk, tsk \in ts →
        tdma_valid_bound tsk = true.

    Fact WCRT_le_period:
      ∀ tsk, tsk \in ts →
      WCRT task_cost time_slot ts tsk ≤ task_period tsk.

    Let no_deadline_missed_by :=
      task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched.

    Theorem ts_is_schedulable_by_tdma :
      ∀ tsk, tsk \in ts →
        no_deadline_missed_by tsk.

  End ExampleTDMA.

End ResponseTimeAnalysisExemple.