WSAT Installation Instructions

In the following, we assume your operating system is Linux.  The package can also work under Windows, you might need file compression tools (e.g. Winzip, WinRar) to unzip the supporting packages, also you might want unix simulation tools such as Cygwin to support the unix commands such as gcc and grep that are used in the demo.

(i) download and unzip packages.

    (1) download wsatDemo-1.0.tar.gz, extract it using the following commands:

            gunzip wsatDemo-1.0.tar.gz

            tar -xvf wsatDemo-1.0.tar.gz

            After extraction, you will see two directories Classes and SamplesClasses contains one single wsat.jar file, and Samples  contains three sample sets.

    (2) download BPWS4J_2.0 engine from IBM site (DOWNLOAD Logo is on the right-top of the page). You will go through a registration process (which takes a few seconds), and then you will have the access to a list of BPWS4J related products.  The file to download is bpws4j-engine-2.0.zip, which is located at the bottom of the list.  Unzip bpwsrj-engine-2.0.zip into the directory wsatDemo-1.0/Classes.       

    (3) download java_cup_v10k.zip from http://www.cs.princeton.edu/~appel/modern/java/CUP/ , put the file java_cup_v10k.zip into the directory wsatDemo-1.0/Classes.

    By now, you should have the following jar files in the wsatDemo-1.0/Classes directory: wsat.jar, java_cup_v10k.zip, bpws4j.jar, wsdl4j.jar, xml-apis.jar, bpws4j-samplesjar, log4j.jar, soap.jar, xalan.jar, qname.jar, xercesImpl.jar.

    (4) download SPIN model checker binary code from http://spinroot.com/spin/Bin/index.html . (The file should be spin420.exe and spin420_linux for windows and linux users respectively.  In the later demo, we use "spin" to refer to the corresponding spin420 file in your system.  You might want to rename spin420yyy to "spin" and set the environment PATH in your system to save your keystrokes.)

(ii) set CLASSPATH

    Suppose wsatDemo-1.0.tar.gz is extracted to the directory mydir/wsatDemo-1.0.  In your shell resource files (e.g. .tcshrc, .cshrc) files, add one line:

    setenv CLASSPATH your_old_classpath:mydir/wsatDemo-1.0/Classes/wsat.jar

   (FOR WINDOWS/XP USERS: control panel -> system -> advanced -> environment variables, add or update the CLASSPATH variable)

(iii) test installation

    Go to any directory, type "java wsat -h", you should get the command usage statement of the tool.  If you get the ClassNotFound error, you should double-check your CLASSPATH setting.