Commit a63ca8f7 authored by Björn Brandenburg's avatar Björn Brandenburg

make definition of completed_jobs_dont_execute uniform

Make it a statement about scheduled jobs, to match the neighboring
parent 1aa2ea08
......@@ -137,7 +137,7 @@ Section ValidSchedule.
(* ... and whether a job cannot be scheduled after it completes. *)
Definition completed_jobs_dont_execute :=
forall j t, service sched j t <= job_cost j.
forall j t, scheduled_at sched j t -> service sched j t < job_cost j.
(* We say that the schedule is valid iff
- jobs come from some arrival sequence
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