2 Download and Installation
Blast can be downloaded from Blast's download web page.
2.1 Downloading Binaries
You can download executable versions of Blast for Linux and
Windows with Cygwin.
You should independently download and install the
Simplify Theorem Prover (see item 5
below). Blast requires that the Simplify theorem prover is in the path.
2.2 Downloading the Source Distribution
You will need OCaml to build Blast.
Blast has been tested on Linux and on Windows with Cygwin.
If you want to use Blast on Windows then you must get a complete installation
of Cygwin and the source-code OCaml distribution and compile it yourself
using the Cygwin tools (as opposed to getting the Win32 native-code version of
OCaml). If you have not done this before then take a look
Download the Blast source distribution.
- Unzip and untar the source distribution. This will create a directory
called blast-2.4 whose structure is explained below.
tar xvfz blast-2.4.tar.gz
- Enter the blast-2.4/blast directory and run
GNU Make to build the distribution.
- You should now find the executables pblast.opt and spec.opt in the directory bin.
These are symbolic links to files of the same name in the directory psrc and spec, respectively.
The executable pblast.opt is the Blast model checker, the executable spec.opt is
the specification instrumenter.
- You should also download and install the
Simplify Theorem Prover.
This involves putting the
executables Simplify (Linux)
or Simplify.exe (Windows) in the bin directory.
Additionally, Blast has interfaces to the Cvc Theorem Prover,
wish to install and use this tool for theorem prover calls.
Again, this involves putting the executable for Cvc in the bin directory.
Note that in order for Blast to use Simplify or Cvc, the executable for Simplify
must be in your current path.
It is a good idea to add the Blast bin directory to your path.
Blast can also use any other
compatible theorem prover for its satisfiability queries
(cf. release notes).
- Blast also comes with an independent GUI. In order to install the GUI, you must download and
install the LablGTK package
in addition to Ocaml. After you have installed LablGTK, you can build the GUI by going to the
blast-2.4 directory and typing:
This will create the GUI executable blastgui.opt in the directory bin.
- Blast (actually the GUI) requires the use of the environment variable BLASTHOME.
Therefore you should set the environment variable BLASTHOME to point to the directory
blast-2.4/blast where you have downloaded Blast.
- Congratulations! You can now start using Blast.