Preliminary Translator, CAPSL to CIL

To test a preliminary version of the CAPSL translator, download this gzipped tar file, from which you can extract a directory containing several java classes, including capsl.class, tcheck.class, and cil2cil.class, a shell script cil, files pre.cap and rulegen.maude, and a subdirectory ex with several .cap files. After uncompressing the file to capsltrans.tar, expand it with:

tar xf capsltrans.tar

The CAPSL translator reads a CAPSL file from the UNIX standard input and writes CIL output to standard output. CAPSL syntax and CIL output are described in the "CAPSL Intermediate Language" report on the CAPSL web site. The restrictions on the current version are summarized later in this note. An example of CIL output is this one for the Needham-Schroeder Public-Key protocol.

To run the CAPSL translator and produce transition rules, you will need the Maude 1 executable, specifically the "Core Maude system." This can be downloaded from the Maude web site http://maude.csl.sri.com. You need Maude 1 rather than Maude 2; follow the "Looking for Maude 1?" link. Versions are available for Linux, Solaris, SunOS, and FreeBSD. All you need for CIL are the Core Maude system (e.g., maude.linux) and the file prelude.maude, which must be in the same directory. The path to the executable should be indicated by setting the environment variable MAUDE, so that the cil script can find it. For example:

setenv MAUDE ~/maude-system/bin/maude.linux

Alternatively, you can simply edit the shell script cil to insert the path to the Maude executable in place of $MAUDE.

The translator is invoked by invoking cil, for example:

cil <ex/nspk.cap

The cil script produces two temporary files outable and outcil containing intermediate partial forms of the specification.

Note: If the rule generator finds an implementability error, the full error message and partial rule set can be seen in the file outcil.

CAPSL syntax and type checking can be tested without Maude, in any system that can run Java programs, using the Java class tcheck.class. It reads CAPSL from the standard input and writes a symbol table and message parse tree to the standard output. The CAPSL prelude pre.cap is automatically read first. For example, invoke:

java tcheck <ex/nspk.cap

Translator Restrictions

This version of the translator is still preliminary and experimental.

When using subprotocols, there should be no further actions or messages after an IF selection or INCLUDE.
IF-THEN-ELSE conditions as boolean expressions are not implemented.
IMPORTS declarations are not checked or acted upon; they are simply informative.
ASSUME and PROVE assertions in the MESSAGES list are not included in the CIL output.
GOALS do not result in the creation of special rewrite rules that generate goal violation facts.