EVAtrans library and eva2eva compiler

Library for the compilation of protocol specifications in EVA concrete syntax
into input specifications for protocol verifiers,
and translator that ouput specifications in EVA language.

+ Unpack:

 untar the package file EVAlib.tgz 
 (you certainly already have done this if you read this file), 
 all the files are left in a directory EVAlib.


+ Compilation: 
 It requires Ocaml 3.06 (ocamlc, ocamllex, ocamlyacc) and gnu make

 compile the EVAtrans library (cmi files and evatrans.cma)
 compile the interpreted executable eva2eva 
 it is left in EVAlib and requires ocamlrun to run
 in the directory EVAlib type
 % make 

 [optional] compile the native executable eva2eva (left in EVAlib)
 in the directory EVAlib type
 % make execopt

 [optional] to compile documentation
 (see section "Documentation files" for the files produced)
 in the directory EVAlib type
 % make doc

+ Other optional Makefile targets 
 (type commands in EVAlib)

 make only the EVAtrans library
 % make lib

 make only the interpreted executable eva2eva
 % make exec

 make the technical report (see "Documentation files")
 requires latex 2e, dvips, dvipdfm
 % make rapport

 make the html documentation of the sources (see "Documentation files")
 requires ocamldoc
 % make html

 rebuilt dependencies
 requires ocamldep
 % make dep  

 build a tag file TAGS from sources for emacs
 require etags
 % make tags 

 prepares the tar archive eva_pack.tar
 % make tar

 % make clean
  

+ Command:
 eva2eva [options] file.eva

 with options:
 -eva :   LAEVA output format
 -debug : debugging output format
 -trace : output debug info
 -help :  resume command and options

+ Library File:
 evatrans.cma

+ Documentation files:
 EVAlib/doc/rapport.pdf  
  technical report in PDF

 EVAlib/doc/rapport.ps (*)
  the same in postscript

 EVAlib/html (*)
  html documentation of the sources

 (*) this file are not included in the package and 
     must be must be compiled with the above commands

+ Source Files:

 evatrans.ml        interprete command line and call modules

 evalex.mll     def of lexical analyser for protocol specifications 
               in EVA concrete syntax 
 evalex.mli    
 evalex.ml      produced by ocamllex from evalex.mll

 evaparse.mly   grammar rules for parser of protocol specifications 
               in EVA concrete syntax   
 evaparse.mli   produced by ocamlparse from evaparse.mly
 evaparse.ml    idem

 abstract.mli   abstract syntax for protocol specifications
 abstract.ml    copy of abstract.mli

 location.mli   module for locations of elements in files
 location.ml 

 termutil.mli   utilities for terms in abstract syntax
 termutil.ml   

 types.mli      type checking and type coercion for abstract spec
 types.ml

 alias.mli      unaliasing and loop detection in alias definition (TODO)
 alias.ml      

 symbols.mli    manage symbols of abstact spec
 symbols.ml  

 translator.mli check specification in abstract syntax obtained by parser
 translator.ml  and translation function of abstract spec a la BAN
               into abstract spec multi-process.
              
 error.mli      error functions
 error.ml     

 trace.mli      trace functions (debug)
 trace.ml      

 evapp.mli      pretty printer to dump abstract spec in EVA concrete syntax  
 evapp.ml         

 debugpp.mli    pretty printer to dump abstract spec, for debug 
 debugpp.ml   

 pp.mli         utilities to pretty print lists
 pp.ml       

 README         this file

 makefile    
        
 exemples/      real exemples in EVA concrete syntax
 test/          small examples in EVA concrete syntax, for debug

 scripts/       perl scripts used to produce the doc