diff --git a/README b/README
index bd00924..73978c3 100644
--- a/README
+++ b/README
@@ -31,3 +31,7 @@ If you want LaTeX output we need
 - The MSC macro package msc.sty
 - preamble.tex and postamble.tex
 
+For the documentation generation, optionally with graphs.
+- Doxygen: http://www.doxygen.org/
+- Dot: http://www.research.att.com/sw/tools/graphviz/
+
diff --git a/src/doxyconfig b/src/doxyconfig
index 1405c9b..d95e688 100644
--- a/src/doxyconfig
+++ b/src/doxyconfig
@@ -997,7 +997,7 @@ HIDE_UNDOC_RELATIONS   = YES
 # toolkit from AT&T and Lucent Bell Labs. The other options in this section 
 # have no effect if this option is set to NO (the default)
 
-HAVE_DOT               = NO
+HAVE_DOT               = YES
 
 # If the CLASS_GRAPH and HAVE_DOT tags are set to YES then doxygen 
 # will generate a graph for each documented class showing the direct and 
diff --git a/src/knowledge.h b/src/knowledge.h
index 3005da2..fc30d39 100644
--- a/src/knowledge.h
+++ b/src/knowledge.h
@@ -4,18 +4,31 @@
 #include "terms.h"
 #include "termlists.h"
 
+//! Knowledge structure.
+/**
+ * Contains a miminal representation of a knowledge set.
+ */
 struct knowledge
 {
+  //! A list of non-encrypted terms.
   Termlist basic;
+  //! A list of terms encrypted, such that the inverse is not in the knowledge set.
   Termlist encrypt;
   Termlist inverses;
   union
   {
+    //! List of open variables in the knowledge set.
+    /**
+     * This list is used to determine whether the knowledge needs to be rewritten.
+     * If a new substitution is done, one of the elements of this list will become closed,
+     * and we need to reconstruct the knowledge set.
+     */
     Termlist vars;		// special: denotes unsubstituted variables
     struct knowledge *next;	// use for alternative memory management.
   };
 };
 
+//! Shorthand for knowledge pointer.
 typedef struct knowledge *Knowledge;
 
 void knowledgeInit (void);
@@ -41,6 +54,7 @@ Knowledge knowledgeSubstDo (const Knowledge know);
 void knowledgeSubstUndo (const Knowledge know);
 Termlist knowledgeNew (const Knowledge oldk, const Knowledge newk);
 
