********************************************************************* Copyright (c) 1997-2003 Massachusetts Institute of Technology. All Rights Reserved. Included in this package are libraries that are open source but governed by specific licenses. For full information on use and distribution of this Toolkit, please see the included "copyright-notice" file. For the rest of the Toolkit: MIT grants permission to use, copy, modify, and distribute this software and its documentation for NON-COMMERCIAL purposes and without fee, provided that this copyright notice appears in all copies. MIT provides this software "as is", without representations or warranties of any kind, either expressed or implied, including but not limited to the implied warranties of merchantability, fitness for a particular purpose, and noninfringement. MIT shall not be liable for any damages arising from any use of this software. ********************************************************************* IOA Toolkit ********************************************************************* This file describes how to use the IOA Toolkit. The file README.{NAME}-distrib, located in this directory, describes which distribution of the Toolkit this file is part of (with {NAME} replaced by whatever distribution this is). The main sections deal with setting up and running the Toolkit for all distributions. Users of binary-only distributions need only read these sections. There are appendices specific to compiling the Toolkit; for environment setup on machines at LCS under the theory domain; and for CVS local/remote checkouts. Any inquiries about the IOA language or toolset should be directed to . Table of contents ================= 1) Setting up path and environment variables 2) Installing the Toolkit 3) Running and testing 4) File and directory listing Appendix A) Building the Toolkit with a source distribution Appendix B) Setting up for machines at LCS under theory domain Appendix C) Setting up for CVS checkouts on theory machines Appendix D) Setting up for remote CVS checkouts on non-theory machines Appendix E) Known bugs 1) Setting up path and environment variables --------------------------------------------- To run the IOA Toolkit, you minimally need the following programs: Program Where to find it Java runtime version 1.4 java.sun.com/j2se gnumake (as your make program) www.gnu.org Linux systems come with gnumake by default, and many modern systems also feature JDK 1.3 as the default Java runtime. The following environment variables must then be set: Variable name Value it should be IOAROOT The location of the IOA_Toolkit directory JDKHOME Directory where JDK 1.4 is (such that ${JDKHOME}/bin contains java and javac) path To include ${JDKHOME}/bin If desired, include ${IOAROOT}/bin to access IOA tools from command line You can set the capitalized variables using the "setenv" command in csh or the "export" command in bash. For example: setenv IOAROOT ~/research/IOA_Toolkit export IOAROOT=~/research/IOA_Toolkit The uncapitalized variables are set with the "set" command in both shells: set path=~/research/IOA_Toolkit/bin;${path} 2) Installing the Toolkit ------------------------- IOA_Toolkit/bin contains the file ioa.jar which has all the Java byte code needed to run IOA tools. However, the bin directory is also set up to create easy shell scripts that automatically load Java with the correct classpaths. To use them: > cd IOA_Toolkit > make install This will go into the bin directory to create the scripts (as shown below). It will also create a .ioarc file in your home directory that tells the Toolkit where certain libraries are. You only need to do this once, unless you move your IOA_Toolkit directory. In this case, you need to remake them by typing: > cd IOA_Toolkit/bin > make clean > make 3) Running and testing ---------------------- The IOA Toolkit programs consist of a "frontend" and many "backend" programs. The frontend is in charge of syntax checking and generating an "intermediate language" (IL) file format that backend tools can use. Each backend tool serves a different purpose. Each of the following commands is actually a shell script that accesses the ioa.jar file. To run the front end: > ioaCheck IOA Checker, August 13, 2003 Usage ioaCheck [option ...] source-file ... Options -il translate to intermediate language -x expand composite automata** -desug desugar primitive automata** -components output component automata -lp produce input files for the Larch Prover (LSL only) -p prettyprint source files -path use to find source files (default '.') -sorts print sorts in first source file (LSL only) -syms print symbols in first source file (LSL only) -debug print debugging information -verbose print verbose debugging information **Feature under development. Current implementation is known to be wrong. Running ioaCheck with the -il option produces intermediate language (IL) files. Without the -il option, the frontend merely syntax checks. The simulator can be run by typing: > sim usage: sim [flags] <# steps> [] For composite simulations, the (IOA) file should contain the specifications of all component automata and the composite automaton. The parameter must match the name of the composite automaton. With no arguments sim will display its usage information including flags that customize the simulation of a composite automaton. Paired simulation can be done with psim. The number of steps to simulate, implementing automaton (implAut), the specification automaton (specAut), and the Intermediate Language file name are passed as arguments to psim. Psim supports a number of optional flags. With no arguments psim will display its usage information including a list of these flags. > psim usage: psim [flags] The IOA to LSL converter can be run by typing: > il2lsl Usage: il2lsl source-file ... The IOA to Isar converter can be run by typing: > il2isar Usage: il2isar source-file ... There is also a handy program to turn .ioa and .lsl files into .tex files for LaTeX: > texify Usage: java ioa.texify.texify -ioa < filename.ioa or: java ioa.texify.texify -lsl < filename.lsl You need to pipe the IOA filename to texify because it assumes input comes from stdin. To run test files, go to IOA_Toolkit/Test for test examples of ioa programs and intended (".goal") output for each. If the tests work for you, you have successfully made the Toolkit. More relevant examples can be found in the Examples directory. 4) File and directory listing ----------------------------- These are with reference to the top level directory File/directory name Description README This file. README.{NAME}-distrib Description of current distribution where {NAME} is the distribution name Doc Documentation for the Toolkit including the IOA manual and various papers. Test Regression testing code and examples for tools Examples Other example IOA programs bin Scripts and .jar for running tools ioa-mode.el Emacs .el file for fontifying IOA programs lp-mode.el Emacs .el file for fontifying LP scripts copyright-notice Copyright notices of the tools used Appendix A) Building the Toolkit with a source distribution ------------------------------------------------------------ The source code distribution of the Toolkit requires a few more environment variables and contains extra directories. The following environment variables are required: Variable name Value it should be IOAROOT The location of the IOA_Toolkit directory JDKHOME Directory where JDK 1.4 is (such that ${JDKHOME}/bin contains java and javac) PJHOME PolyJ 1.0.2 compiler directory path In addition to ${JDKHOME}/bin, include ${PJHOME}. If you have the Jikes compiler, include its path here too. Make sure your make program is gnumake. To build the Toolkit totally, you should have PolyJ and Jikes. PolyJ former is available at http://www.pmg.lcs.mit.edu/polyj/ and is used to build the frontend. If you cannot obtain PolyJ, the Toolkit will still compile (but with a special flag). However, you will not be able to change any part of the frontend (in other words, we've included .class files from the frontend). Jikes is simply a faster Java compiler that enables us to compile all the Toolkit at once without generating dependencies. It can be substituted by Javac with a special flag. There are more files in the source distribution: File/directory name Description README This file. README.{NAME}-distrib Description of current distribution where {NAME} is the distribution name TODO IOA to-do and done lists Code All source for the Toolkit, plus .class files. Also root of the PolyJ class hierarchy. Doc Documentation for the Toolkit including the IOA manual, various papers and files related to building the Toolkit. Makefile Main makefile that recursively compiles the Toolkit Test Regression testing code and examples for tools. The source distribution contains the full set of tests. Examples Other example IOA programs bin Scripts and .jar for running tools. In the source distribution, library .jar files are separated out of the ioa.jar file. javadoc Javadoc documentation for the source code. ioa.el Emacs .el file for fontifying Javadoc used in IOA source code ioa-mode.el Emacs .el file for fontifying IOA programs lp-mode.el Emacs .el file for fontifying LP scripts copyright-notice Copyright notices of the tools used distrib Directory for generating distributions, such as this one. Further distributions can be generated from this directory. Installation is slightly different too now. Since the .class and javadoc are pre-made for convenience, you don't have to compile to actually use the tools and doing: > cd IOA_Toolkit > make install will work as before. There are two (nearly invisible) differences. Instead of just using ioa.jar, the shell scripts created now source from three library .jar files. Also, the shell scripts use the ioa.jar file, which has to be explicitly recompiled from the .class files in the Code/classes directory. To use the .class instead, there are the "no-jar" versions of the scripts. For example, > ioaChecknj will run the frontend directly from the .class files. To recompile, you can go to the top level IOA_Toolkit directory and type: > make If you just want to recompile the code (without the javadoc or the remaking of the ioa.jar file) you can do this in the Code directory. If you do not have PolyJ, you have to instead type: > cd IOA_Toolkit/Code/ioa > make noPolyj This only recompiles the backend files. If you do not have Jikes, you have to change the Code/ioa/Make.basics file such that the line: JIKES = jikes +E becomes JIKES = javac To run test files, go to IOA_Toolkit/Test and type "make" for a list of options. There are options such as "sim" for running tests for the simulator, and "add" for adding a new test case. Appendix B) Setting up for machines at LCS under theory domain --------------------------------------------------------------- If you work from theory machines at LCS, a lot of the environment setup is predetermined. You can mostly source the .cshrc file in the IOA_Toolkit directory. The actual values are: Variable Value IOAROOT User-dependent JDKHOME /e/IOA/site/jdk1.3 PJHOME /e/IOA/site/polyj-1.0.2/guavac/compiler path Include ${JDKHOME}/bin, ${PJHOME} and /e/IOA/bin (Jikes is already included in /usr/bin) Append ${JDKHOME}/bin to the front of your path so that jdk1.3 is the default version. Theory machines use gnumake by default. For convenience, you may want to add the following two lines to your .cvsrc file in your home directory: cvs -e /usr/bin/emacs update -d -P The first makes sure that you use emacs to edit your commit logs, and the second creates directories when you update if new directories are created in the repository. If you don't have a .cvsrc file, just create one. Appendix C) Setting up for CVS checkouts on theory machines ----------------------------------------------------------- The main repository of the IOA Toolkit is kept under GNU's Concurrent Versions System (CVS) on LCS's theory server. To access the IOA CVS repository, you need to have been given write permission to the CVS root directory, which is /e/IOA/cvcsroot. Go to the directory where you want to put the Toolkit and then type: > cvs -d /e/IOA/cvsroot checkout IOA_Toolkit This will create an IOA_Toolkit directory that will contain the Toolkit. From then on you can use regular CVS commands in that directory (and its subdirectories) without the -d flag. You can find out more about CVS at . A CVS checkout distribution will include every file related to the IOA Toolkit. This means all the test cases, along with sources for some of the manuals. Appendix D) Setting up for remote CVS checkouts on non-theory machines ---------------------------------------------------------------------- If you are doing a CVS checkout, you must already have an account (and proper permissions) on the theory.lcs machines. The following additional variable is required: Variable name Value it should be CVS_RSH ssh What we want to do is set up CVS to use SSH to log onto a theory machine, but make the SSH part of it smart so you only have to type in your password once every session. First, to establish a checkout, type (in the desired directory): > cvs -d user@theory.lcs.mit.edu:/e/IOA/cvsroot checkout IOA_Toolkit Just replace "user" with your username on theory. You will be asked for a password this time, but this is just an initial setup. You now have the equivalent of a CVS checkout on a theory.lcs machine in Appendix C, but you will need to set up your environment for building as in Appendix A. Future CVS commands should automatically work from the directory without the "-d user..." flag, but you will be prompted for a password every time. The rest of this section deals with avoiding this password hassle. 1) Set up ssh If you don't have ssh set up to use RSA keys you can do this simply with the following. On your home machine: > cd ~ > ssh-keygen > cp .ssh/identity.pub .ssh/authorized_keys > scp -r .ssh user@theory.lcs.mit.edu:~/.ssh 2) Run ssh-agent to handle authentication Every time you login, you want to create an ssh-agent so that when CVS routes commands through SSH, no password is required. > ssh-agent tcsh > ssh-add You can replace "tcsh" by your favorite shell. If prompted for a passphrase, enter the one you put in for ssh-keygen. Now you should be able to run cvs commands on the home machine just as if you were logged into a theory machine. You can automate this step in the future by including the above two lines in your .cshrc file. [If this doesn't work, you may need to set your home directory permissions to something Draconian like: drwx--x--x (chmod ~ 711). Also try ssh -v to debug the connection. ] E) Known bugs -------------- As of today, the frontend only builds under Linux. This is due to an unfortunate bug in the current PolyJ implementation on Solaris. The rest of the Toolkit, being in Java, should build on any JDK 1.3 platform.