        \problemdata       % Takes 5 *mandatory* arguments
        {spantree-algorithm}             % latex-friendly label for the prob.
        {state machines}  % The topic(s) of the problem content.
        {}               % Source (if known)
        {F01 PS6-2} % Usage (list ones you are aware of).
        {}        % Last revision info (author, date).


\begin{problem}

The algorithm $Mark$ starts with a connected, undirected graph $G =
(V,E)$, with all edges unmarked.  Then it proceeds to mark some of the
edges, by repeatedly performing the following steps:
\begin{enumerate}
\item {\bf Choose} any edge $e \in E$ such that there is currently no path of
marked edges between the endpoints of $e$.
\item {\bf Mark} edge $e$.
\end{enumerate}
Prove that the algorithm finishes and that when it finishes, the set
of marked edges forms a spanning tree of the input graph $G$. (A {\em
spanning tree} of $G$ is a tree whose edges are a subset of the set
$E$ of edges of $G$, and that contains an edge incident on every
vertex of $G$.)

\solution{ We will need to show that the marked edges form a
spanning tree of G ({\em i.e.} they form an acyclic graph and touch
every vertex of G), {\em and} that the algorithm does indeed finish.

\begin{description}

\item[Marked edges form an acyclic graph:]

Use the Invariant Theorem:

{\bf Invariant:} The marked edges form an acyclic graph. 
\begin{description}
\item[Start condition:] Initial state.  
Initially all edges are unmarked, so there are no cycles consisting of
marked edges. 

\item[Step condition:] Consider a step $(q,q')$, where we assume that
there are no cycles consisting of marked edges in state $q$.  We show
that the same condition holds in state $q'$.

In this step, the algorithm marks an edge $e$ for which there was
previously no marked path between its endpoints.  This means that,
after the step, there is exactly one marked path between the endpoints
of $e$.  Thus, the new edge is not part of a cycle, in the new state
$q'$.  This means that there are still no cycles in state $q'$.
\end{description}

\item[Marked edges touch every vertex of G:] We can show this by
noticing that if $(v, w)$ is an edge in G then there is a path of
marked edges from $v$ to $w$. If there wasn't, then $(v, w)$ would
become a candidate edge because its endpoints are not connected by
marked edges. Then $(v,w)$ would itself be marked and thus $v$ and $w$
are indeed connected by marked edges.

Now we need to show that every vertex is touched by a marked edge. For
contradiction, suppose there is some vertex $v$ in G that is not
touched by any marked edges.  However, G is connected, so there must
be at least one $(v,w)$ edge in G. Since this edge exists, $v$ and $w$
must be connected by marked edges, so $v$ must indeed be touched by a
marked edge. Contradiction.

\item[Algorithm terminates:] 
This is shown because once an edge is marked, it can never be
unmarked. Since we have a finite set of edges, and every transition
necessarily marks one edge, we will eventually run out of candidate edges
and the algorithm will terminate.

%[[[We must also show that when no rule can be applied, it must be the
%case that the marked edges form a spanning tree of $G$.
%Shishir?  Prove this?  The following lines appeared in the previous
%solution, but they don't look like a convincing proof to me.
%
%``Since the for-loop loops over all the edges then all the vertices of
%$G$ (that have edges) will be contained in the forest.''
%
%Basically, we have to argue that, if we reach a point where no further
%steps are enabled (a ``final state''), then any two nodes are
%connected by some path of marked edges.
%I think that this probably will use a lemma saying, in a final state,
%if $(v,w)$ is an edge of $G$ then there is a path of marked edges from
%v to w.
%Then apply this lemma in an inductive proof to show that any two nodes
%of $G$ (which are assumed to be connected in $G$ by SOME path), are
%connected in the final state by a path of marked edges.
%Probably could avoid the induction by using some kind of transitive
%closure result.
%]]]
%
\end{description}
}


\end{problem}