==========================
Modification Documentation
==========================

User Interface
==============

The user interface was modified so that fgets() was called instead of
scanf(). This has the benefit that it does not rely on the undefined
behaviour of calling fflush(stdin), and doesn't allow the various
buffers used in the program to be overflowed by malicious users. It
has the disadvantage that backspace is entered as a character rather
than being parsed by the function.

Functions Implemented
=====================

travel
------
	main() (modified)

citystk (given functionality implemented)
-------
	newStack()
	push()
	pop()
	isEmpty()

cityroutes (created)
----------
	isIn() -- is a city in the path?
	path_distance() -- how long is the path?
	connected() -- are two cities connected?
	shortest_path() -- what is the shortest path between a and b?
		(no, you can't rename this straight_line())
	add_steps() -- add all the steps you can add to the given path
		that don't cause a loop
	take_step() -- backtrack to the start of the most recent noted
		step, and take it.

Both add_steps() and take_step() are assistant functions for
shortest_path(), and are probably not useful elsewhere.

isIn() is the obligatory token effort towards conformance with the
given MaimingConvention. I'll follow it properly when I start getting
paid to write this stuff, or when it's mentioned explicitly mentioned
as a requirement in the assignment sheet.

Debugging Facilities
====================

Compile with the DEBUG option to enable debugging code to be
exectued. Compile with the NDEBUG option to disable assertion
checking. Compiling with both or neither defined may be entertaining,
but is probably not something you want to try straight after eating.

============================================
Design and Implementation of shortest_path() 
============================================

The shortest_path() functions implements a depth first search of the
cities defined by the City type with the following algorithm:

   1) We first create a path beginning at the source city, but not
      going anywhere, and initialize the stack of untaken steps to
      empty.

   2a) If the path ends at the destination city, we have a possible
       solution. We note down and return the shortest of these
       solutons, by recording each solution iff it is the shortest so
       far, and returning the most recently noted solution.
 
   2b) If the path doesn't end at our final destination, we note down
       every connecting city (every step we can make), if there are
       any. 

   3a) If there are some steps noted down for us to look at, we
       examine the most recent: returning to the city it left, and
       then, taking the step, moving to the city it entered. Having
       done so, we return to step 2a/b).

   3b) If there aren't any steps left for us to look at, we're done.

It should not be called if the source and destination are one and the
same, nor if there is no route between them. (See connected())

Why does this work?
===================

State Invariants
----------------

Denote the array of visited cities by [v1,v2,...,vn], and the set of
untaken steps by [s1,s2,...,sk]. If s is some step, s.from is the city
departed on that step, and s.to is the city entered, denoted by the
ordered pair, s=(s.from, s.to).

There are some state invariants, that are always true after step 1:
   a) The first city in the path is the source:
	n >= 1, v1 = source
   b) There are no loops in the path:
	(vx = vy) ==> (x = y)

Define a function f(c) = x defined on all the cities included in the
path, where the value at a city is that city's position in the path.  

   c) Each step in the path is valid:
	for all 1 <= i < n, vi is connected to v(i+1)
   d) All the untaken steps are valid:
	for all 1 <= i <= k, si.to and si.from are valid cities, and
	are connected.  
   e) The from of each untaken step is still on our path:
	for all 1 <= i <= k, and for some 1 <= x <= n, si.from = vx 
   f) Taking any untaken step won't cause a loop:
	for all 1 <= i <= k, si.to not in path or f(si.from)<f(si.to)
   g) The untaken steps are in order:
	for all 1 <= i < j <= k, f(si.from) <= f(sj.from)	
   h) No untaken step occurs twice
	(si = sj) ==> (i = j) 


The Invariants Don't Vary!
--------------------------

It is easy to verify that all of these invariants are satisfied after
(1).


2a) We have a solution: the path is a valid path (each city is
reachable from the city immediately prior by (c)), it begins at the
source (a), ends at the destination, and contains no loops (b). We do
not actually change v or s at all in this case, so our invariants
trivially remain.


