Commit d6ff7353 authored by's avatar
Browse files

polished code style for wc_trans.v

parent 6914b490
Pipeline #21244 passed with stages
in 3 minutes and 42 seconds
......@@ -27,7 +27,7 @@ Section WCTransformation.
Definition relevant_pstate (reference_time: instant) (s: PState) :=
match s with
| None => false
| Some j' => job_arrival j' <= reference_time
| Some j => job_arrival j <= reference_time
(* In order to patch an idle allocation, we look in the future for another allocation
......@@ -42,10 +42,13 @@ Section WCTransformation.
procedure: given an idle allocation at t, find a job allocation in the future
to swap with. *)
Definition find_swap_candidate (sched : SchedType) (t : instant) :=
let order _ _ := false in (* always take the first result *)
let max_dl := max_deadline_for_jobs_arrived_before t
let order _ _ := false (* always take the first result *)
if search_arg sched (relevant_pstate t) order t max_dl is Some t_swap
let max_dl := max_deadline_for_jobs_arrived_before t
let search_result := search_arg sched (relevant_pstate t) order t max_dl
if search_result is Some t_swap
then t_swap
else t. (* if nothing is found, swap with yourself *)
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