Commit 62c5aa23 authored by Marco Maida's avatar Marco Maida 🌱
Browse files

Added delta-min theory (to discuss)

parent 109324ac
Pipeline #36703 failed with stages
in 17 minutes and 5 seconds
......@@ -28,11 +28,11 @@ Class MinArrivals (Task : TaskType) := min_arrivals : Task -> duration -> nat.
maximum-distance functions. *)
(** We let [min_separation tsk N] denote the minimal length of an interval in
which exactly [N] jobs of task [tsk] arrive. *)
which at least [N] jobs of task [tsk] arrive. *)
Class MinSeparation (Task : TaskType) := min_separation : Task -> nat -> duration.
(** Conversely, we let [max_separation tsk N] denote the maximal length of an interval in
which exactly [N] jobs of task [tsk] arrive. *)
which at most [N] jobs of task [tsk] arrive. *)
Class MaxSeparation (Task : TaskType) := max_separation : Task -> nat -> duration.
......
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment