From c6204c35949efabd583847f4cbf68f12521431ff Mon Sep 17 00:00:00 2001
From: Thomas Pani <thomas.pani@gmail.com>
Date: Mon, 16 Dec 2024 15:41:29 +0100
Subject: [PATCH] Two small fixes to the Alloy section

---
 reports/spec3-alloy.tex | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/reports/spec3-alloy.tex b/reports/spec3-alloy.tex
index 5de6a88..f73d78b 100644
--- a/reports/spec3-alloy.tex
+++ b/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 {