CIVL Installation Instructions ------------------------- Binary Distribution ------------------------- For most users, this will be the easiest way to install and use CIVL. 1. Install a Java 7 SDK if you have not already. Go to http://www.oracle.com/technetwork/java/javase/downloads/ for the latest from Oracle. On linux, you can optionally sudo apt-get install openjdk-7-jdk. 2. Download the approrpriate complete binary distribution from http://vsl.cis.udel.edu/civl. 3. Unzip and untar the downloaded file if this does not happen automatically. This should result in a folder named CIVL-TAG, where TAG is some version id string. This folder contains the following: - README : this file - bin : containing one executable sh script called "civl" - lib : containing civl-TAG.jar and native libraries used by CIVL - doc : containing some documentation about CIVL - licenses : licenses for CIVL and included libraries - examples : some example CIVL programs 4. For OS X, move the CIVL-TAG folder into /Applications. For linux, move it into /usr/local. 5. Put the civl script in your path however you like to put things in your path. Either move it to a directory in your path, or create a symlink to it, or edit your .profile or equivalent to put it in your path. Now you should be able to run CIVL from the command line by typing "civl ". Type just "civl" for usage information. ------------------------- Source Installation ------------------------- We recommend using the Eclipse IDE for Java/EE developers. 1. Install the C front-end ABC, http://vsl.cis.udel.edu/abc, following the instructions in its INSTALL file for Eclipse installation. This should result in a project named ABC in your Eclipse workspace. Build the abc.jar from within Eclipse by right-clicking (or ctrl-clicking on OS X) on the build.xml file and selecting Run As->Ant Build. 2. Install the symbolic algebra and reasoning library SARL, http://vsl.cis.udel.edu/sarl, following the instructions in its INSTALL file for Eclipse installation. This should result in a project named SARL in your Eclipse workspace. Build the sarl.jar from within Eclipse by right-clicking (or ctrl-clicking) on the build.xml file and selecting Run As->Ant Build. 3. Install the generic model checking utilities package GMC, http://vsl.cis.udel.edu/gmc in Eclipse. This one is pure Java, so is easy. This should result in a project named GMC in your Eclipse workspace. Build the gmc.jar from within Eclipse by right-clicking (or ctrl-clicking) on the build.xml file and selecting Run As->Ant Build. 4. From within Eclipse, select New Project...from SVN. The archive is svn://vsl.cis.udel.edu/civl. After entering that, open it up and select the "trunk". (It is simplest to just check out the trunk for the Eclipse project.) 5. Check out the trunk, and create the project using the New Java Project Wizard as usual, naming it "CIVL". The .project, .classpath, and other Eclipse meta-data are already in the SVN archive, saving you a bunch of work. 6. Create a build.properties file as above. This is not needed by Eclipse, but you will want to use Ant to build the jar and other things. 7. The platform-specific information are handled in Eclipse by defining Classpath variables. Since you already followed the installation directions for ABC and SARL, you should have defined variables ANTLR, ANTLR_SOURCE (optional), CVC3, PCOLLECTIONS, PCOLLECTIONS_SOURCE (optional), and CLD-DS. Now define new variables ABC, SARL, and GMC to point to the jar files in the respective project directories. 8. Do a clean build by selecting "Clean...". 9. Run the JUnit test suite from within Eclipse: Go to Run->Run Configurations.... Create a new JUnit configuration. Name it CIVL Tests. Select "Run all tests in the selected project..." and navigate to the folder "test" in the CIVL project. The Test runner should be JUnit 4. Under the Arguments tab, type "-ea" (without the quotes) in the VM arguments area (to enable assertion checking). Under the Environment tab, add an entry for DYLD_LIBRARY_PATH (OS X) or LD_LIBRARY_PATH (linux). The value for this variable should be a colon-separated list of directories containing the CVC3 and libgmp shared libraries. You might want to put those shared libraries in one directory in a permanent place to simplify things. You can also define another Eclipse variable containing this colon-separated list and use the variable name for the value. You should now be able to run the tests by clicking "Run". 10. An example of how to set up a single test from within Eclipse: create a new Run Configuration via the Run->Run Configurations... menu. Create a new "Java Application" configuration. Call it "CIVL barrier2". The Project is CIVL. The main class is edu.udel.cis.vsl.civl.CIVL. Under the Arguments tab, set the Program arguments to "examples/barrier2.cvl" (without the quotes). Modify the VM arguments and the Environment as in the step above. You should now be able to run the test by clicking "Run".