\chapter{Further Worked Examples}
\label{Further_Worked_Examples}
\section{The Seven Bridges of K\"{o}nigsberg}
In this section, we will show a special case where Alloy can be used to \emph{prove} that a puzzle has no solution. 

\setcounter{footnote}{8}

\subsection{The Problem}
The city of K\"{o}nigsberg, Prussia (now Kaliningrad, Russia) is set on the river Pregel (now Pregoyla). The river divides, creating two large islands which in the eighteenth century were connected to each other and the mainland by seven bridges\footnote{Picture taken from \htmladdnormallink{http://en.wikipedia.org/wiki/Image:7\_bridges.svg}{http://en.wikipedia.org/wiki/Image:7\_bridges.svg}}:

\begin{figure}[htp]
\centering
\includegraphics[width=0.5\textwidth]{Koenigsberg.jpg}
\caption{The Seven Bridges of K\"{o}nigsberg}
\end{figure}

It had become a challenge amongst the citizens to see if anyone could walk around the town, crossing each bridge once and only once. Nobody seemed to be able to find such a path and in 1735, Euler proved that the task was impossible. His proof is now considered to be the first theorem of graph theory\footnote{cf. \cite{sautoy04} p. 43, \cite{agnarsson06} p. 2f., \htmladdnormallink{http://en.wikipedia.org/wiki/Seven\_Bridges\_of\_Koenigsberg}{http://en.wikipedia.org/wiki/Seven\_Bridges\_of\_Koenigsberg}}.

\subsection{Using Alloy To Show No Solution Exists}
To model the K\"{o}nigsberg bridge problem in Alloy, we first introduce signatures representing the four landmasses as in the picture above. 

\begin{code}
	\begin{alltt}
		\highlight{abstract} \highlight{sig} Landmass \{\}
		\highlight{one} \highlight{sig} N, E, S, W \highlight{extends} Landmass \{\}
	\end{alltt}
\end{code}

Here, \highlight{one} specifies that the signatures N, E, S and W are \emph{singleton}, i.e. that there is exactly one `instance' of each of them. \newline

For encoding the bridges, we introduce \texttt{Bridge}:

\begin{code}
	\begin{alltt}
		\highlight{abstract} \highlight{sig} Bridge \{ connects: \highlight{set} Landmass \} \{	#connects = 2 \}
	\end{alltt}
\end{code}

The second pair of curly brackets after the field declarations of a signature above is an example of an \emph{appended fact}. This is equivalent to:

\begin{code}
	\begin{alltt}
		\highlight{abstract} \highlight{sig} Bridge \{ connects: \highlight{set} Landmass \} 
		\highlight{fact} \{ all b:Bridge | #connects = 2 \}
	\end{alltt}
\end{code}

Note that we have chosen to model the two landmasses that a bridge connects by a set rather than by a relation or two fields of type \texttt{Landmass}. This makes it easier to reflect the fact that bridges can be traversed in both directions. \newline

Modelling the actual bridges is straightforward: 

\begin{code}
	\begin{alltt}
		\highlight{one} \highlight{sig} Bridge1 \highlight{extends} Bridge \{\} \{ connects = N + W \}
		\highlight{one} \highlight{sig} Bridge2 \highlight{extends} Bridge \{\} \{ connects = N + W \}
		\highlight{one} \highlight{sig} Bridge3 \highlight{extends} Bridge \{\} \{ connects = N + E \}
		\highlight{one} \highlight{sig} Bridge4 \highlight{extends} Bridge \{\} \{ connects = E + W \}
		\highlight{one} \highlight{sig} Bridge5 \highlight{extends} Bridge \{\} \{ connects = E + S \}
		\highlight{one} \highlight{sig} Bridge6 \highlight{extends} Bridge \{\} \{ connects = S + W \}
		\highlight{one} \highlight{sig} Bridge7 \highlight{extends} Bridge \{\} \{ connects = S + W \}
	\end{alltt}
\end{code}

Next, we need to be able to represent a \texttt{Path} across bridges: 

\begin{code}
	\begin{alltt}
		\begin{tabbing}
			\highlight{sig} Path \{ firstStep: Step \}\\
			\highlight{sig}\= Step \=\{\\
			\>	from, to: Landmass, \\
			\>	via: Bridge, \\
			\>	nextStep: \highlight{lone} Step\\
			\} \{ via.connects = from + to \}\\
			\highlight{fact} \{\\
			\>	\highlight{all} curr:Step, next:curr.nextStep |\\
			\>	\>	next.from = curr.to\\
			\}
		\end{tabbing}
	\end{alltt}
\end{code}

(This might remind you of the \texttt{Queue} model in section \ref{Statics_I}!) There are two constraints on a path and its steps: First, each step over a bridge has to start at one side of the bridge and end on its other side. Second, the destination of the current step is the start of the next. \newline

Finally, we want Alloy to find a path that crosses all bridges: 

\begin{code}
	\begin{alltt}
		\begin{tabbing}
			\highlight{fun}\= steps (p:Path): set Step \{\\
			\>	p.firstStep.*nextStep\\
			\}\\

			\highlight{pred} path() \{\\
			\>	\highlight{some} p:Path | steps[p].via = Bridge\\
			\}
		\end{tabbing}
	\end{alltt}
\end{code}

But how do we ensure that the path crosses each bridge \emph{exactly once}? Well, if each of the seven bridges is crossed exactly once, then the path will consist of seven steps provided each step actually crosses a bridge. As this is implicit from our model (you are encouraged to check this by using an assertion and finding out why!), it is enough to constrain the scope to 7:

\begin{code}
	\begin{alltt}
		\highlight{run} path \highlight{for} 7 \highlight{but} \highlight{exactly} 1 Path
	\end{alltt}
\end{code}

This shows that the Koenigsberg Bridge Problem has no solution! (Mathematically, the problem can be translated to graph theory by viewing the land masses as nodes and the bridges as edges of a graph. Euler proved the general result that for there to be a path that visits each edge exactly once either all, or all but two vertices must have an even number of vertices connected to them (such a path is now called an \emph{Eulerian path}). As this is not the case for the landmasses and bridges of K\"{onigsberg}, there cannot be such a path.) 

\section{Modelling Memory in Object-Z and Alloy}
In this section, we will show how Object-Z and Alloy can be used to model the same example\footnote{This example was taken from \cite{russo}. }. 

\subsection{The Problem}
We will be modelling a computer store that associates addresses with the values at the respective addresses in the store. To be as general as possible, both addresses and values will be represented as \emph{words}. We will also define a function \emph{lookup} which returns the value associated with a particular address in the store. 

\subsection{The Solution In Object-Z}
We have already seen the solution to the first part in section \ref{Question_Look_Up} (p. \pageref{Question_Look_Up}): 

\begin{figure}[h!]
		\begin{center}
			\includegraphics[scale=0.6]{Store_Q5.jpg}
		\end{center}
\end{figure}

\texttt{store} is defined as a finite subset of the cartesian product $WORD \times WORD$ and can thus be seen as a binary relation. The axiom of the schema then further constrains it to be a partial function, i.e. it ensures that each address maps to at most one value. \newline

Having defined the state schema for the store, we now define the operation schema for \texttt{lookup}: 

	\begin{figure}[h!]
		\begin{center}
		\includegraphics[scale=0.75]{Look_Up.jpg}
		\end{center}
	\end{figure}

The variable \texttt{address} is followed by \texttt{?} to indicate it is an input variable. Similarly, \texttt{value} is followed by \texttt{!} to indicate it is an output variable. $\Xi Store$ indicates that the state of the store is not affected by the operation. Finally, the single axiom ensures that our function returns the correct value associated with the given address in the store. 

\subsection{The Solution In Alloy}
As before, if you have already answered question 2 in section \ref{Question_Look_Up}, this might seem familiar: 

	\begin{code}
		\begin{alltt}
			\begin{tabbing}
			\highlight{one} \highlight{sig} Store \{ store: Word -> \highlight{lone} Word \} \\
			\highlight{sig} Word \{\}\end{tabbing}\end{alltt}
	\end{code}

Just as in the state schema above, \texttt{store} is a relation mapping each \texttt{Word} to at most one other \texttt{Word}. Thanks to the simpler syntax of Alloy, the Alloy model is much more concise than the corresponding schemas. There is just one thing that is implicit in the schemas which we have to specify explicitly in the Alloy model: that there is exactly \highlight{one} \texttt{Store}. \newline

Now on to the lookup function!

	\begin{code}
		\begin{alltt}
			\highlight{fun} lookup(address:Word) : Word \{ address.(Store.store) \}
		\end{alltt}
	\end{code}

Here, we specify that \texttt{lookup} takes \texttt{address} as an argument and returns the value it is associated with in the store. \newline

Notice that Alloy will quietly swallow the error if we give the function a bad input. In Object-Z, we would have to allow for bad inputs by use of pre-conditions or by handling exceptions.
