Preliminary Translator, MuCAPSL to MuCIL

To test a preliminary version of the MuCAPSL translator, download this gzipped tar file, from which you can extract the following files:
gui.jar mucil.jar muparse.jar pre.cap capslex.muc mobile.muc gka.muc

This translator has a simple window interface with two text areas, one for a MuCAPSL specification and one for the translated result. MuCAPSL syntax and MuCIL output are described in the "MuCAPSL" DISCEX III paper on the CAPSL web site. A language reference report will appear soon. There is also a MuCAPSL introductory tutorial here. More details on the interface and usage are given below. The preliminary translator doesn't handle some language features completely as yet, such as ABORT.

The prelude pre.cap for MuCAPSL is somewhat different from that for CAPSL. The example capslex.muc is essentially a trivial CAPSL specification re-expressed in MuCAPSL. The example mobile.muc is a simplified mobile agent message forwarding protocol. The example gka.muc is a simplified version of the group key agreement algorithm used in Secure Spread.

Expand the tar file with:

gunzip mucapsltrans.tar.gz

tar xf mucapsltrans.tar

The translator is invoked with the java call

java -classpath gui.jar:mucil.jar:muparse.jar MuCAPSL

This call assumes that the jar files and the prelude pre.cap are in the current directory. Use the Open command in the File menu to load a MuCAPSL specification into the upper window. The Parse button invokes the parser only, to check the syntax, and puts the parse tree into the lower window. The Translate button puts the MuCIL translation into the lower window. The MuCIL output includes symbol table entries from the prelude, and axioms, if the Prelude box is activated, otherwise it omits them for brevity.

It is also possible to run the translator without the window by invoking the Java class MuCilGen, or just the type checker with the class mucheck, or just the parser with the class mucapsl. These classes read and write the UNIX Standard Input and Output.

The MuCAPSL translator was developed with the help of Sreekanth Malladi, as a graduate student at U. Idaho in 2002.