2b) In this case we add s(k+1)...sk' to the list of untaken
steps. (a), (b) and (c) remain trivially; (d), (e), (f) remain true by
construction; (g) and (h) require a little proof, however:
	Divide s1...sk' into two sets, s1...sk and s(k+1)...sk'.

	if i,j are both <= k, (g) and (h) are true by assumption.

	if i,j are both > k, f(si.from) = f(sj.from) = n (g),
		and si.to = sj.to only if i=j (h), by construction.

	otherwise i <= k < j. f(si.from) <= n = f(sj.from) by
		definition of f(), giving (g). The step before (2b)
		was either (1), in which case there were no prior
		steps (ie, there is no such i) or (3a), in which case
		just before stage (3a), step si was earlier than the
		step (v(n-1), vn) which was taken in stage (3a), and
		thus, f(si.from) <= f(v(n-1)) = n-1 < n, and hence
		si.from and sj.from are different, so (h) remains. 
So in each case, (g) and (h) remain.


3a) After this operation, the set of visited cities becomes
[v1,...,v(f(sk.from)),vn'=sk.to], and the set of steps becomes
[s1,...,s(k-1)].

By (e), f(sk.from) >= 1, so (a) remains. By (f), (b) remains, and by
(d), (c) remains. Since no steps are added, (d) remains. By (g), for
each 1<=i<k, f(si.from)<=f(sk.from), so (e) holds, since all cities as
early in the path as sk.from remain in the path. Since no steps were
added, (f), (g) and (h) remain.


3b) Does not change the state, but does make a strong claim: that all
possible solutions have been checked.

We show this by taking an arbitrary path, denoted [u1,...,um] from the
source to the destination, and showing that at some point it occurs
after stage (3). We do this by induction on each step in that path.

Proposition(m'): the path [u1,...,um'] occurs after stage (2), and
before stage (3), and, if m'<m, after execution of stage (3),
(um',u(m'+1)) is one of the untaken steps.

Proposition(1): Initially the path is set to [u1]. If 1<m, u1 is
different to um (otherwise there would be a loop in the path), in
which case all the steps from u1, including (u1,u2) is included in the
list of untaken steps by step (2b).

Proposition(m'+1): At the point of Proposition(m') becoming true, we
have [u1,...,um'] as our unvisited cities, and (um', u(m'+1)) as one
of the unvisited steps. Processing of the algorithm proceeds without
modifying any of the first m' entries in the path, as otherwise (e)
would be violated. When the step (um', u(m'+1)) is taken at (3) (and
all steps are taken by the time (3b) is reached), then, backtracking
to um' will give [u1,...,um',u(m'+1)] as the path. If m'+1<m, then the
algorithm will proceed to (2b), and note down the step
(u(m'+1),u(m'+2)) as untaken.

By the Principle of Mathematical Induction, the path [u1,...,um] is
covered if (3b) is reached.

Termination
===========

The only remaining question is whether the algorithm terminates.

Since there are a finite number of cities, and loops are not allowed,
then if the algorithm does not terminate at some point a path that has
previously occured will occur again (in fact, this would have to
happen infinitely often, although only countably so).

We will consider the state of the algorithm between stages (3) and (2)
taking the first path that repeats (if it does, in fact, exist),
called [u1,...,u,v], and the behaviour of the algorithm between
this path's first ocurrence, and it's second.

If we set time t1 to be the point in the algorithm between (3) and (2)
where the path first occurs, t1-1 to be the point just earlier, before
(3) is executed, and t2 to be the point in the algorithm between (3)
and (2) where the path occurs for the second time, and t2-1 to be,
similarly, the point just earlier, before (3) is executed.

Then at t1-1, the stack contains exactly one instance of the (u,v)
step (by (h)) and this is the last step. At time t1, when this step is
taken, there is no step (u,v) in the list of untaken steps. At time
t2-1, however there is an occurence of the step (u,v) in the list.

How did this get there? Evidently the city u was considered in stage
(2b), between times t1 and t2-1. But if this was the case, then either
between steps (3a) and (2b) we had a loop, namely: [u1,...,u,v,...,u];
or we backtracked past u -- in which case we either stopped at u, or
later (and before t2-1), we had to build back up past u so that when
later we backtracked to u and added v at t2-1, we obtained the
original path). In either case, though, our original path was not the
first such path that repeated -- [u1,...,u] was! 

We have thus obtained a contradiction. Hence no path ever repeats, and
the algorithm terminates.

Implementation Considerations
=============================

While it's all find and dandy to have a proof that the algorithm
works, it's even nicer to know that what you typed bears more than a
passing resemblence to the algorithm. As such, a number of assertions
verifying some of these invariants were added to the code.

--
Anthony Towns
24 August 1997