The following instructions should aid in installing PV on UNIX machines. These have been tested on Solaris 5.7 (Sun architecture), and RedHat Linux 6.2-7.3 (i386).

1. You will need GCC or some ANSI C compiler. Many already have some sort of C compiler installed on their machine. In the event that you do not, GNU's GCC can be obtained from http://www.gnu.org/software/gcc directly. Here you will find the latest release along with information regarding installation on all supported platforms.

2. We must assume that you have a good collection of the standard UNIX utilities such as gunzip, tar, lex, yacc, make, etc. If you do not, they are freely available from http://www.gnu.org.

3. Tcl/Tk. This is necessary for the graphical user interface xpv02. The latest version of Tcl/Tk is freely available from http://dev.scriptics.com/software/tcltk/. The latest version should be compatible with our interface, although we tested xpv02 on Tcl/Tk 8.3. Again installation information should be available on all supported platforms.

4. Insure that GCC, Lex, Yacc, and Wish are in your search path.

5. If you intend to use Parallel PV for safety model-checking some additional requirements are necessary and are listed below. If not, proceed to the next step.

   Assumptions:

   1. Parallel PV assumes that all of the machines in the computational cluster will be running Linux on i386 based machines. We have also used Parallel PV with FreeBSD on i386 machines with some minor changes. I recommend RedHat Linux 7.2 or later.

   2. Parallel PV assumes that the machines that will be used in the compuational cluster have a shared filesystem. It is also assumed that the model checking program is run from a location on the filesystem that is accessable by all nodes in the computation.

   3. Parallel PV assumes that every machine in the computational cluster has the ability to make and recieve connections either through rsh and rshd or ssh and sshd. Our development and testing has been done with ssh and sshd. I recommend setting up your ssh client so you don't have to type your password all the time as outlined in the userguide to MPICH.

   4. Parallel PV assumes that the MPICH implementation of the MPI interface has been installed on the master node of the computational cluster. The master node is the node from which the model-checking program will be initiated.

   5. Do not use Lam/MPI that comes with Linux.

6. Download pv.tar.gz from our web site.
   

7. Move the archive to the directory where you would like to keep your installation. Then Gunzip and untar the file. I used these commands:

   ->tar -xzvf pv.tar.zip

8. Change to the directory where the source is kept.

   ->cd pv/src

9. Once in the src directory type " make ". (Without the quotation marks.) PV should compile with no errors.

   ->make

10. xpv02 is located in the pv directory. The first line of xpv02 looks something like: #!/usr/bin/wish -f . You will need to change this path to be consistent with the location of wish on your machine. One way to find this information is:

    ->which wish

11. Your compiler must be able to find the root directory of your PV distribution. This is so the "include" directory included with your package can be properly accessed. If you plan to compile your model-checking binaries somewhere other than the root directory of your PV distribution then please take steps to be able to access the "include" directory.

12. To use PV with xpv02, simply copy the pv executable into the same directory with xpv02.

13. Parallel PV is accessable from the graphical user interface.