Changes between Version 5 and Version 6 of Introduction

Timestamp:

12/28/18 19:31:49 (7 years ago)

Author:

siegel

Comment:

--

Introduction

@@ -32 +32 @@
 == Installation and Quick Start ==
 
-# Install the automated theorem prover CVC4, following instructions at http://cvc4.cs.stanford.edu/web/.  You only need the binary (`cvc4`), which must be in your `PATH`.
-# Install the automated theorem prover Z3, following instructions at https://github.com/Z3Prover/z3.  You only need the binary (`z3`), which must be in your `PATH`.
-# Install a Java 8 SDK.   Later versions of Java may also work.  See https://www.oracle.com/technetwork/java/javase/downloads/index.html.
-# Download and unpack the latest stable release of CIVL from http://vsl.cis.udel.edu/lib/sw/civl/current/latest/release/.
+1. Install the automated theorem prover CVC4, following instructions at http://cvc4.cs.stanford.edu/web/.  You only need the binary (`cvc4`), which must be in your `PATH`.
+1. Install the automated theorem prover Z3, following instructions at https://github.com/Z3Prover/z3.  You only need the binary (`z3`), which must be in your `PATH`.
+1. Install a Java 8 SDK.   Later versions of Java may also work.  See https://www.oracle.com/technetwork/java/javase/downloads/index.html.
+1. Download and unpack the latest stable release of CIVL from http://vsl.cis.udel.edu/lib/sw/civl/current/latest/release/.
+1. The resulting directory should be named CIVL-tag for some string tag which identifies the version of CIVL you downloaded. Move this directory wherever you like.
+1. The JAR file in the `lib` directory is all you need to run CIVL. You may move this JAR file wherever you want. You run CIVL by typing a command of the form `java -jar /path/to/civl-TAG.jar ...`. For convenience, you may instead use the shell script `civl` included in the `bin` directory. This allows you to replace `java -jar /path/to/civl-TAG.jar` with just `civl` on the command line. Simply edit the `civl` script to reflect the path to the JAR file and place the script somewhere in your `PATH`.  In the following, we assume you have done this.
+1. From the command line, type `civl help`. You should see a help message describing the command line syntax.
+1. From the command line, type `civl config`. This should report that cvc4 and z3 were found, and it should create a file named `.sarl` in your home directory.
 
+To test your installation, copy the file `examples/concurrency/locksBad.cvl` to your working directory. Look at the program: it is a simple 2-process program with two shared variables used as locks. The two processes try to obtain the locks in opposite order, which can lead to a deadlock if both processes obtain their first lock before either obtains the second. Type `civl verify locksBad.cvl`. You should see some output culminating in a message 
+
+`The program MAY NOT be correct.  See CIVLREP/locksBad_log.txt.`
+
+Type `civl replay locksBad.cvl`. You should see a step-by-step account of how the program arrived at the deadlock.