Library rt.restructuring.model.task_cost
From rt.restructuring.behavior Require Export arrival_sequence.
From rt.restructuring.model Require Export task.
Section TaskCost.
Context {T : TaskType}.
Variable (task_cost : duration).
Definition valid_task_cost := task_cost > 0.
End TaskCost.
(* Definition of a generic type of parameter for task cost *)
Class TaskCost (T : TaskType) := task_cost : T → duration.
Section TasksetCosts.
Context {T : TaskType} `{TaskCost T}.
Variable ts : seq T.
Definition valid_taskset_costs :=
∀ tsk : T,
tsk \in ts →
task_cost tsk > 0.
Context {J : JobType} `{JobTask J T} `{JobCost J}.
Variable arr_seq : arrival_sequence J.
Definition respects_taskset_costs :=
∀ j,
arrives_in arr_seq j →
job_cost j ≤ task_cost (job_task j).
End TasksetCosts.
From rt.restructuring.model Require Export task.
Section TaskCost.
Context {T : TaskType}.
Variable (task_cost : duration).
Definition valid_task_cost := task_cost > 0.
End TaskCost.
(* Definition of a generic type of parameter for task cost *)
Class TaskCost (T : TaskType) := task_cost : T → duration.
Section TasksetCosts.
Context {T : TaskType} `{TaskCost T}.
Variable ts : seq T.
Definition valid_taskset_costs :=
∀ tsk : T,
tsk \in ts →
task_cost tsk > 0.
Context {J : JobType} `{JobTask J T} `{JobCost J}.
Variable arr_seq : arrival_sequence J.
Definition respects_taskset_costs :=
∀ j,
arrives_in arr_seq j →
job_cost j ≤ task_cost (job_task j).
End TasksetCosts.