source: CIVL/INSTALL@ bfdacccd

                    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 <filename>".  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".