+//! Harnass macro for recursive procedures.
 #define mindwipe(k,recurse) \
 	if (k != NULL && k->vars != NULL) { \
 		Termlist tl = k->vars; \
diff --git a/src/runs.c b/src/runs.c
index b3b06b6..b9d7a70 100644
--- a/src/runs.c
+++ b/src/runs.c
@@ -1,3 +1,7 @@
+/**
+ * @file runs.c Originally contained only procedures related to runs, but has grown
+ * somewhat over time.
+ */
 #include <stdlib.h>
 #include <stdio.h>
 #include <limits.h>
@@ -14,7 +18,10 @@
 /* from compiler.o */
 extern Term TERM_Type;
 
-/* for e.g. termprinting */
+//! Global flag that signals LaTeX output.
+/**
+ * True iff LaTeX output is desired.
+ */
 int globalLatex;
 
 static int indentState = 0;
diff --git a/src/runs.h b/src/runs.h
index 6f8bd14..0c7b888 100644
--- a/src/runs.h
+++ b/src/runs.h
@@ -13,125 +13,192 @@
 #define runPointerGet(sys,run)		sys->runs[run].index
 #define runPointerSet(sys,run,newp)	sys->runs[run].index = newp
 
+//! Structure for a role event node or list.
+/**
+ *\sa role
+ */
 struct roledef
 {
-  /* flag for internal actions (overriding normal type) */
+  //! flag for internal actions.
+  /**
+   * Typically, this is true to signify internal reads (e.g. variable choices)
+   * as opposed to a normal read.
+   */
   int internal;
+  //! Type of event.
+  /**
+   *\sa READ, SEND, CLAIM
+   */
   int type;
+  //! Event label.
   Term label;
+  //! Event sender.
   Term from;
+  //! Event target.
   Term to;
+  //! Event message.
   Term message;
+  //! Pointer to next roledef node.
   struct roledef *next;
 
-  /* illegal injections */
+  //! Illegal injections for this event.
   Knowledge forbidden;
-  /* knowledge transitions counter */
+  //! knowledge transitions counter.
   int knowPhase;
 
   /* evt runid for synchronisation, but that is implied in the
      base array */
 };
 
+//! Shorthand for roledef pointer.
 typedef struct roledef *Roledef;
 
-
+//! Role definition.
+/**
+ *\sa roledef
+ */
 struct role
 {
+  //! Name of the role encoded in a term.
   Term nameterm;
+  //! List of role events.
   Roledef roledef;
+  //! Local constants for this role.
   Termlist locals;
+  //! Pointer to next role definition.
   struct role *next;
 };
 
+//! Shorthand for role pointer.
 typedef struct role *Role;
 
+//! Protocol definition.
 struct protocol
 {
+  //! Name of the protocol encoded in a term.
   Term nameterm;
+  //! List of role definitions.
   Role roles;
+  //! List of role names.
   Termlist rolenames;
+  //! List of local terms for this protocol.
   Termlist locals;
+  //! Pointer to next protocol.
   struct protocol *next;
 };
 
+//! Shorthand for protocol pointer.
 typedef struct protocol *Protocol;
 
+//! Run container.
 struct run
 {
+  //! Protocol of this run.
   Protocol protocol;
+  //! Role of this run.
   Role role;
+  //! Agents involved in this run.
   Termlist agents;
+  //! Current execution point in the run.
   Roledef index;
+  //! Head of the run definition.
   Roledef start;
+  //! Current knowledge of the run.
   Knowledge know;
+  //! Locals of the run.
   Termlist locals;
 };
 
+//! Shorthand for run pointer.
 typedef struct run *Run;
 
+//! Buffer for variables substitution state.
 struct varbuf
 {
+  //! List of closed variables.
   Termlist	from;
+  //! List of terms to which the closed variables are bound.
   Termlist	to;
+  //! List of open variables.
   Termlist	empty;
 };
 
+//! Shorthand for varbuf pointer.
 typedef struct varbuf *Varbuf;
 
+//! Trace buffer.
 struct tracebuf
 {
+  //! Length of trace.
   int		length;
+  //! Length of trace minus the redundant events.
   int		reallength;
+  //! Array of events.
   Roledef	*event;
+  //! Array of run identifiers for each event.
   int		*run;
+  //! Array of status flags for each event.
+  /**
+   *\sa S_OKE, S_RED, S_TOD, S_UNK
+   */
   int		*status;
+  //! Array for matching sends to reads.
   int		*link;
-  int		violatedclaim;	// index of violated claim in trace
+  //! Index of violated claim in trace.
+  int		violatedclaim;	
+  //! Array of knowledge sets for each event.
   Knowledge	*know;
+  //! List of terms required to be in the final knowledge.
   Termlist	requiredterms;
+  //! List of variables in the system.
   Varbuf	variables;
 };
 
+//! The main state structure.
 struct system
 {
-  int step;			// can be managed globally
-  Knowledge know;
+  int step;			//!< Step in trace during exploration. Can be managed globally
+  Knowledge know;		//!< Knowledge in currect step of system.
   struct parameters *parameters;	// misc
   /* static run info, maxruns */
   Run runs;
 
   /* global */
-  int maxruns;
+  int maxruns;			//!< Number of runs in the system.
 
   /* properties */
-  Termlist secrets;		// integrate secrets list into system
-  int shortestattack;		// length of shortest attack trace
+  Termlist secrets;		//!< Integrate secrets list into system.
+  int shortestattack;		//!< Length of shortest attack trace.
 
   /* switches */
   int report;
-  int prune;			// type of pruning
-  int switch_maxtracelength;	// helps to remember the length of the last trace
-  int maxtracelength;		// helps to remember the length of the last trace
-  int switchM;			// memory
-  int switchT;			// time
-  int switchS;			// progress (traversed states)
-  int porparam;			// a multi-purpose integer parameter, passed to the partial order reduction method selected
-  int latex;			// latex output switch
+  int prune;			//!< Type of pruning.
+  int switch_maxtracelength;	//!< Helps to remember the length of the last trace.
+  int maxtracelength;		//!< helps to remember the length of the last trace.
+  int switchM;			//!< Memory display switch.
+  int switchT;			//!< Time display switch.
+  int switchS;			//!< Progress display switch. (traversed states)
+  int porparam;			//!< A multi-purpose integer parameter, passed to the partial order reduction method selected.
+  //! Latex output switch.
+  /**
+   * Obsolete. Use globalLatex instead.
+   *\sa globalLatex
+   */
+  int latex;			
 
   /* traversal */
-  int traverse;			// traversal method
-  int explore;			// boolean: explore states after actions or not
+  int traverse;			//!< Traversal method.
+  int explore;			//!< Boolean: explore states after actions or not.
 
   /* counters */
   unsigned long int statesLow;
   unsigned long int statesHigh;
-  unsigned long int claims;	// number of claims encountered
-  unsigned long int failed;	// number of claims failed
+  unsigned long int claims;	//!< Number of claims encountered.
+  unsigned long int failed;	//!< Number of claims failed.
 
   /* matching */
-  int match;			// matching type
-  int clp;			// do we use clp?
+  int match;			//!< Matching type.
+  int clp;			//!< Do we use clp?
 
   /* protocol definition */
   Protocol protocols;
@@ -150,7 +217,7 @@ struct system
   int knowPhase;		// which knowPhase have we already explored?
   Constraintlist constraints;	// only needed for CLP match
 
-  /* relevant: storage of shortest attack */
+  //! Shortest attack storage.
   struct tracebuf* attack;
 };
 
diff --git a/src/termlists.c b/src/termlists.c
index b998650..c36df18 100644
--- a/src/termlists.c
+++ b/src/termlists.c
@@ -11,34 +11,36 @@
 extern Term TERM_Function;
 extern Term TERM_Hidden;
 
+//! Open termlists code.
 void
 termlistsInit (void)
 {
   return;
 }
 
+//! Close termlists code.
 void
 termlistsDone (void)
 {
   return;
 }
 
-/* inline candidate */
-
+//! Allocate memory for a termlist node.
+/**
+ *@return A pointer to uninitialised memory of the size of a termlist node.
+ */
 Termlist
 makeTermlist ()
 {
+  /* inline candidate */
   return (Termlist) memAlloc (sizeof (struct termlist));
 }
 
-/*
-
-termlistDuplicate
-
-A deep copy.
-
-*/
-
+//! Duplicate a termlist.
+/**
+ * Uses termDuplicate to copy the elements, and allocated new memory for the list nodes.
+ *\sa termDuplicate(), termlistShallow()
+ */
 Termlist
 termlistDuplicate (Termlist tl)
 {
@@ -55,15 +57,12 @@ termlistDuplicate (Termlist tl)
   return newtl;
 }
 
-/*
-
-termlistShallow
-
-A shallow copy, because I gather we won't be modifying any terms, only
-termlists. Oh, and it reverses the order :) Don't forget!
-
-*/
-
+//! Shallow reverse copy of a termlist.
+/**
+ * Just copies the element pointers. Allocates new memory for the list nodes.
+ * Note that it reverses the order of the list.
+ *\sa termlistDuplicate()
+ */
 Termlist
 termlistShallow (Termlist tl)
 {
@@ -78,14 +77,11 @@ termlistShallow (Termlist tl)
   return newtl;
 }
 
-/*
-
-termlistDelete
-
-(shallow)
-
-*/
-
+//! Shallow deletion of a termlist.
+/**
+ * Deletes the termlist nodes only. Elements are intact after exit.
+ *\sa termlistShallow()
+ */
 void
 termlistDelete (Termlist tl)
 {
@@ -96,14 +92,11 @@ termlistDelete (Termlist tl)
 }
 
 
-/*
-
-termlistDestroy
-
-(deep)
-
-*/
-
+//! Deep deletion of a termlist.
+/**
+ * Deletes the termlist nodes as well as the elements.
+ *\sa termlistDuplicate(), termDuplicate(), termDelete()
+ */
 void
 termlistDestroy (Termlist tl)
 {
@@ -114,14 +107,10 @@ termlistDestroy (Termlist tl)
   memFree (tl, sizeof (struct termlist));
 }
 
-/*
-
-inTermlist
-
-check whether a term occurs in a termlist
-
-*/
-
+//! Determine whether a term is an element of a termlist.
+/**
+ *@return True iff the term is an element of the termlist.
+ */
 int
 inTermlist (Termlist tl, Term term)
 {
@@ -141,8 +130,11 @@ inTermlist (Termlist tl, Term term)
     }
 }
 
