source: CIVL/INSTALL@ 1a3834b

                    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 prerequisite projects ABC, SARL and GMC. 
   Make sure that the three projects are put in the same 
   directory "workspace" (you can use any other name).

        a. 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.
        
        b. 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.

        c. 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.

2. 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.)

3. 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.

4. Link prerequisite projects (ABC, SARL, GMC) to CIVL project.
Select the project CIVL, right click, and select "Properties".
In the Properties window, click Java Build Path on the left, 
and go to the tab “Projects”. Click Add…, and choose the projects
 “ABC”, “GMC” and “SARL”, then click OK.

5. Download and prepare dependent packages.

        a. If you are using 64-bit mac os, download the tgz archives from 
           http://vsl.cis.udel.edu/tools/vsl_depend_osx.tgz 
           and unzip it some where on your system. 

        b. Otherwise, point your web browser to http://vsl.cis.udel.edu/tools 
           and download the following:
                        hamcrest-core-1.3.jar
                        jacoco.tgz
                        junit-4.11.jar
           Put these files somewhere on your system and untar the Jacoco archive 

6. Create a file named build.properties in the directory where build.xml is in. 
This is not needed by Eclipse, but you will want to use Ant to build the jar 
and other things.

        a. If you are using 64-bit mac os, copy and paste the content from 
           properties/build.properties.osx. Edit the entry "root" to point to the 
           corresponding directory that you download at step 6.a. 
        
        b. Otherwise, copy and edit one of the examples in the properties directory. 
           Edit each entry to point to the corresponding items you downloaded in step 6.b.

7. The platform-specific information are handled in Eclipse by defining Classpath variables.  

        a. If you have put all dependent packages in one directory 
           (http://vsl.cis.udel.edu/tools/vsl_depend_osx.tgz), there is 
           only one class path variable that needs to be modified. 
           Go to Preferences -> Java -> Build Path -> Classpath Variables, 
           and edit the entry “VSL_DEPEND” to point to the directory 
           where you put the dependent packages.
        
        b. Otherwise, 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.

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