Previous Up Next

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 here.
  1. Download the Blast source distribution.
  2. 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
  3. Enter the blast-2.4/blast directory and run GNU Make to build the distribution.
        cd blast-2.4/blast
        make distclean
        make
  4. 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.

  5. 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, should you 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 and Cvc 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 SMT-LIB compatible theorem prover for its satisfiability queries (cf. release notes).

  6. 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:
        make gui
    This will create the GUI executable blastgui.opt in the directory bin.

  7. 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.

  8. Congratulations! You can now start using Blast.
Previous Up Next