-/* are all elements of list 1 in list 2, and vice versa? 
- Note that we assume unique elements !
+//! Equality of two term lists.
+/**
+ * Are all elements of list 1 in list 2, and vice versa? 
+ * Note that we assume unique elements!
+ *@param True iff every element of the list is in the other list.
  */
 
 int
@@ -159,15 +151,12 @@ isTermlistEqual (Termlist tl1, Termlist tl2)
   return 1;
 }
 
-/*
-
-termlistAdd
-
-Adds a term. Duplicates are allowed.
-A new list pointer is returned.
-
-*/
-
+//! Adds a term to the front of a termlist.
+/**
+ * Duplicates are allowed.
+ *@return A new list pointer.
+ *\sa termlistAppend()
+ */
 Termlist
 termlistAdd (Termlist tl, Term term)
 {
@@ -191,15 +180,12 @@ termlistAdd (Termlist tl, Term term)
   return newtl;
 }
 
-/*
-
-termlistAppend
-
-Appends a term to the end of the list. Duplicates are allowed.
-A new list pointer is returned.
-
-*/
-
+//! Adds a term to the end of a termlist.
+/**
+ * Duplicates are allowed.
+ *@return A new list pointer if the termlist was NULL.
+ *\sa termlistAdd()
+ */
 Termlist
 termlistAppend (const Termlist tl, const Term term)
 {
@@ -226,6 +212,11 @@ termlistAppend (const Termlist tl, const Term term)
   return tl;
 }
 
