Library prosa.classic.model.schedule.uni.susp.platform
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.arrival_sequence prosa.classic.model.suspension
prosa.classic.model.priority.
Require Import prosa.classic.model.schedule.uni.susp.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module PlatformWithSuspensions.
Export ScheduleWithSuspensions Priority.
Section Definitions.
Context {Task: eqType}.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → Task.
Variable next_suspension: job_suspension Job.
Variable arr_seq: arrival_sequence Job.
Variable sched: schedule Job.
Let job_pending_at := pending job_arrival job_cost sched.
Let job_scheduled_at := scheduled_at sched.
Let job_backlogged_at := backlogged job_arrival job_cost next_suspension sched.
Section ScheduleConstraints.
Section Execution.
Definition work_conserving :=
∀ j t,
arrives_in arr_seq j →
job_backlogged_at j t →
∃ j_other, job_scheduled_at j_other t.
End Execution.
Section FP.
Variable higher_eq_priority: FP_policy Task.
Definition respects_FP_policy :=
∀ j j_hp t,
arrives_in arr_seq j →
job_backlogged_at j t →
job_scheduled_at j_hp t →
higher_eq_priority (job_task j_hp) (job_task j).
End FP.
Section JLFP.
Variable higher_eq_priority: JLFP_policy Job.
Definition respects_JLFP_policy :=
∀ j j_hp t,
arrives_in arr_seq j →
job_backlogged_at j t →
job_scheduled_at j_hp t →
higher_eq_priority j_hp j.
End JLFP.
Section JLDP.
Variable higher_eq_priority: JLDP_policy Job.
Definition respects_JLDP_policy :=
∀ j j_hp t,
arrives_in arr_seq j →
job_backlogged_at j t →
job_scheduled_at j_hp t →
higher_eq_priority t j_hp j.
End JLDP.
End ScheduleConstraints.
End Definitions.
End PlatformWithSuspensions.
Require Import prosa.classic.model.arrival.basic.arrival_sequence prosa.classic.model.suspension
prosa.classic.model.priority.
Require Import prosa.classic.model.schedule.uni.susp.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module PlatformWithSuspensions.
Export ScheduleWithSuspensions Priority.
Section Definitions.
Context {Task: eqType}.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → Task.
Variable next_suspension: job_suspension Job.
Variable arr_seq: arrival_sequence Job.
Variable sched: schedule Job.
Let job_pending_at := pending job_arrival job_cost sched.
Let job_scheduled_at := scheduled_at sched.
Let job_backlogged_at := backlogged job_arrival job_cost next_suspension sched.
Section ScheduleConstraints.
Section Execution.
Definition work_conserving :=
∀ j t,
arrives_in arr_seq j →
job_backlogged_at j t →
∃ j_other, job_scheduled_at j_other t.
End Execution.
Section FP.
Variable higher_eq_priority: FP_policy Task.
Definition respects_FP_policy :=
∀ j j_hp t,
arrives_in arr_seq j →
job_backlogged_at j t →
job_scheduled_at j_hp t →
higher_eq_priority (job_task j_hp) (job_task j).
End FP.
Section JLFP.
Variable higher_eq_priority: JLFP_policy Job.
Definition respects_JLFP_policy :=
∀ j j_hp t,
arrives_in arr_seq j →
job_backlogged_at j t →
job_scheduled_at j_hp t →
higher_eq_priority j_hp j.
End JLFP.
Section JLDP.
Variable higher_eq_priority: JLDP_policy Job.
Definition respects_JLDP_policy :=
∀ j j_hp t,
arrives_in arr_seq j →
job_backlogged_at j t →
job_scheduled_at j_hp t →
higher_eq_priority t j_hp j.
End JLDP.
End ScheduleConstraints.
End Definitions.
End PlatformWithSuspensions.