Library prosa.classic.analysis.uni.susp.sustainability.allcosts.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
prosa.classic.model.schedule.uni.susp.platform
prosa.classic.model.schedule.uni.susp.build_suspension_table.
Require Import prosa.classic.model.schedule.uni.transformation.construction.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq bigop fintype.
Module SustainabilityAllCosts.
Import ScheduleWithSuspensions Suspension Priority PlatformWithSuspensions
ScheduleConstruction SuspensionTableConstruction.
Section Reduction.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Require Import prosa.classic.model.priority prosa.classic.model.suspension.
Require Import prosa.classic.model.schedule.uni.susp.schedule
prosa.classic.model.schedule.uni.susp.platform
prosa.classic.model.schedule.uni.susp.build_suspension_table.
Require Import prosa.classic.model.schedule.uni.transformation.construction.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq bigop fintype.
Module SustainabilityAllCosts.
Import ScheduleWithSuspensions Suspension Priority PlatformWithSuspensions
ScheduleConstruction SuspensionTableConstruction.
Section Reduction.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Basic Setup & Setting
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.
Definition of the Reduction
Variable inflated_job_cost: Job → time.
Variable j: Job.
Let arr_j := job_arrival j.
Variable R: time.
(A) Schedule Construction
Section ScheduleConstruction.
Section ConstructionStep.
Variable sched_prefix: schedule Job.
Variable t: time.
Let arrivals := jobs_arrived_up_to arr_seq t.
Let job_is_pending := pending job_arrival inflated_job_cost sched_prefix.
Definition job_is_late any_j t :=
service sched_prefix any_j t
< service sched_susp any_j t + (inflated_job_cost any_j - job_cost any_j).
Section ConstructionStep.
Variable sched_prefix: schedule Job.
Variable t: time.
Let arrivals := jobs_arrived_up_to arr_seq t.
Let job_is_pending := pending job_arrival inflated_job_cost sched_prefix.
Definition job_is_late any_j t :=
service sched_prefix any_j t
< service sched_susp any_j t + (inflated_job_cost any_j - job_cost any_j).
(A.1) The prefix is built in a way that prevents jobs from getting late.
Section Prefix.
Definition jobs_that_are_late_or_scheduled_in_sched_susp :=
[seq any_j <- arrivals | job_is_pending any_j t &&
(job_is_late any_j t || scheduled_at sched_susp any_j t)].
Definition highest_priority_late_job :=
seq_min (higher_eq_priority t) jobs_that_are_late_or_scheduled_in_sched_susp.
End Prefix.
Definition jobs_that_are_late_or_scheduled_in_sched_susp :=
[seq any_j <- arrivals | job_is_pending any_j t &&
(job_is_late any_j t || scheduled_at sched_susp any_j t)].
Definition highest_priority_late_job :=
seq_min (higher_eq_priority t) jobs_that_are_late_or_scheduled_in_sched_susp.
End Prefix.
(A.2) In the suffix, we just pick the highest-priority pending job
so that the schedule constraints are satisfied.
Section Suffix.
Definition pending_jobs :=
[seq any_j <- arrivals | job_is_pending any_j t ].
Definition highest_priority_job :=
seq_min (higher_eq_priority t) pending_jobs.
End Suffix.
Definition pending_jobs :=
[seq any_j <- arrivals | job_is_pending any_j t ].
Definition highest_priority_job :=
seq_min (higher_eq_priority t) pending_jobs.
End Suffix.
(A.3) In the end, we just combine the prefix and suffix schedules.
Definition build_schedule :=
if t < arr_j + R then
highest_priority_late_job
else
highest_priority_job.
End ConstructionStep.
Let empty_schedule : schedule Job := fun t ⇒ None.
Definition sched_new :=
build_schedule_from_prefixes build_schedule empty_schedule.
End ScheduleConstruction.
if t < arr_j + R then
highest_priority_late_job
else
highest_priority_job.
End ConstructionStep.
Let empty_schedule : schedule Job := fun t ⇒ None.
Definition sched_new :=
build_schedule_from_prefixes build_schedule empty_schedule.
End ScheduleConstruction.
(B) Definition of Suspension Times
Section DefiningSuspension.
Let job_is_suspended_in_sched_susp :=
suspended_at job_arrival job_cost job_suspension_duration sched_susp.
Definition suspended_in_sched_new (any_j: Job) (t: time) :=
(t < arr_j + R) && job_is_suspended_in_sched_susp any_j t
&& ~~ job_is_late sched_new any_j t.
Definition reduced_suspension_duration :=
build_suspension_duration sched_new (arr_j + R) suspended_in_sched_new.
End DefiningSuspension.
End Reduction.
End SustainabilityAllCosts.