>From c313894cb1f877b1d8ef5303d59d97b187cf925e Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@xxxxxxxxx>
Date: Tue, 31 Oct 2017 00:48:11 +0900
Subject: [PATCH] formal/regression: Fix typo
Signed-off-by: Akira Yokosawa <akiyks@xxxxxxxxx>
---
Hi Paul,
Here are fixes of several typos in the new section.
There are chances I'm guessing wrong in some of the hunks, though.
Thanks, Akira
--
formal/regression.tex | 10 +++++-----
1 file changed, 5 insertions(+), 5 deletions(-)
diff --git a/formal/regression.tex b/formal/regression.tex
index 39ca388..09d28e1 100644
--- a/formal/regression.tex
+++ b/formal/regression.tex
@@ -60,7 +60,7 @@ and C++ code, but these tools work only on very small litmus tests,
which normally means that you must extract the core of your
mechanism---by hand.
As with Promela and \co{spin}, both PPCMEM and \co{herd} are
-extremely useful, but they are well-suited for regression suites.
+extremely useful, but they are not well-suited for regression suites.
In contrast, \co{cbmc} and Nidhugg can input C programs of reasonable
(though still quite limited) size, and if their capabilities continue
@@ -394,7 +394,7 @@ Worse yet, imagine another software artifact with one bug that fails
once every day on average and 24 more that fail every million years
each.
Suppose that a formal-verification tool located the 24 million-year
-bugs, but failed to fined the one-day bug.
+bugs, but failed to find the one-day bug.
Fixing the 24 bugs located will take time and effort, likely slightly
decrease reliability, and do nothing at all about the pressing
each-day failure that is likely causing much embarrassment and perhaps
@@ -479,7 +479,7 @@ Despite requiring hand translation, Promela handles assertions
in a natural way, so its fifth cell is green.
PPCMEM usually requires hand translation due to the small size of litmus
-tests that it support, so its first cell is orange.
+tests that it supports, so its first cell is orange.
It accurately handles several memory models, so its second cell is green.
Its overhead is quite high, so its third cell is red.
It provides a graphical display of relations among operations, which
@@ -493,7 +493,7 @@ so \co{herd}'s first cell is also orange.
It supports a wide variety of memory models, so its second cell is blue.
It has reasonable overhead, so its third cell is yellow.
Its bug-location and assertion capabilities are quite similar to those
-of \co{cbmc}, so \co{herd} gets the same color for the next two cells.
+of PPCMEM, so \co{herd} gets the same color for the next two cells.
The \co{cbmc} tool inputs C code directly, so its first cell is blue.
It supports a few memory models, so its second cell is yellow.
@@ -515,7 +515,7 @@ so they are all yellow with question marks.
Once again, please note that this table rates these tools for use in
regression testing.
-Just because many of them area poor fit for regression testing does
+Just because many of them are poor fit for regression testing does
not at all mean that they are useless, in fact,
many of them have proven their worth many times over.
Just not for regression testing.
--
2.7.4
--
To unsubscribe from this list: send the line "unsubscribe perfbook" in
the body of a message to majordomo@xxxxxxxxxxxxxxx
More majordomo info at http://vger.kernel.org/majordomo-info.html
