From 8e5aba27f3a68f3ac4e8ff2dcc8c2fdd0fd5b0b8 Mon Sep 17 00:00:00 2001
From: Kimaya Bedarkar <kbedarka@mpi-sws.org>
Date: Wed, 19 Mar 2025 10:10:23 +0000
Subject: [PATCH] Apply 6 suggestion(s) to 1 file(s)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
Co-authored-by: Björn Brandenburg <bbb@mpi-sws.org>
---
analysis/facts/model/ideal_uni_exceed.v | 18 +++++++++---------
1 file changed, 9 insertions(+), 9 deletions(-)
diff --git a/analysis/facts/model/ideal_uni_exceed.v b/analysis/facts/model/ideal_uni_exceed.v
index b30a00b3c..b1268dfde 100644
--- a/analysis/facts/model/ideal_uni_exceed.v
+++ b/analysis/facts/model/ideal_uni_exceed.v
@@ -24,9 +24,9 @@ Section ExceedanceProcStateProperties.
(** A job [j] is said to be [scheduled_at] some time [t] if and only if the
processor state at that time is [NominalExecution j] or
[ExceedanceExecution j]. *)
- Lemma scheduled_at_procstate (sched : schedule (exceedance_proc_state Job)) j t:
- scheduled_at sched j t <->
- sched t = NominalExecution j \/ sched t = ExceedanceExecution j.
+ Lemma scheduled_at_procstate (sched : schedule (exceedance_proc_state Job)) j t :
+ scheduled_at sched j t <->
+ sched t = NominalExecution j \/ sched t = ExceedanceExecution j.
Proof.
split.
- move => SCHED.
@@ -46,7 +46,7 @@ Section ExceedanceProcStateProperties.
(** Next we prove that the processor model under consideration is a uniprocessor
- model i.e., only one job can be scheduled at any time instant. *)
+ model, i.e., only one job can be scheduled at any time instant. *)
Lemma eps_is_uniproc : uniprocessor_model (exceedance_proc_state Job).
Proof.
rewrite /uniprocessor_model.
@@ -63,7 +63,7 @@ Section ExceedanceProcStateProperties.
Qed.
(** Next, we prove that the processor model under consideration is fully
- consuming i.e., all the supply offered is consumed by the scheduled job. *)
+ consuming, i.e., all the supply offered is consumed by the scheduled job. *)
Lemma eps_is_fully_consuming :
fully_consuming_proc_model (exceedance_proc_state Job).
Proof.
@@ -81,7 +81,7 @@ Section ExceedanceProcStateProperties.
Qed.
(** Finally we prove that the processor model under consideration is unit
- service i.e., it provides at most one unit of service at any time instant. *)
+ service, i.e., it provides at most one unit of service at any time instant. *)
Lemma eps_is_unit_service : unit_service_proc_model (exceedance_proc_state Job).
Proof.
rewrite /unit_service_proc_model.
@@ -97,7 +97,7 @@ End ExceedanceProcStateProperties.
ideal uniprocessor with exceedance processor state. *)
Section ExceedanceProcStateProperties1.
- (** In this section we consider any type of jobs. *)
+ (** In this section, we consider any type of jobs. *)
Context `{Job : JobType}.
(** First let us define the notion of exceedance execution. A processor state
@@ -105,8 +105,8 @@ Section ExceedanceProcStateProperties1.
[ExceedanceExecution j] for some [j]. *)
Definition is_exceedance_exec (pstate : (exceedance_proc_state Job)) :=
match pstate with
- |ExceedanceExecution _ => true
- |_ => false
+ | ExceedanceExecution _ => true
+ | _ => false
end.
Local Transparent scheduled_in scheduled_on service_on.
--
GitLab