Installing Hybrid SAL
The Hybrid SAL documentation is a little sparse, and its install scripts are rather fragile. Here's a simple list of steps to get Hybrid SAL running on a Linux machine.
- Install Java. You're own your own for this step, I'm afraid. The usual place to go is http://java.sun.com
- Install the Antlr parser generator. You need version 2.7.1, which you can get and install as follows
wget http://www.antlr2.org/download/antlr-2.7.1.tar.gz tar xzf antlr-2.7.1.tar.gz
- Download Hybrid SAL and get the parser working.
wget http://sal.csl.sri.com/hybridsal/hybridsal-lite.tgz tar xzf hybridsal-lite.tgz cd hybridsal-lite/hybridsal2xml/
Next you need to modify your path to include the directory above. How you do this depends on the shell that you use. Then type the following; you need to substitute the path to the directory where you downloaded Antlr
./install.sh <PATH TO ANTLR>/antlr-2.7.1
You should see a dozen lines or so of output, ending with
hybridsal2xml installation successfully tested Testing complete.
- Get the Lisp part working. You need a running Lisp environment and one way to do this is to use the Lisp environment of PVS.
- So, if you haven't got it already, first install PVS.
Next, go to the directory that contains Hybrid SAL and start PVS there.
cd hybridsal-lite pvs
Go to the PVS Lisp buffer by typing the following to the PVS Emacs
C-x b *pvs*
Go to the bottom of the buffer (type M->) and then type
(in-package :cl-user) (load "load.lisp")
The first time you do this, the Hybrid SAL lisp files will be compiled.
To make sure it's working, run some simple examples:
- Use Hybrid SAL by invoking its Lisp functions in the PVS Lisp window. See the README in the examples directory, and read the documentation from the link on the Hybrid SAL web page.
Hybrid SAL files will be read from whatever directory you name in the command (and the parsed .xml files will be written back there); abstracted SAL files will be written to the current directory (i.e., hybridsal-lite). You'll need to have regular SAL installed to analyze the abstracted models generated by Hybrid SAL. Note that you'll get an error message when you quit PVS (by C-x C-c); you'll need to force it.