From a63ca8f79bf06b9a892e8b74b355b395306e5e48 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Tue, 20 Aug 2019 22:16:33 +0200
Subject: [PATCH] make definition of completed_jobs_dont_execute uniform
Make it a statement about scheduled jobs, to match the neighboring
definitions.
---
restructuring/behavior/schedule.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/restructuring/behavior/schedule.v b/restructuring/behavior/schedule.v
index 6f93d73b4..b61d05cbd 100644
--- a/restructuring/behavior/schedule.v
+++ b/restructuring/behavior/schedule.v
@@ -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
--
GitLab