Library prosa.classic.analysis.uni.susp.dynamic.jitter.jitter_taskset_generation

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.priority prosa.classic.model.suspension.
Require Import prosa.classic.model.arrival.basic.arrival_sequence.
Require Import prosa.classic.model.schedule.uni.jitter.schedule.
Require Import prosa.classic.analysis.uni.susp.dynamic.jitter.jitter_schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq.

Module JitterTaskSetGeneration.

  Import UniprocessorScheduleWithJitter Suspension Priority
         JitterScheduleConstruction.

  Section GeneratingTaskset.

    Context {Task: eqType}.

    Variable ts: seq Task.

    Variable original_task_cost: Task → time.
    Variable task_suspension_bound: Task → time.

    Variable higher_eq_priority: FP_policy Task.

    Variable tsk_i: Task.

    Let other_hep_task tsk_other := higher_eq_priority tsk_other tsk_i && (tsk_other != tsk_i).

    Definition inflated_task_cost (tsk: Task) :=
      if tsk == tsk_i then
        original_task_cost tsk + task_suspension_bound tsk
      else original_task_cost tsk.

    Variable R: Task → time.

    Definition task_jitter (tsk: Task) :=
      if other_hep_task tsk then
        R tsk - original_task_cost tsk
      else 0.

  End GeneratingTaskset.

End JitterTaskSetGeneration.