COMPILING INSTRUCTIONS:
-----------------------

1.) Install ACL2. The proof has been compiled completely with version 3.6. Installation instructions can be found at http://www.cs.utexas.edu/~moore/acl2/
2.) Set the ACL2_SYSTEM_BOOKS variable:
	export ACL2_SYSTEM_BOOKS="/xx/books"
    where `xx' is replaced with the installation directory of ACL2.
3.) Type the following from the directory lispfiles/:
	make

All books in all directories will be certified.


CONTENTS:
---------
This directory contains a formal proof of a necessary and sufficient condition for adpative deadlock-free packet-swicthing networks.

The following files are contained:
	algorithm.lisp:
		Contains the algorithm + the verification of all guards
	correctness.lisp:
		Contains the proof of correctness of the algorithm
	nec-suff-adaptive-PS.lisp
		Contains the complete proof of a neccessary and sufficient conditon.
	GeNoC.lisp
		The GeNoC function + generic proof of functional correctness
	GeNoC-*.lisp
		Generic definitions of routing, scheduling, injection, network state, nodeset, etc.
	equal-ids.lisp
		Definition and theorems on the equivalence-relation `equal-ids'.
	generic-buff-sign.lisp
		Defines a generic network state with buffers.
	generic-update-ntkstate:
		Definition of and theorems on a generic function to update the network state.
	perm.lisp
		Definitions and theorems on permutations.
	trlstp.lisp:
		Theorems on lists of valid travels.
	graphs.lisp:
		Formal graph theorems.
	dep-graph.lisp:
		Generic definition of the dependency graph.
	wait-graph:
		Generic definition of waiting graph.
	dally-seitz.lisp:
		The necessary and sufficient condition by Dally/Seitz

	
		

CONTACT:
--------
For any questions, mail f.verbeek@cs.ru.nl.

