Library prosa.classic.analysis.uni.susp.sustainability.singlecost.reduction

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.priority prosa.classic.model.suspension.
Require Import prosa.classic.model.schedule.uni.susp.schedule.
Require Import prosa.classic.model.schedule.uni.transformation.construction.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq.

Module SustainabilitySingleCost.

  Import ScheduleWithSuspensions Suspension Priority ScheduleConstruction.

  Section Reduction.

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

    Variable arr_seq: arrival_sequence Job.

    Variable higher_eq_priority: JLDP_policy Job.

    Variable sched_susp: schedule Job.

    Variable job_suspension_duration: job_suspension Job.

    Variable j: Job.

    Variable inflated_job_cost: Job → time.

    Section ScheduleConstruction.

      Section ConstructionStep.

        Variable sched_prefix: schedule Job.
        Variable t: time.

        Let job_is_pending := pending job_arrival inflated_job_cost sched_prefix.
        Let job_is_suspended :=
          suspended_at job_arrival inflated_job_cost job_suspension_duration sched_prefix.
        Let actual_job_arrivals_up_to := jobs_arrived_up_to arr_seq.

        Let job_is_ready j t := job_is_pending j t && ~~ job_is_suspended j t.

        Definition ready_jobs :=
          [seq j_other <- actual_job_arrivals_up_to t | job_is_ready j_other t].

        Definition highest_priority_job := seq_min (higher_eq_priority t) ready_jobs.

        Definition build_schedule : option Job :=
          if highest_priority_job is Some j_hp then
            if sched_susp t is Some j_in_susp then
              if job_is_ready j_in_susp t && higher_eq_priority t j_in_susp j_hp then
                Some j_in_susp
              else
                Some j_hp
            else Some j_hp
          else None.

      End ConstructionStep.

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

      Definition sched_susp_highercost :=
        build_schedule_from_prefixes build_schedule empty_schedule.

    End ScheduleConstruction.

  End Reduction.

End SustainabilitySingleCost.