+//! Concatenates two termlists.
+/**
+ * The last pointer of the first list is made to point to the second list.
+ *@return The pointer to the concatenated list.
+ */
 Termlist
 termlistConcat (Termlist tl1, Termlist tl2)
 {
@@ -241,14 +232,12 @@ termlistConcat (Termlist tl1, Termlist tl2)
   return tl1;
 }
 
-/*
-
-termlistDelTerm
-
-remove the current element from the termlist. Easier because of the
-double linked list.
-
-*/
+//! Remove the pointed at element from the termlist.
+/**
+ * Easier because of the double linked list.
+ *@param tl The pointer to the termlist node to be deleted from the list.
+ *@return The possibly new head pointer to the termlist.
+ */
 Termlist
 termlistDelTerm (Termlist tl)
 {
@@ -273,6 +262,10 @@ termlistDelTerm (Termlist tl)
   return newhead;
 }
 
+//! Construct the conjunction of two termlists.
+/**
+ *@return A new termlist containing the elements in both lists.
+ */
 Termlist
 termlistConjunct (Termlist tl1, Termlist tl2)
 {
@@ -290,6 +283,10 @@ termlistConjunct (Termlist tl1, Termlist tl2)
   return newtl;
 }
 
+//! Construct the conjunction of two termlists, and a certain type.
+/**
+ *@return A new termlist containing the elements in both lists, that are also of the desired type.
+ */
 Termlist
 termlistConjunctType (Termlist tl1, Termlist tl2, int termtype)
 {
@@ -307,6 +304,10 @@ termlistConjunctType (Termlist tl1, Termlist tl2, int termtype)
   return newtl;
 }
 
+//! Construct the conjunction of a termlist and a certain type.
+/**
+ *@return A new termlist containing the elements in the list that are of the desired type.
+ */
 Termlist
 termlistType (Termlist tl, int termtype)
 {
@@ -324,6 +325,10 @@ termlistType (Termlist tl, int termtype)
   return newtl;
 }
 
+//! Display a termlist.
+/**
+ * Lists of terms are displayed between square brackets, and seperated by commas.
+ */
 void
 termlistPrint (Termlist tl)
 {
@@ -343,6 +348,13 @@ termlistPrint (Termlist tl)
   printf ("]");
 }
 
