From: SeongJae Park <sj38.park@xxxxxxxxx>
A few sentences in ppcmem.tex are using lowercase 's' for Spin, while
other sentences in other tex files are using the uppercase 'S'.
Consistently use uppercase 'S'.
Signed-off-by: SeongJae Park <sj38.park@xxxxxxxxx>
---
formal/ppcmem.tex | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/formal/ppcmem.tex b/formal/ppcmem.tex
index 9f584b15..62a45383 100644
--- a/formal/ppcmem.tex
+++ b/formal/ppcmem.tex
@@ -7,7 +7,7 @@
%
\epigraph{Jack of all trades, master of none.}{Unknown}
-Although Promela and spin allow you to verify pretty much any (smallish)
+Although Promela and Spin allow you to verify pretty much any (smallish)
algorithm, their very generality can sometimes be a curse.
For example, Promela does not understand memory models or any sort
of reordering semantics.
@@ -403,7 +403,7 @@ These tools do have some intrinsic limitations:
running on small numbers of threads.
Larger examples result
in state-space explosion, just as with similar tools such as
- Promela and spin.
+ Promela and Spin.
\item The full state-space search does not give any indication of how
each offending state was reached.
That said, once you realize that the state is in fact reachable,
--
2.17.1
