This is the readme.txt file associated with 
Hoover - Rudnicki, Uniform Self-Stabilizing Orientation of
Unicyclic Networks under Read/Write Atomicity.

This paper relies on the positive results of a state exploration of the token
passing algorithm.  The exploration is implemented by a C program, explore.

To compile and run explore, do the following
	gcc explore.c problem.c -o explore
	explore

To obtain more details from the state space exploration output, uncomment
the statement 
	print_details();
that appears in the body of main in explore.c.

Explore is constructed from the following components:

1. A generic state space exploration module, consisting of explore.c,
explore.h, and some declarations in problem.h

2. A module that is tailored to the problem that is being explored,
consisting of problem.c, and additional declarations in problem.h
This particular one implements the token passing protocol of Section 3 of
the paper.

Details of the components:

explore.c  - implements the general framework for state space exploration.

explore.h  - common data types and macros needed for a problem definition.

problem.c  - implements the algorithm for the pair token passing problem that 
	hooks into the general framework.

problem.h  - problem specific definitions, and the definitions of the hooks
	that the state exploration framework expects to be supplied by every
	problem definition.