From 00a1ec2842bcc0d94e0b395b05d40cf483f1661d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Fri, 28 Feb 2025 09:42:55 +0100
Subject: [PATCH] fix `t = 0` cornercase in definition of `completes_at`
This definition isn't actually used anywhere important, maybe it's
time to get rid of it.
---
behavior/service.v | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/behavior/service.v b/behavior/service.v
index 507ecddc6..6b7dd9e0a 100644
--- a/behavior/service.v
+++ b/behavior/service.v
@@ -43,8 +43,9 @@ Section Service.
Definition completed_by (j : Job) (t : instant) := service j t >= job_cost j.
(** We say that job [j] completes at time [t] if it has completed by time [t] but
- not by time [t - 1]. *)
- Definition completes_at (j : Job) (t : instant) := ~~ completed_by j t.-1 && completed_by j t.
+ not by time [t - 1] (or if [t == 0]). *)
+ Definition completes_at (j : Job) (t : instant) :=
+ (~~ completed_by j t.-1 || (t == 0)) && completed_by j t.
(** We say that a constant [R] is a response time bound of a job [j] if [j]
has completed by [R] units after its arrival. *)
--
GitLab