+//! Append all open variables in a term to a list.
+/**
+ *@param tl The list to which to append to.
+ *@param t The term possibly containing open variables.
+ *@return The pointer to the extended list.
+ *\sa termlistAddRealVariables()
+ */
 Termlist
 termlistAddVariables (Termlist tl, Term t)
 {
@@ -368,6 +380,13 @@ termlistAddVariables (Termlist tl, Term t)
     }
 }
     
+//! Append all variables in a term to a list.
+/**
+ *@param tl The list to which to append to.
+ *@param t The term possibly containing open and closed variables.
+ *@return The pointer to the extended list.
+ *\sa termlistAddVariables()
+ */
 Termlist
 termlistAddRealVariables (Termlist tl, Term t)
 {
@@ -403,6 +422,13 @@ termlistAddRealVariables (Termlist tl, Term t)
     }
 }
 
+//! Append all basic terms in a term to a list.
+/**
+ *@param tl The list to which to append to.
+ *@param t The term containing basic terms.
+ *@return The pointer to the extended list.
+ *\sa termlistAddBasics()
+ */
 Termlist
 termlistAddBasic (Termlist tl, Term t)
 {
@@ -426,6 +452,13 @@ termlistAddBasic (Termlist tl, Term t)
   return tl;
 }
 
+//! Append all basic terms in a termlist to another list.
+/**
+ *@param tl The list to which to append to.
+ *@param scan The termlist with terms containing basic terms.
+ *@return The pointer to the extended list.
+ *\sa termlistAddBasic()
+ */
 Termlist
 termlistAddBasics (Termlist tl, Termlist scan)
 {
@@ -437,13 +470,11 @@ termlistAddBasics (Termlist tl, Termlist scan)
   return tl;
 }
 
-/*
- * termlistMinusTerm
- *
- * Remove a term from a termlist, and yield a new termlist pointer.
- * Semantics: remove the first occurrence of the term.
+//! Remove a term from a termlist.
+/**
+ * Removes the first occurrence of the term.
+ *@return A new termlist pointer.
  */
-
 Termlist
 termlistMinusTerm (Termlist tl, Term t)
 {
@@ -460,6 +491,7 @@ termlistMinusTerm (Termlist tl, Term t)
   return tl;
 }
 
+//! Determine the length of a termlist.
 int
 termlistLength (Termlist tl)
 {
@@ -473,14 +505,15 @@ termlistLength (Termlist tl)
   return i;
 }
 
-/*
-
-inverseKey
-
-Gives the inverse Key of some term (which is used to encrypt something), as is defined
-by the termlist, which is a list of key1,key1inv, key2, key2inv, etc...
-
-*/
+//! Give the inverse key term of a term.
+/**
+ * Gives a duplicate of the inverse Key of some term (which is used to encrypt something), as is defined
+ * by the termlist, which is a list of key1,key1inv, key2, key2inv, etc...
+ *@param inverses The list of inverses, typically from the knowledge.
+ *@param key Any term of which the inverse will be determined.
+ *@return A pointer to a duplicate of the inverse key term.
+ *\sa termDuplicate(), knowledge::inverses
+ */
 
 
 Term
@@ -535,14 +568,12 @@ inverseKey (Termlist inverses, Term key)
   return termDuplicate (key);	/* defaults to symmetrical */
 }
 
+//! Create a term local to a run.
 /*
- * localTerm
- *
- * Creates a term local to a run.
  * We assume that at this point, no variables have been instantiated yet that occur in this term.
  * We also assume that fromlist, tolist and locals only hold real leaves.
+ *\sa termlistLocal()
  */
-
 Term
 termLocal (const Term t, Termlist fromlist, Termlist tolist,
 	   const Termlist locals, const int runid)
@@ -585,12 +616,11 @@ termLocal (const Term t, Termlist fromlist, Termlist tolist,
     }
 }
 
-/*
- * termlistLocal
- *
- * We expand the previous concept to termlists.
+//! Create a list of instance terms.
+/**
+ * We expand the termlocal concept to termlists.
+ *\sa termLocal()
  */
-
 Termlist
 termlistLocal (Termlist tl, const Termlist fromlist, const Termlist tolist,
 	       const Termlist locals, int runid)
