Fix diagram

1 files changed, 5 insertions, 5 deletions

diff --git a/verilog.tex b/verilog.tex
index 8c63b86..9b67118 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -57,13 +57,13 @@ In addition to adding support for two-dimensional arrays, support for receiving
   \centering
   \begin{minipage}{1.0\linewidth}
     \begin{gather*}
-      \inferrule[Module]{\Gamma_{r} ! s_{t} = \texttt{Some } v \\ (m_{i}, \Gamma_{r}^{0}, \Gamma_{a}^{0}, \epsilon, \epsilon\ l)\ \longrightarrow_{\vec{m}} (m_{i}, \Gamma_{r}^{1}, \Gamma_{a}^{1}, \Delta_{r}^{1}, \Delta_{a}^{1}) \\ (\Gamma_{r}^{1} // \Delta_{r}^{1}) ! s_{t} = \texttt{Some } v'}{\texttt{State } \textit{sf }\ m\ v\ \Gamma_{r}^{0}\ \Gamma_{a}^{0} \longrightarrow \texttt{State } \textit{sf }\ m\ v'\ (\Gamma_{r}^{1} // \Delta_{r}^{1})\ (\Gamma_{a}^{1} // \Delta_{a}^{1})}\\
+      \inferrule[Module]{\Gamma_{r} ! s_{t} = \yhconstant{Some } v \\ (m_{i}, \Gamma_{r}^{0}, \Gamma_{a}^{0}, \epsilon, \epsilon\ l)\ \longrightarrow_{\vec{m}} (m_{i}, \Gamma_{r}^{1}, \Gamma_{a}^{1}, \Delta_{r}^{1}, \Delta_{a}^{1}) \\ (\Gamma_{r}^{1}\ //\ \Delta_{r}^{1}) ! s_{t} = \yhconstant{Some } v'}{\yhconstant{State } \textit{sf }\ m\ v\ \Gamma_{r}^{0}\ \Gamma_{a}^{0} \longrightarrow \yhconstant{State } \textit{sf }\ m\ v'\ (\Gamma_{r}^{1}\ //\ \Delta_{r}^{1})\ (\Gamma_{a}^{1}\ //\ \Delta_{a}^{1})}\\
       %
-      \inferrule[Finish]{\Gamma_{r}!\textit{fin} = \texttt{Some } 1 \\ \Gamma_{r}!\textit{ret} = \texttt{Some } r}{\texttt{State } \textit{sf }\ m\ s_{t}\ \Gamma_{r}\ \Gamma_{a} \longrightarrow \texttt{Returnstate } \textit{sf }\ r}\\
+      \inferrule[Finish]{\Gamma_{r}!\textit{fin} = \yhconstant{Some } 1 \\ \Gamma_{r}!\textit{ret} = \yhconstant{Some } r}{\yhconstant{State } \textit{sf }\ m\ s_{t}\ \Gamma_{r}\ \Gamma_{a} \longrightarrow \yhconstant{Returnstate } \textit{sf }\ r}\\
       %
-      \inferrule[Call]{ }{\texttt{Callstate } []\ m\ \vec{r} \longrightarrow \texttt{State } []\ m\ n\ (\textit{init\_params }\ \vec{r}\ a // \{s_{t} \rightarrow n\})}\\
+      \inferrule[Call]{ }{\yhconstant{Callstate } \textit{sf}\ m\ \vec{r} \longrightarrow \yhconstant{State } \textit{sf}\ m\ n\ (\yhfunction{init\_params}\ \vec{r}\ a\ //\ \{s_{t} \rightarrow n\})}\\
       %
-      \inferrule[Return]{ }{\texttt{Returnstate } (\texttt{Stackframe } r\ m\ \textit{pc }\ \Gamma_{r}\ \Gamma_{a} :: \textit{sf}) \longrightarrow \texttt{State } \textit{sf }\ m\ \textit{pc }\ (\Gamma_{r} // \{ \textit{st} \rightarrow \textit{pc}, r \rightarrow i \})\ \epsilon}
+      \inferrule[Return]{ }{\yhconstant{Returnstate } (\yhconstant{Stackframe } r\ m\ \textit{pc }\ \Gamma_{r}\ \Gamma_{a} :: \textit{sf}) \longrightarrow \yhconstant{State } \textit{sf }\ m\ \textit{pc }\ (\Gamma_{r}\ //\ \{ \textit{st} \rightarrow \textit{pc}, r \rightarrow i \})\ \epsilon}
     \end{gather*}
   \end{minipage}
   \caption{Inferrence rules for modules}%
@@ -87,7 +87,7 @@ However, as Verilog behaves quite differently to software programming languages,
   \item[stack] The function stack can be modelled as a RAM using a two-dimensional array in the module, denoted as \textit{stk}.
 \end{description}
 
-Figure~\ref{fig:inferrence_module}
+Figure~\ref{fig:inferrence_module} shows the inferrence rules that convert from one state to another.  The first thing to note is that there is no step from \texttt{State}
 
 %~\NR{Isn't the 'main' addition that the PL community may not have seen the always blocks? It can be counter-intuitive to them. Also have you intentionally avoided assign statements? Finally, what is $\epsilon$ in the syntax?}\YH{Yes, I will probably have to explain always blocks some more, I'll try and add a paragraph about them.  Yes, assign statements are quite complex to model and many semantics do not model them.  They are also not needed for translation.  The $\epsilon$ is an empty skip statement, which is just a semicolon.}