Library prosa.classic.model.schedule.uni.workload
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.time prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.arrival_sequence
prosa.classic.model.priority.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module Workload.
Import Time ArrivalSequence Priority.
Section WorkloadDefs.
Context {Task: eqType}.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → Task.
Variable arr_seq: arrival_sequence Job.
Variable jobs: seq Job.
Section WorkloadOfJobs.
Variable P: Job → bool.
Definition workload_of_jobs := \sum_(j <- jobs | P j) job_cost j.
End WorkloadOfJobs.
Section PerTaskPriority.
Variable higher_eq_priority: FP_policy Task.
Variable tsk: Task.
Let of_higher_or_equal_priority j :=
higher_eq_priority (job_task j) tsk.
Definition workload_of_higher_or_equal_priority_tasks :=
workload_of_jobs of_higher_or_equal_priority.
End PerTaskPriority.
Section PerJobPriority.
Variable higher_eq_priority: JLFP_policy Job.
Variable j: Job.
Let of_higher_or_equal_priority j_hp := higher_eq_priority j_hp j.
Definition workload_of_higher_or_equal_priority_jobs :=
workload_of_jobs of_higher_or_equal_priority.
End PerJobPriority.
End WorkloadDefs.
Section TaskWorkload.
Context {Task: eqType}.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → Task.
Variable arr_seq: arrival_sequence Job.
Variable tsk: Task.
Let of_task_tsk j := job_task j == tsk.
Definition task_workload jobs := workload_of_jobs job_cost jobs of_task_tsk.
Definition task_workload_between (t1 t2: time) :=
task_workload (jobs_arrived_between arr_seq t1 t2).
End TaskWorkload.
Section BasicLemmas.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable arr_seq: arrival_sequence Job.
Let arrivals_between := jobs_arrived_between arr_seq.
Lemma workload_of_jobs_cat:
∀ t t1 t2 P,
t1 ≤ t ≤ t2 →
workload_of_jobs job_cost (arrivals_between t1 t2) P =
workload_of_jobs job_cost (arrivals_between t1 t) P
+ workload_of_jobs job_cost (arrivals_between t t2) P.
End BasicLemmas.
End Workload.
Require Import prosa.classic.model.time prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.arrival_sequence
prosa.classic.model.priority.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module Workload.
Import Time ArrivalSequence Priority.
Section WorkloadDefs.
Context {Task: eqType}.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → Task.
Variable arr_seq: arrival_sequence Job.
Variable jobs: seq Job.
Section WorkloadOfJobs.
Variable P: Job → bool.
Definition workload_of_jobs := \sum_(j <- jobs | P j) job_cost j.
End WorkloadOfJobs.
Section PerTaskPriority.
Variable higher_eq_priority: FP_policy Task.
Variable tsk: Task.
Let of_higher_or_equal_priority j :=
higher_eq_priority (job_task j) tsk.
Definition workload_of_higher_or_equal_priority_tasks :=
workload_of_jobs of_higher_or_equal_priority.
End PerTaskPriority.
Section PerJobPriority.
Variable higher_eq_priority: JLFP_policy Job.
Variable j: Job.
Let of_higher_or_equal_priority j_hp := higher_eq_priority j_hp j.
Definition workload_of_higher_or_equal_priority_jobs :=
workload_of_jobs of_higher_or_equal_priority.
End PerJobPriority.
End WorkloadDefs.
Section TaskWorkload.
Context {Task: eqType}.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → Task.
Variable arr_seq: arrival_sequence Job.
Variable tsk: Task.
Let of_task_tsk j := job_task j == tsk.
Definition task_workload jobs := workload_of_jobs job_cost jobs of_task_tsk.
Definition task_workload_between (t1 t2: time) :=
task_workload (jobs_arrived_between arr_seq t1 t2).
End TaskWorkload.
Section BasicLemmas.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable arr_seq: arrival_sequence Job.
Let arrivals_between := jobs_arrived_between arr_seq.
Lemma workload_of_jobs_cat:
∀ t t1 t2 P,
t1 ≤ t ≤ t2 →
workload_of_jobs job_cost (arrivals_between t1 t2) P =
workload_of_jobs job_cost (arrivals_between t1 t) P
+ workload_of_jobs job_cost (arrivals_between t t2) P.
End BasicLemmas.
End Workload.