Finish(?) SSH example

1 files changed, 2 insertions, 2 deletions

diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index 9d956b6..72304d2 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -145,6 +145,7 @@ The final step of the algorithm entails removing the parts of the formula that c
 
 \camil
 \begin{example}[Properties for an Authentication System]
+	\label{ex:pltl-to-ltl:authentication}
 	Consider again the property from \cref{ex:pltl:authentication-system}, repeated here with less verbose names:
 	$\phi = \square (c \rightarrow \lnot f \Sop s)$.
 	This can be rewritten to a form with only $\Uop$ and $\Sop$:
@@ -254,8 +255,7 @@ The final step of the algorithm entails removing the parts of the formula that c
 		\item $\square\lnot(f \land \psi)$.
 			After an authentication failure, a connection cannot be established without prior authentication success.
 	\end{itemize}
-	We see that the formula is reasonably succinct compared to its PLTL version, $\square(c \rightarrow \lnot f \Sop s)$.
-	Using past modalities was not needed in this case.
+	The resulting LTL formula is reasonably succinct, but is clear that the PLTL formula is easier to construct and understand.
 \end{example}
 
 \erin