1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278
|
(***********************************************************************)
(* *)
(* FaCiLe *)
(* A Functional Constraint Library *)
(* *)
(* Nicolas Barnier, Pascal Brisset, LOG, CENA *)
(* *)
(* Copyright 2004 CENA. All rights reserved. This file is distributed *)
(* under the terms of the GNU Lesser General Public License. *)
(***********************************************************************)
(* $Id: scheduling.ml,v 1.4 2004/08/12 15:31:52 barnier Exp $ *)
open Facile
open Easy
module Task = struct
type t = {
start : Fd.t;
end_time : Arith.t;
processing_time : int;
name : string ;
id : int
}
let gen_int = Misc.gen_int_fun ()
let create ?(name = "") s p = {
start = s;
end_time = fd2e s +~ i2e p;
processing_time = p;
name = name;
id = gen_int ()
}
let id a = a.id
let name a = a.name
let start a = a.start
let end_time a = a.end_time
let release_date a = Fd.min a.start
let processing_time a = a.processing_time
let deadline a = Fd.max a.start + a.processing_time
let update_release_date a x =
let s = a.start in
match Fd.value s with
Unk attra -> Fd.refine s (Domain.remove_low x (Var.Attr.dom attra))
| Val v -> if x > v then Stak.fail "Scheduling.Task.update_release_date"
let update_deadline a x =
let s = a.start in
match Fd.value s with
Unk attra ->
Fd.refine s
(Domain.remove_up (x - a.processing_time) (Var.Attr.dom attra))
| Val v ->
if x < v + a.processing_time then
Stak.fail "Scheduling.Task.update_deadline"
let end_time_bounds a = Arith.min_max_of_expr a.end_time
let fprint_end_time c a =
let (mi, ma) = end_time_bounds a in
if mi = ma then Printf.fprintf c "%d" mi
else Printf.fprintf c "[%d-%d]" mi ma
let before a1 a2 = a1.end_time <=~ fd2e a2.start
let after a1 a2 = before a2 a1
let fprint c a =
Printf.fprintf c "%a -- %d --> %a\n"
Fd.fprint a.start a.processing_time fprint_end_time a
end
type t = Task.t array
let fprint f s = Array.iter (Task.fprint f) s
let create = Array.of_list
let tasks = Array.to_list
let iter = Array.iter
let number_of_tasks = Array.length
(* Edge Finding *)
(* From Constraint-Based Scheduling, page 24 *)
(*
[cc] maximal minimal end time
[c.(i)] maximal minimal end time of A_j that come after A-i
[pp] sum of processing times
*)
module T = Task
let compare_release_dates a a' = compare (T.release_date a) (T.release_date a')
let update_r a =
let n = Array.length a in
(* First sort {A_1,...,A_n} ascending release dates *)
Array.sort compare_release_dates a;
(* Check first if it is globally consistent *)
try
for i = 1 to n - 1 do
if T.release_date a.(i) < T.deadline a.(i-1) then raise Exit done;
true
with Exit -> (* Copy release_dates in [r] and do updates directly in [a] *)
let r = Array.map T.release_date a in (* 1..3 *)
let c = Array.create n 0 in
for k = 0 to n-1 do (* 4..29 *)
let pp = ref 0
and cc = ref min_int in
let dk = T.deadline a.(k) in
for i = n-1 downto 0 do (* 6..15 *)
let di = T.deadline a.(i)
and pi = Task.processing_time a.(i) in
if di <= dk then begin
pp := !pp + pi;
cc := max !cc (r.(i) + !pp);
if !cc > dk then Stak.fail "Scheduling.update_r" end;
c.(i) <- !cc done;
let hh = ref min_int in
for i = 0 to n-1 do (* 16..28 *)
let di = T.deadline a.(i)
and pi = T.processing_time a.(i) in
if di <= dk then begin (* 17..19 *)
hh := max !hh (r.(i) + !pp);
pp := !pp - pi end
else begin (* 20..26 *)
if r.(i) + !pp + pi > dk then T.update_release_date a.(i) c.(i);
if !hh + pi > dk then T.update_release_date a.(i) !cc end
done
done;
false (* Check is done at the beginning of update *)
let compare_deadlines a a' = compare (T.deadline a) (T.deadline a')
let update_d a =
let n = Array.length a in
(* First sort {A_1,...,A_n} asscending deadline dates *)
Array.sort compare_deadlines a;
(* Check done ONLY in update_r *)
(* Copy deadlines in [d] and do updates directly in [a] *)
let d = Array.map T.deadline a in (* 1..3 *)
let c = Array.create n 0 in
for k = n-1 downto 0 do (* 4..29 *)
let pp = ref 0
and cc = ref max_int in
let rk = T.release_date a.(k) in
for i = 0 to n-1 do (* 6..15 *)
let ri = T.release_date a.(i)
and pi = Task.processing_time a.(i)
in
if ri >= rk then begin
pp := !pp + pi;
cc := min !cc (d.(i) - !pp);
if !cc < rk then Stak.fail "Scheduling.update_d" end;
c.(i) <- !cc done;
let hh = ref max_int in
for i = n-1 downto 0 do (* 16..28 *)
let ri = T.release_date a.(i)
and pi = T.processing_time a.(i)
in
if ri >= rk then begin (* 17..19 *)
hh := min !hh (d.(i) - !pp);
pp := !pp - pi end
else begin (* 20..26 *)
if d.(i) - (!pp + pi) < rk then T.update_deadline a.(i) c.(i);
if !hh - pi < rk then T.update_deadline a.(i) !cc end
done
done;
false (* Check is done at the beginning of update *)
let edge_finding = fun a ->
let update _ = update_r a || update_d a
and delay ct =
Array.iter
(fun a ->
Fd.delay [Var.Fd.on_min; Var.Fd.on_max] (Task.start a) ct) a
and priority = Cstr.later
and name = "Scheduling.edge_finding" in
Cstr.create ~priority ~name update delay
let disjunctive2 a1 a2 =
let update _ =
T.release_date a2 >= T.deadline a1 ||
let p1p2 = T.processing_time a1 + T.processing_time a2 in
if T.release_date a2 + p1p2 > T.deadline a1 then begin
(* a2 cannot be before a1 *)
Cstr.post (fd2e (T.start a2) >=~ T.end_time a1);
true end
else false
and delay ct =
Fd.delay [Var.Fd.on_max] (Task.start a1) ct;
Fd.delay [Var.Fd.on_min] (Task.start a2) ct
and priority = Cstr.later
and name = "Scheduling.disjunctive2" in
Cstr.create ~priority ~name update delay
let disjunctive a =
let n = Array.length a and c = ref Cstr.one in
for i = 0 to n - 1 do
for j = 0 to n - 1 do
if i <> j then c := Reify.(&&~~) !c (disjunctive2 a.(i) a.(j))
done done;
!c
module Goals = struct
let rank s =
let n = Array.length s
and s = Array.copy s in (* We will swap elements *)
let swap i j = let tmp = s.(i) in s.(i) <- s.(j); s.(j) <- tmp
and arg_smallest_release_date i =
let value j =
(T.release_date s.(j),
T.deadline s.(j) - T.processing_time s.(j),
T.id s.(j)) in
let best = ref i in
for j = i+1 to n-1 do if value j < value !best then best := j done;
!best
and is_first i () =
let endsi = Task.end_time s.(i) in
for j = i + 1 to n - 1 do (* Others start after *)
Cstr.post (fd2e (Task.start s.(j)) >=~ endsi) done
and is_not_first i () =
if i = n-1 then Stak.fail "Scheduling.Goals.rank.is_not_first";
let minimal_end_time_of_another =
FdArray.min
(Array.map
(fun a -> Arith.e2fd (T.end_time a))
(Array.sub s (i+1) (n-i-1))) in
(***Printf.printf "%a >= %a\n" Fd.fprint (Task.start s.(i)) Fd.fprint minimal_end_time_of_another; flush stdout; ***)
Cstr.post
(fd2e (Task.start s.(i)) >=~ fd2e minimal_end_time_of_another) in
(***
let rec rank i =
Goals.create
(fun i ->
(***Printf.printf "rank %d: \n" i;
fprint stdout s; ***)
if i < n then
let j = arg_smallest_release_date i in
(*** Printf.printf "i=%d j=%d\n" i j; ***)
swap i j;
Goals.(||~)
(Goals.(&&~) (Goals.atomic (is_first i)) (rank (i+1)))
(Goals.(&&~) (Goals.atomic (is_not_first i)) (rank i))
else begin
(***fprint stdout s; ***)
Goals.success end)
i in
rank 0
***)
let swap_bt i j () =
if i <> j then begin
let tmp = s.(i) in
s.(i) <- s.(j); s.(j) <- tmp;
Stak.trail (fun () -> swap i j) end in
(*
let another_first i j () =
let latest_start_j = T.deadline s.(j) - T.processing_time s.(j) in
try
for i = i to n - 1 do
if i <> j && T.release_date s.(i) + T.processing_time s.(i) <= latest_start_j then raise Exit done;
Stak.fail "Scheduling.Goals.another_first"
with Exit -> () in
*)
let rec rank i i' = (* i' is the smallest which can be selected first *)
Goals.create
(fun i ->
if i < n then
if i' < n then
let j = arg_smallest_release_date i' in
(Goals.atomic (swap_bt i j)
&&~ Goals.atomic (is_first i)
&&~ rank (i+1) (i+1))
||~
(Goals.atomic (swap_bt i' j)
&&~ Goals.atomic (is_not_first i')
&&~ rank i (i'+1))
else Stak.fail "Scheduling.Goals.rank"
else Goals.success)
i in
rank 0 0
end
|