@@ -607,10 +637,12 @@ termlistLocal (Termlist tl, const Termlist fromlist, const Termlist tolist,
   return newtl;
 }
 
-/*
- * Check whether tl2 is contained in tl1.
+//! Check whether a termlist is contained in another.
+/**
+ *@param tlbig The big list.
+ *@param tlsmall The list that is possibly contained in the big one.
+ *@return True iff tlsmall is contained in tlbig.
  */
-
 int
 termlistContained (const Termlist tlbig, Termlist tlsmall)
 {
@@ -623,9 +655,14 @@ termlistContained (const Termlist tlbig, Termlist tlsmall)
   return 1;
 }
 
-/*
+//! Check substitution validity
+/**
  * Determine whether a variable has been substituted with something with
  * the right type.
+ *@param matchmode The system matching mode, typically system::match
+ *@param term The closed variable term.
+ *@return True iff the substitution is valid in the current mode.
+ *\sa system::match
  */
 
 int
@@ -653,15 +690,15 @@ validSubst (const int matchmode, const Term term)
     }
 }
 
-/*
- * termFunction
- *
- * An assist function that helps to simulate Term->Term functions, using
- * termlists. One termlist functions as the domain, and the other as the
- * range.
- *
- * Extending a function with a value y = f(x) amounts to extending the
- * domain with x, and the range with y.
+//! Yield the result of f(x)
+/**
+ * This function interpretes two termlists as the domain and range of a function,
+ * and if the term occurs in the domain, returns the matching value from the range.
+ * Note that these functions cannot have NULL in the domain or the range.
+ *@param fromlist The domain list.
+ *@param tolist The range list, in a one-to-one correspondence with the fromlist.
+ *@param tx The point on which the function is to be evaluated.
+ *@return The result of the function application or NULL if the point is not within the domain.
  */
 
 Term
@@ -679,10 +716,7 @@ termFunction (Termlist fromlist, Termlist tolist, Term tx)
   return NULL;
 }
 
-/*
- * Forward the termlist pointer to the last item
- */
-
+//! Yield the last node of a termlist.
 Termlist
 termlistForward (Termlist tl)
 {
diff --git a/src/termlists.h b/src/termlists.h
index 235bb73..40303a4 100644
--- a/src/termlists.h
+++ b/src/termlists.h
@@ -3,13 +3,22 @@
 
 #include "terms.h"
 
+//! The list container for the term type.
+/**
+ * Implemented as a double linked list to allow for element deletion.
+ *\sa term
+ */
 struct termlist
 {
+  //! The term element for this node.
   Term term;
+  //! Next node pointer or NULL for the tail of the list.
   struct termlist *next;
+  //! Previous node pointer or NULL for the head of the list.
   struct termlist *prev;
 };
 
+//! Shorthand for termlist pointers.
 typedef struct termlist *Termlist;
 
 void termlistsInit (void);
diff --git a/src/terms.c b/src/terms.c
index 7ddcec1..bd76703 100644
--- a/src/terms.c
+++ b/src/terms.c
@@ -25,24 +25,34 @@ void indent (void);
 /* Two types of terms: general, and normalized. Normalized rewrites all
    tuples to (x,(y,z))..NULL form, making list traversal easy. */
 
+//! Initialization of terms code.
 void
 termsInit (void)
 {
   return;
 }
 
+//! Cleanup of terms code.
 void
 termsDone (void)
 {
   return;
 }
 
+//! Allocate memory for a term.
+/**
+ *@return A pointer to the new term memory, which is not yet initialised.
+ */
 Term
 makeTerm ()
 {
   return (Term) memAlloc (sizeof (struct term));
 }
 
+//! Create a fresh encrypted term from two existing terms.
+/**
+ *@return A pointer to the new term.
+ */
 Term
 makeTermEncrypt (Term t1, Term t2)
 {
@@ -54,6 +64,10 @@ makeTermEncrypt (Term t1, Term t2)
   return term;
 }
 
+//! Create a fresh term tuple from two existing terms.
+/**
+ *@return A pointer to the new term.
+ */
 Term
 makeTermTuple (Term t1, Term t2)
 {
@@ -82,6 +96,11 @@ makeTermTuple (Term t1, Term t2)
   return tt;
 }
 
+//! Make a term of the given type with run identifier and symbol.
+/**
+ *@return A pointer to the new term.
+ *\sa GLOBAL, VARIABLE, LEAF, ENCRYPT, TUPLE
+ */
 Term
 makeTermType (const int type, const Symbol symb, const int runid)
 {
@@ -94,12 +113,13 @@ makeTermType (const int type, const Symbol symb, const int runid)
   return term;
 }
 
-/* deVar unwraps any substitutions.
- *
- * For speed, it is a macro. Sometimes it will call
+//! Unwrap any substitutions.
+/**
+ * For speed, it is also a macro. Sometimes it will call
  * deVarScan to do the actual unwinding.
+ *@return A term that is either not a variable, or has a NULL substitution.
+ *\sa deVar()
  */
-
 Term
 deVarScan (Term t)
 {
@@ -108,6 +128,10 @@ deVarScan (Term t)
   return t;
 }
 
+//! Determine whether a term contains an unsubstituted variable as subterm.
+/**
+ *@return True iff there is an open variable as subterm.
+ */
 int
 hasTermVariable (Term term)
 {
@@ -125,18 +149,16 @@ hasTermVariable (Term term)
     }
 }
 
