------
README
------

This file is part of EST package.

This file describes, how Model Checking module is builded.

1. INTRODUCTION
---------------

The short name of Model Checking module is 'mc'. This name is placed
in front of all filenames and external identifiers related to the module.
It may appear in all lowercase, or with its first letter capitalized,
written as 'mc' and 'Mc', respectively.

There are three categories of C functions:
- exported functions are visible outside the package,
- internal functions are visible to all files within the package only,
- static functions are visible to the file only.

There are two C headers, external and internal. The external header file,
named 'mc.h', defines features visible from outside the package.
The internal header file, named 'mcInt.h' defines features used in
multiple files inside the package, but not outside.

2. AN OVERVIEW
--------------

Model checking module consists of the following files:

  README		    - this file
  Makefile		    - Makefile
  Makefile.Linux	- Makefile for GNU/Linux
  Makefile.SunOS	- Makefile for Solaris
  Makefile.MINGW	- Makefile for MS Windows
  Makefile.Darwin	- Makefile for MacOSX
  mc.def	        - symbol definition for MS Windows
  mcstubs.def       - symbol definition for MS Windows

  mc.h
  mcInt.h
  mcMain.c
  mcThread.c
  mcDiagnostic.c
  mcAutomata.c
  mcMsc.c
  mcTree.c
  mcParser.l
  mcParser.y
  mcTcl.c
  mcDialog.tcl

  mc.decls
  mcDecls.h
  mcStubInit.c
  mcStubLib.c

3. HEADER FILES
---------------

mc.h:

mcInt.h:

4. SOURCE FILES
---------------

mcMain.c:

mcThread.c:

mcDiagnostic.c:

mcAutomata.c:

mcMsc.c:

mcTree.c:

mcParser.l:

mcParser.y:

mcTcl.c:

mcDialog.tcl:
