DCVALID version 1.3
			 ===================
				  by
			  Paritosh K. Pandya
		Tata Institute of Fundamental Research
			    Mumbai, India
  

DCVALID is a program to check validity of discrete time duration
calculus formulae. It also provides facilities for checking validity
of dense-time formulae without any lengths or durations.  DCVALID
deals with Quantified (i.e. second order) Propositional Duration
Calculus formulae.

DCVALID1.3 makes use of the the validity checker for WS1S formulae,
MONA1.3, from Aarhus University, Denmark. Information on Mona may be
obtained on the Web at the following URL
       http://www.brics.dk/~mona/ 
We are grateful to the designers of MONA for giving us permission to
use MONA1.3 with DCVALID1.3.



INSTALLATION NOTES:

1. Distribution is available for linux-elf and Sun SOLARIS platforms.
   For example, the linux distribution is called
           dccheck103-linux.tgz
   Please gunzip and untar the distribution archive. 

2. This will create a subdirectory called 
           dccheck103
   Please go to this subdirectory by doing
           cd dccheck103

3. Run installation script
           install.dcvalid

   This generates three executable scripts 
      dcvalid dcestobs dcautps

4. Add the directory with script file "dcvalid" to your search path.
   OR
   Add a link to files "dcvalid" "dcestobs" and "dcautps" from a 
   directory in your search path such as /usr/local/bin

USAGE:

1. The validity checker can be invoked by 
           dcvalid <file>
   where the <file> is the name of the file giving Duration Calculus
   specification to be checked. Try    
          dcvalid test 

2. File dcvalid.doc is the user manual for this software.

3. Subdirectory 
         examples
   contains some example specifications including that of a Minepump
   and Fischer's mutual exclusion protocol.

5. Comments and bug reports should be sent to
	pandya@tcs.tifr.res.in