-/*
 
-isTermEqualFn(term,term)
-
-Tests whether two terms are completely identical. This also includes
-variables. This is the recursive function.
-
-We assume the term is normalized, e.g. no tupling has direct
-subtupling.
-
-Out: 0 unequal, 1 equal
-*/
+//!Tests whether two terms are completely identical.
+/**
+ * This also includes
+ * variables. This is the recursive function.
+ * We assume the term is normalized, e.g. no tupling has direct
+ * subtupling.
+ *@return True iff the terms are equal.
+ *\sa isTermEqual()
+ */
 
 int
 isTermEqualFn (Term term1, Term term2)
@@ -179,6 +201,12 @@ isTermEqualFn (Term term1, Term term2)
     }
 }
 
+//! See if a term is a subterm of another.
+/**
+ *@param t Term to be checked for a subterm.
+ *@param tsub Subterm.
+ *@return True iff tsub is a subterm of t.
+ */
 int
 termOccurs (Term t, Term tsub)
 {
@@ -195,7 +223,7 @@ termOccurs (Term t, Term tsub)
     return (termOccurs (t->op, tsub) || termOccurs (t->key, tsub));
 }
 
-
+//! Print a term to stdout.
 void
 termPrint (Term term)
 {
@@ -282,13 +310,12 @@ termPrint (Term term)
 }
 
 
-/*
-
-Duplicate
-
-make a deep copy of a term, but not of leaves.
-
-*/
+//! Make a deep copy of a term.
+/**
+ * Leaves are not copied.
+ *@return If the original was a leaf, then the pointer is simply returned. Otherwise, new memory is allocated and the node is copied recursively.
+ *\sa termDuplicateDeep()
+ */
 
 Term
 termDuplicate (const Term term)
@@ -315,13 +342,13 @@ termDuplicate (const Term term)
   return newterm;
 }
 
-/*
+//! Make a true deep copy of a term.
+/**
+ * Currently, it this function is not to be used, so we can be sure leaf nodes occur only once in the system.
+ *@return New memory is allocated and the node is copied recursively.
+ *\sa termDuplicate()
+ */
 
-DuplicateDeep
-
-make a deep copy of a term, and also of leaves.
-
-*/
 
 Term
 termDuplicateDeep (const Term term)
@@ -353,10 +380,10 @@ termDuplicateDeep (const Term term)
   return newterm;
 }
 
-/*
- * DuplicateUV
- *
+//! Make a copy of a term, but remove substituted variable nodes.
+/**
  * Remove all instantiated variables on the way down.
+ *\sa termDuplicate()
  */
 
 Term
@@ -423,13 +450,12 @@ realTermDuplicate (const Term term)
   return newterm;
 }
 
-/*
-
-termDelete
-
-Removes a term and deallocates memory
-
-*/
+//!Removes a term and deallocates memory.
+/**
+ * Is meant to remove terms make with termDuplicate. Only deallocates memory
+ * of nodes, not of leaves.
+ *\sa termDuplicate(), termDuplicateUV()
+ */
 
 void
 termDelete (const Term term)
