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
