formalregress.tex is using \co{} for spin in most cases. Use it always
for better consistency.
Signed-off-by: SeongJae Park <[email protected]>
---
future/formalregress.tex | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/future/formalregress.tex b/future/formalregress.tex
index a50df4ad..b1a39b29 100644
--- a/future/formalregress.tex
+++ b/future/formalregress.tex
@@ -155,7 +155,7 @@ testing, which is in fact the topic of this section.
It is critically important that formal-verification tools correctly
model their environment.
One all-too-common omission is the memory model, where a great
-many formal-verification tools, including Promela/spin, are
+many formal-verification tools, including Promela/\co{spin}, are
restricted to \IXh{sequential}{consistency}.
The QRCU experience related in
\cref{sec:formal:Is QRCU Really Correct?}
@@ -359,7 +359,7 @@ What is needed is a tool that gives at least \emph{some}
information
as to where the bug is located and the nature of that bug.
The \co{cbmc} output includes a traceback mapping back to the source
-code, similar to Promela/spin's, as does Nidhugg.
+code, similar to Promela/\co{spin}'s, as does Nidhugg.
Of course, these tracebacks can be quite long, and analyzing them
can be quite tedious.
However, doing so is usually quite a bit faster
--
2.17.1
