MAGIC Version 0.1 User's Manual

Table of Contents


The general goal of MAGIC is to verify that an implementation conforms to its specification. The implementation is always a C program and hence quite standard. However, MAGIC can be used to play around with several kinds of specifcations and notions of conformance. For a quick overview of how to start using MAGIC, check out the tutorial.

Back to Top

Download and Installation

MAGIC has been successfully installed on RedHat 7.1, RedHat 8.0 and Windows 2K with Cygwin and gcc 3.x. You can obtain the latest MAGIC distribution as a tar.gz file here. Save it in some directory, say "/foo". Depending on the version you download, the tarball will be named magic-x.tar.gz. Unpack the tarball as follows:

$ cd /foo
$ tar xvfz magic-x.tar.gz

You should find a directory called "/foo/magic-x". First set the environment variable MAGICROOT to "/foo/magic-x". If your shell is csh or tcsh you can do it as follows:

$ setenv MAGICROOT /foo/magic-x

If your shell is bash, you can do the same using:

$ export MAGICROOT=/foo/magic-x

If your platform is Windows 2K you can set environment variables via the Control Panel. Next set the enviroment variable OSTYPE. On Linux, OSTYPE must be set to "linux" and on Windows 2K it must be set to "Windows_NT". MAGIC also requires the Simplify theorem prover and the Pseudo-Boolean Solver (PBS) to operate correctly. Further, it expects that these two tools be located in very specific directories. If your platform is Linux, the binaries for these tools must be called Simplify and PBS respectively. Copy them to their required directories as follows:

$ cp Simplify /foo/magic-x/theorem-prover/simplify/Simplify
$ cp PBS /foo/magic-x/pbs/PBS

If your platform is Windows 2K, the binaries must be called Simplify.exe and PBS.exe. They can be copied to their required directories as follows:

$ cp Simplify.exe /foo/magic-x/theorem-prover/simplify/Simplify.exe
$ cp PBS.exe /foo/magic-x/pbs/PBS.exe

Simplify and PBS do not come with the MAGIC distribution by default. However, if you have trouble locating these binaries, email me and I will try to help you out. Finally, compile MAGIC as follows:

$ cd /foo/magic-x
$ make

If the compilation succeeds you will find a binary called "magic" (or "magic.exe" if you are using Cygwin) in the directory "/foo/magic-x/main". Make sure this binary is in your PATH and that the environment variable MAGICROOT is set to "/foo/magic-x" whenever you use MAGIC. It is advisable that you do these automatically via some startup script like .cshrc or.bashrc, or using the Control Panel if your platform is Windows 2K. If you have problems with compilation email me and I will try to send you a binary (I should be able to help you with Linux and Windows 2K). Just save the binary to the file "/foo/magic-x/main/magic". MAGIC comes bundled with a set of simple examples. Once MAGIC is installed, read the "/foo/magic-x/README" file for instructions on how to play around with them. Have fun!!

NOTE: In order to draw its figures MAGIC requires the Graphviz package, and in particular the DOT tool. However, if you do not want to use MAGIC's drawing capabilities, there is no need to install Graphviz. Look at the tutorial for an overview of how to make MAGIC draw.

Back to Top

Precompiled Binaries

We realize that the installation process described above can be quite tedious. If you already have an existing MAGIC installation and would like to simply upgrade to the latest version, you might want to download just the latest MAGIC executable. Here are precompiled binaries of the latest MAGIC release for RedHat 7.1, RedHat 8.0, RedHat 9.0 and Windows 2K. Simply download them and save them as "magic" (or "magic.exe" on Windows 2K) inside the "main" subdirectory.

Caution: These binaries are quite large. Also you must have an existing MAGIC distribution with the proper directory hierarchy, Simplify and PBS installed, and environment variables set as per the installation instructions above. Standalone MAGIC binaries will not work.

Back to Top


MAGIC is, as of yet, a command line based tool. It can be invoked from any standard command shell with appropriate options and input filenames. Here is an overview:
Back to Top

Common Options

Back to Top

Less Used Options

Back to Top