CSML is a high level level language for describing finite state machines. There is a compiler which produces a finite state machine as output. There is also a CTL model checker called MCB which accepts the state machine file as input. MCB is an enhanced version of the EMC model checker. Both are available by clicking on the line below, or via anonymous FTP (user anonymous, password anonymous@host) on EMC.CS.CMU.EDU ( in


pub/csml.tar.Z (230K) - compressed tar file
csml.tar.gz (131K) - gzipped tar file
Clicking on the reference above retrieves the file automatically.

csml.tar.Z contains the sources and binaries for Sun 3, and VAX in "tar" format. To break out the directory structure, after you have gotten the file, use the commands


uncompress csml.tar.Z
tar -xf csml.tar
The package contains:
  • 1. Csml, the compiler for the CSML language.
  • 2. Ltd, the compiler for SML, the predecassor to CSML
  • 3. Smc, a program for composing modules generated by CSML
  • 4. Mcb, the CTL model checker
  • 5. Examples, a collection of CSML and SML examples from various papers
  • Each source directory contains a file READ.ME which describes how to build the program(s). Particular attention should be paid to the directions for compiling csml. The CSML compiler uses a macro preprocessor called ltdmac, which in turn uses the C language preprocessor cpp. In the makefile there is a definition which tells ltdmac where to find cpp on your system. This should ordinarily be set to /lib/cpp. Also, the state machine composer program smc has some parameters in its makefile which set limits on the size of the composed state machine. If you want to construct very large state machines, you will want to modify these.

    There is a UNIX manual entry for the CSML compiler in the file csml/csml.1, and for the model checker in smc/smc.1. If you put these files in your man path, you will be able to get some documentation on-line.

    CMU-SCS Model Checking home page