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

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.model.schedule.uni.transformation.construction.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq.

Module JitterScheduleConstruction.

  Import UniprocessorScheduleWithJitter Suspension Priority ScheduleConstruction.

  Section ConstructingJitterSchedule.

    Context {Task: eqType}.
    Context {Job: eqType}.
    Variable job_arrival: Job → time.
    Variable job_task: Job → Task.

    Variable arr_seq: arrival_sequence Job.

    Variable higher_eq_priority: FP_policy Task.
    Let job_higher_eq_priority := FP_to_JLFP job_task higher_eq_priority.

    Variable job_cost: Job → time.
    Variable task_cost: Task → time.

    Variable job_suspension_duration: job_suspension Job.

    Variable sched_susp: schedule Job.

    Variable j: Job.

    Let arr_j := job_arrival j.
    Let task_of_j := job_task j.

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

    Variable R: Job → time.

    Section DefiningJobParameters.

      Section CostInflation.

        Let job_total_suspension :=
          total_suspension job_cost job_suspension_duration.

        Definition inflated_job_cost (any_j: Job) :=
          if any_j == j then
            job_cost any_j + job_total_suspension any_j
          else
            job_cost any_j.

      End CostInflation.

      Section ConvertingSuspensionToJitter.

        Variable any_j: Job.

        Let distance_to_j := job_arrival j - job_arrival any_j.

        Definition job_jitter :=
          if other_hep_task (job_task any_j) then
            minn distance_to_j (R any_j - job_cost any_j)
          else 0.

      End ConvertingSuspensionToJitter.

    End DefiningJobParameters.

    Section ScheduleConstruction.

      Section ConstructionStep.

        Variable sched_prefix: schedule Job.
        Variable t: time.

        Let job_is_pending := pending job_arrival inflated_job_cost job_jitter sched_prefix.
        Let actual_job_arrivals_up_to := actual_arrivals_up_to job_arrival job_jitter arr_seq.
        Let lower_priority j1 j2 := ~~ job_higher_eq_priority j1 j2.

        Definition pending_jobs_other_than_j :=
          [seq j_other <- actual_job_arrivals_up_to t | job_is_pending j_other t & j_other != j].

        Definition highest_priority_job_other_than_j :=
          seq_min job_higher_eq_priority pending_jobs_other_than_j.

        Definition build_schedule : option Job :=
          if job_is_pending j t then
            if highest_priority_job_other_than_j is Some j_hp then
              if lower_priority j_hp j then
                Some j
              else Some j_hp
            else Some j
          else highest_priority_job_other_than_j.

      End ConstructionStep.

      Let empty_schedule : schedule Job := fun t ⇒ None.

      Definition sched_jitter := build_schedule_from_prefixes build_schedule empty_schedule.

    End ScheduleConstruction.

  End ConstructingJitterSchedule.

End JitterScheduleConstruction.