From 3335f978b44bf11d9c0163d5e74588e2b9873351 Mon Sep 17 00:00:00 2001
From: Marco Maida <mmaida@mpi-sws.org>
Date: Sat, 7 May 2022 02:18:52 +0200
Subject: [PATCH] Reverted comment
---
model/task/arrival/curves.v | 9 ++++-----
1 file changed, 4 insertions(+), 5 deletions(-)
diff --git a/model/task/arrival/curves.v b/model/task/arrival/curves.v
index 09ac4b036..0544433e9 100644
--- a/model/task/arrival/curves.v
+++ b/model/task/arrival/curves.v
@@ -64,11 +64,10 @@ Section ArrivalCurves.
Definition valid_arrival_curve (num_arrivals : duration -> nat) :=
num_arrivals 0 = 0 /\
monotone leq num_arrivals.
-
- (** Similarly, we say that [max_arrivals] is an upper arrival
- bound for task [tsk] iff, for any interval <<[t1, t2)>>,
- [max_arrivals (t2 - t1)] bounds the number of jobs of [tsk]
- that arrive in that interval. *)
+
+ (** We say that [max_arrivals] is an upper arrival bound for task [tsk]
+ iff, for any interval <<[t1, t2)>>, [max_arrivals (t2 - t1)] bounds the
+ number of jobs of [tsk] that arrive in that interval. *)
Definition respects_max_arrivals (tsk : Task) (max_arrivals : duration -> nat) :=
forall (t1 t2 : instant),
t1 <= t2 ->
--
GitLab