Merge pull request #96 from freespek/th/fix-allow-sec

Two small fixes to the Alloy section

reports/spec3-alloy.tex

@@ -1,6 +1,6 @@
 %! TeX root = report.tex
 
-\section{\SpecThreeB{} in Alloy}\label{sec:alloy}
+\section{\SpecThreeC{} in Alloy}\label{sec:alloy}
 
 Once we saw that our specifications~\SpecThree{} and~\SpecFour{}
 were too challenging for the \tlap{} tools, we decided to employ
@@ -49,9 +49,10 @@ \subsection{From \tlap{} to Alloy}
   one sig GenesisBlock extends Block {}
 \end{lstlisting}
 
-In contrast to~\SpecThree{}, our Alloy specification does not describe a
-state machine, but it specifies an arbitrary single state of the protocol. As
-in~\SpecThree{}, we compute the set of justified checkpoints as a fixpoint:
+Unlike~\SpecThree{} but similar to~\SpecThreeB{}, our Alloy specification does
+not describe a state machine, but it specifies an arbitrary single state of the
+protocol. As in~\SpecThree{}, we compute the set of justified checkpoints as a
+fixpoint:
 
 \begin{lstlisting}[language=alloy,columns=fullflexible]
   one sig JustifiedCheckpoints {