From 3f3fac41866ed17ac90a89283af848467a90b98b Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Mon, 1 Mar 2021 15:19:25 +0100
Subject: [PATCH] add notion `receives_service_at`
---
behavior/service.v | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/behavior/service.v b/behavior/service.v
index 34e89f96a..b4ff0fa7e 100644
--- a/behavior/service.v
+++ b/behavior/service.v
@@ -17,6 +17,10 @@ Section Service.
(** ... and the instantaneous service received by job j at time t. *)
Definition service_at (j : Job) (t : instant) := service_in j (sched t).
+
+ (** We say that a job [j] receives service at time [t] if
+ [service_at j t] is positive. *)
+ Definition receives_service_at (j : Job) (t : instant) := 0 < service_at j t.
(** Based on the notion of instantaneous service, we define the cumulative
service received by job j during any interval from [t1] until (but not
--
GitLab