% some global effects/font defn's
\nopagenumbers
% \parskip 1 em
% \parindent 0 em
\font\fhead = cmbx10 scaled \magstep 2
\font\fnorm = cmr10 scaled \magstep 1
\font\fbold = cmbx10 scaled \magstep 1


% useful macros

\def\mysecthead#1{ {
   \vskip 1 em\fbold\noindent
   #1
   \vskip 1 ex
 } }

\def\myreversed#1{ {
   \leftskip=20 pt
   \noindent\hang
   #1

   } }

%
% The document:
%
\fnorm
\noindent
Matthew Ogilvie\hfill\break
CS 522-1\hfill\break
December 18, 1996\hfill\break
\centerline{\fbold Research Project Writeup}
\vskip 1 ex

My project was to write a tool for analyzing communications protocols.
More specifically, my program takes specifications for several communications
finite state machines, and then performs reachability analysis on them.
Among other things, it can find unused states and transitions, identify
deadlock and unspecified reception global states, and list out the
global states.

The program is invoked with as single command line 
argument the name of an input file.  This file has two types of statements,
first there are channel and message declarations, and second, there
are actual machine definations.  An example line declaring channels
is "channel A B C;",
which says that you have three channels, A, B and C.  Similarly,
"message X Y Z;" says that X, Y, and Z are possible messages that can be
send through channels.

To define a machine, the first line is "machine machine\_name",
where machine\_name is the name of the machine.  Then comes a block
defining the states and transitions in that machine.  It contains
"state\_name:" followed by one or more phrases
that read "channel + message $>$ new\_state ;"
(for receive message transition), "channel - message $>$ new\_state ;" (for
send message transitions), or "timeout $>$ new\_state ;"  (for timeout
transitions.  Timeouts will only occur if there are no more then 2
messages in any channel.)  The entire block (which may have multiple
"state\_name:" phrases) is enclosed in braces.  See one any of the
example machine files; it is easier to read an example.

The file is free-format, ignoring white space except where it separates
keywords from identifiers.  Comments can be specified anywhere by
putting a \# sign in; it comments out everything to the end of the line.
All states, machines, channels and messages are identified with standard
symbolic identifiers; you don't have to use nondescript numbers/letters
for any of them.

The output consists of three parts.  The first part is a list
of all global states.  All global states are numbered.  The first
time a given global state occurs in the output, it is printed out
completely.  Subsequent references only print the ID number.
The output repeatably lists the ID number of a
global state, then lists all successors of that state.  If a state
is deadlock or UR, that fact is listed in place of the nonexistent
successors.

The second part of the output prints out the machine specification, along
with information telling, for each state and each transition, weather or
not it was ever used.

The third part lists each channel, and tells weather it was ever used
and the maximum number of messages that were ever qued up in it.
After that is a single line summarizing how many deadlock and UR states
were found.

I've prepared several simple machines to test this program.
altbit.m is the simple alternating bit protocol.  dead.m demonstrates
dead code, as well as deadlocks and UR states.  proxybit.m is the alternating
bit protocol running through proxy machines.  timeout.m demonstrates
simple timeouts.  loosebit.m is supposed
to be the alternating bit protocol running on an unreliable connection,
but it seems to bring out a bug in my program instead.  My program ends up
generating about 40,000 global states before I decide to give up and
kill it.  I think there is a bug somewhere, either in loosebit.m, or
in my tool.  I haven't had time to track it down.

Internally, most everything is stored in linked lists, with a twist.
When I want to link a new element on to the front of a list, the
code first checks a hashtable of all elements ever enterred to
see if an element with the same data and the same next element
has been created before.  If it has, the thing returns that old element,
rather then creating a new one.  This of course means that
once an element is linked to something, it becomes immutable.  This
representation has 2 advantages: save memory, and easy comparison
to see if two global states are the same.  Comparing two
global states is as simple as comparing the pointers, because of
the way the lists are constructed.

The source code can be accessed in "\~{}mmogilvi/cs401/proj/".  analize.cpp
holds the meat of the program.  The other .cpp files are separate packages
I've written before.  The *.m files are the example machines, while
the *.out files are the tool's output on the corresponding machine.

Due to a combination of the fact that I was
rushed when I wrote this, and that this is the first C++ program I've written
that was more then 15 lines long, the code is somewhat ugly.  It could
definitely use a good overhaul to clean it up and make it more readable.

Some features that would be nice to add to this tool include:

\noindent \hang
0) A good name.

\noindent \hang
1) Fix the bug with the loosebit machine.

\noindent \hang
2) Clean up the code.

\noindent \hang
3) Add support for "variables" that can store references to channels,
and allow messages to have parameters.  Together these could
be used to simulate a client asking a server for the address of another
client.

\noindent \hang
4) Possibly related to 3, include support for machine templates, so
that you can specify several similar machines that differ only in
their name and in the channels they communicate with.

\bye
