Merge pull request #100 from freespek/roberto/minor-fixes-2

Minor fixes (2)

reports/report.tex

@@ -11,6 +11,7 @@
 
 \newcommand{\tth}[1]{\footnote{\textcolor{blue}{#1}}}
 \newcommand{\tbh}[1]{\textsc{\textbf{#1}}}
+\newcommand{\rs}[1]{\footnote{\textcolor{purple}{#1}}}
 
 \title{\vspace{-2em}Technical Report: Exploring Automatic Model-Checking of the Ethereum specification\footnote{%
 		The specifications, scripts, and experimental results can be accessed at: \url{https://github.com/freespek/ssf-mc}}}

reports/spec1.tex

@@ -31,9 +31,9 @@ \subsection{Shape of the Python Specification}
 code. Composite types are defined using the \texttt{pyrsistent} library, which
 provides immutable data structures such as sets and maps.
 
-\paragraph{Functions.} The function definitions are mostly pure functions that
+\paragraph{Functions.} The function definitions are pure functions that
 take some input and return some output -- side-effects are rare and limited to
-auxiliary state when computing the function output. Some functions are
+local state. Some functions are
 (mutually) recursive, as can be seen in Figure~\ref{fig:callgraph}.
 
 \paragraph{Similarities between Python and \tlap{}.} Despite being a programming

reports/spec2.tex

@@ -134,7 +134,7 @@ \subsection{Checking the Specification}
 on top of these graphs.
 
 
-To further evaluate \SpecTwo{}, we fix the block graph --- this way the solver
+To further evaluate \SpecTwo{}, we fix the block graph\footnote{We consider forests, rather than just trees, because the specification allows for that. Specifically, forests can occur when only some of the blocks of a given chain are received by a node. In the specification, the set of blocks received corresponds to the map \texttt{CommonNodeState.view\_blocks}.} --- this way the solver
 only has to reason about voting. We encode three example block graphs: a
 single, linear chain (\texttt{SingleChain}), a minimal forked chain of three
 blocks (\texttt{ShortFork}), and a forest of disconnected chains