===========================================================================
This directory contains the source code for the Murphi Compiler 
Release 3.1.

Please follow the following steps to generate the executable of the 
Murphi Compiler (mu) if you do not find an executable for your machine 
in the bin directory:
- edit the Makefile to select the correct C++ compiler for your machine
- build the Murphi compiler with "make mu"
- set the link in the bin directory with "ln -s ../src/mu mu", if the link
 has not already been created.

If you want to do changes in the Murphi language, read the Rebuild.Note 
and the Hacker.Manual1.

===========================================================================
This directory contains the following files:

Hacker.Manual1	: manual on how the source code is structured
Makefile	: makefile for compiling Murphi Compiler
Makefile.full	: makefile for compiling Murphi Compiler with modified grammar
Readme		: this file
Rebuild.Note	: note on how to recompile Murphi Compiler
cpp_code.C	: code generation routines for the C++ verifier
cpp_code_as.C	: code generation routines for the assignment operators
cpp_sym.C	: code generation routines for symmetry reduction
cpp_sym.h	: header for symmetry code generation
cpp_sym_aux.C	: auxiliary code generation for symmetry reduction
cpp_sym_decl.C	: declaration handling for symmetry reduction
decl.C		: declaration handling
decl.h		: interface for declarations
error.C		: error handler
expr.C		: expression handling
expr.h		: interface for expressions
lex.yy.c	: code for the lexer, generated by flex
		: source: "mu.l"
lextable.C	: hash table used by the lexer
lextable.h	: interface for the hashtable
mu.C		: main program
mu.grammar	: yacc grammar for Murphi, without any actions 
		: not used in compilation
mu.h		: main header file, includes all other .h files
mu.l		: lex (flex) source for the lexer
mu.y		: yacc (Berkeley yacc) source for the parser
no_code.C	: an empty code.C, to facilitate writing back ends.
		: not used in compilation
parse.C		: parsing routines
rule.C		: rules handling
rule.h		: interface for rules
stmt.C		: statements handling
stmt.h		: interface for statements
symtab.C	: symbol table handling
util.C		: utilities
y.output	: info file generated by Berkeley yacc from "mu.y"
y.tab.c		: C file generated by Berkeley yacc from "mu.y"
y.tab.h		: Include file generated by Berkeley yacc "mu.y"
===========================================================================
