From ce01dfe1199d90f75de8825b32c03ee96d7a8f11 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Mon, 2 Dec 2019 12:52:38 +0100
Subject: [PATCH] address spell-checker complaints in behavior module
---
restructuring/behavior/ready.v | 4 ++--
restructuring/behavior/schedule.v | 2 +-
restructuring/behavior/time.v | 6 +++---
3 files changed, 6 insertions(+), 6 deletions(-)
diff --git a/restructuring/behavior/ready.v b/restructuring/behavior/ready.v
index 50b1fd882..90361a662 100644
--- a/restructuring/behavior/ready.v
+++ b/restructuring/behavior/ready.v
@@ -25,7 +25,7 @@ Class JobReady (Job : JobType) (PState : Type)
(** Based on the general notion of readiness, we define what it means to be
backlogged, i.e., ready to run but not executing. *)
Section Backlogged.
- (** Conside any kinds of jobs and any kind of processor state. *)
+ (** Consider any kinds of jobs and any kind of processor state. *)
Context {Job : JobType} {PState : Type}.
Context `{ProcessorState Job PState}.
@@ -79,7 +79,7 @@ Section ValidSchedule.
jobs_must_be_ready_to_execute.
(** Note that we do not explicitly require that a valid schedule satisfies
- jobs_must_arrive_to_execute or completed_jobs_dont_execute because these
+ [jobs_must_arrive_to_execute] or [completed_jobs_dont_execute] because these
properties are implied by jobs_must_be_ready_to_execute. *)
End ValidSchedule.
diff --git a/restructuring/behavior/schedule.v b/restructuring/behavior/schedule.v
index 6801eaf43..cba3f33eb 100644
--- a/restructuring/behavior/schedule.v
+++ b/restructuring/behavior/schedule.v
@@ -6,7 +6,7 @@ Require Export rt.restructuring.behavior.arrival_sequence.
(** Rather than choosing a specific schedule representation up front, we define
the notion of a generic processor state, which allows us to state general
definitions of core concepts (such as "how much service has a job
- received") that work across many possble scenarios (e.g., ideal
+ received") that work across many possible scenarios (e.g., ideal
uniprocessor schedules, schedules with overheads, variable-speed
processors, multiprocessors, etc.).
diff --git a/restructuring/behavior/time.v b/restructuring/behavior/time.v
index 54dd8b230..58fb14fa2 100644
--- a/restructuring/behavior/time.v
+++ b/restructuring/behavior/time.v
@@ -1,8 +1,8 @@
(** * Model of Time *)
(** Prosa is based on a discrete model of time. Thus, time is simply defined by
- the natural numbers. To aid readability, we distinguish between time values
- that represent durations and time values that represent specific
- instants. *)
+ the natural numbers. To aid readability, we distinguish between values of time
+ that represent a duration and values of time that represent a specific
+ instant. *)
Definition duration := nat.
Definition instant := nat.
--
GitLab