eva2cpl

Translator to compile protocol specifications in EVA concrete syntax
into CPL input spec for protocol verifiers.
It is based on the EVA translator library v6.1


+ Unpack:

 untar the package file EVA2CPL.tar in a directory that we call SRC below
 (you certainly already have done this if you read this file).
 It produces the subdirectory of SRC:
  - EVAlib which contains the source and doc of the EVAtrans library,
    necessary to compile eva2CPL
  - EVA2CPL which contains the sources of eva2cpl 


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

 compile the EVAtrans library, it produces cmi files and evatrans.cma
 in the directory SRC type:
 % make -C EVAlib lib

 compile the interpreted executable eva2cpl
 it is left in SRC/EVA2CPL and requires ocamlrun to run,
 a symbolic link to eva2cpl called evatrans is also left in SRC/EVA2CPL
 in the directory SRC/EVA2CPL type:
 % make  

 [optional] compile the native executable eva2eva.opt
            it is left in SRC/EVA2CPL
 in SRC/EVA2CPL type:
 % make execopt

 To produces doc files (EVA language syntax and semantics etc), 
 see SRC/EVAlib/README


+ Other optional Makefile targets 
 (type commands in SRC/EVA2CPL )

 build html documentation of sources
 requires ocamldoc
 % make doc

 prepares the tar archive eva_pack.tar
 % make tar

 rebuilt dependencies
 requires ocamldep
 % make dep  

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

 % make clean 


+ Command:

 eva2cpl [options] file.eva

 with options:
 -cpl :   CPL output format (default)
 -eva :   LAEVA output format
 -debug : debugging output format
 -trace : output debug info
 -help :  resume command and options



+ Files:

 see SRC/EVAlib/README for a description of the files of the EVAtrans library

 SRC/EVA2CPL/eva2cpl.ml   
  sources main, interpretation of command line

 SRC/EVA2CPL/cplpp.mli
 SRC/EVA2CPL/cplpp.ml 
  pretty printer to dump abstract spec in CPL syntax, source and interface

 SRC/EVA2CPL/README
  this file

 SRC/EVA2CPL/Makefile    

 SRC/EVA2CPL/.depend 
  dependencies for Makefile  
        
 SRC/EVA2CPL/test/
  test files in EVA concrete syntax, for debug purpose