@@ -450,13 +476,13 @@ termDelete (const Term term)
     }
 }
 
-/*
-   termNormalize
-
-   avoids problems with associativity by rewriting every ((x,y),z) to
-   (x,y,z)), i.e. a normal form for terms, after which equality is
-   okay.
-*/
+//! Normalize a term with respect to tupling.
+/**
+ * Avoids problems with associativity by rewriting every ((x,y),z) to
+ * (x,(y,z)), i.e. a normal form for terms, after which equality is
+ * okay. No memory was allocated or deallocated, as only pointers are swapped.
+ *
+ *@return After execution, the term pointed at has been normalized. */
 
 void
 termNormalize (Term term)
@@ -493,7 +519,12 @@ termNormalize (Term term)
     }
 }
 
-
+//! Copy a term, and ensure all run identifiers are set to the new value.
+/**
+ * Strange code. Only to be used on locals, as is stupidly replaces all run identifiers.
+ *@return The new term.
+ *\sa termDuplicate()
+ */
 Term
 termRunid (Term term, int runid)
 {
@@ -527,8 +558,10 @@ termRunid (Term term, int runid)
     }
 }
 
-/* tupleCount yields the size of the top tuple in the term */
-
+//! Determine tuple width of a given term.
+/**
+ *\sa tupleProject()
+ */
 int
 tupleCount (Term tt)
 {
@@ -550,9 +583,13 @@ tupleCount (Term tt)
     }
 }
 
-/* tupleProject yields the projection pi (0 .. n-1) on a top tuple. Returns
- * NULL if the range is incorrect. */
-
+//! Yield the projection Pi(n) of a term.
+/**
+ *@param tt Term
+ *@param n The index in the tuple.
+ *@return Returns either a pointer to a term, or NULL if the index is out of range.
+ *\sa tupleCount()
+ */
 Term
 tupleProject (Term tt, int n)
 {
@@ -591,9 +628,12 @@ tupleProject (Term tt, int n)
     }
 }
 
-/* number of elements in a term.
- *
+//! Determine size of term.
+/**
+ * Determines the size of a term according to some heuristic.
  * Currently, the encryption operator is weighed as well.
+ *@return Returns a nonnegative integer.
+ *\sa termDistance()
  */
 
 int
@@ -622,7 +662,10 @@ termSize(Term t)
     }
 }
 
-/* Yield some sort of distance between two terms, as a float between 0 and 1.
+//! Determine distance between two terms.
+/**
+ *@return A float value between 0, completely dissimilar, and 1, equal.
+ *\sa termSize()
  */
 
 float
diff --git a/src/terms.h b/src/terms.h
index 5b82c51..fc2a9ce 100644
--- a/src/terms.h
+++ b/src/terms.h
@@ -9,31 +9,53 @@
 #define	ENCRYPT  4
 #define	TUPLE	 5
 
+//! The most basic datatype in the modelchecker.
+/**
+ * Describes a single term.
+ */
+
 struct term
 {
   /* basic  : name,runid
      encrypt: op,key
      tuple  : op,next
    */
+
+  //! The type of term.
+  /**
+   * \sa GLOBAL, VARIABLE, LEAF, ENCRYPT, TUPLE
+   */
   int type;
-  void *stype;			// only for leaf, termlist pointer
+  //! Data Type termlist (e.g. agent or nonce)
+  /** Only for leaves. */
+  void *stype;			
+  //! Substitution term.
+  /**
+   * If this is non-NULL, this leaf term is apparently substituted by
+   * this term.
+   */
   struct term *subst;		// only for variable/leaf, substitution term
 
   union
   {
     Symbol symb;
+    //! Encrypted subterm.
     struct term *op;
+    //! Left-hand side of tuple pair.
     struct term *op1;
     struct term *next;		// for alternative memory management
   };
   union
   {
     int runid;
+    //! Key used to encrypt subterm.
     struct term *key;
+    //! Right-hand side of tuple pair.
     struct term *op2;
   };
 };
 
+//! Pointer shorthand.
 typedef struct term *Term;
 
 void termsInit (void);