Grez

Grez is a tool which searches for a proof that a given graph transformation system terminates (or not). For this, it uses a variety of techniques, in particular the type graph technique, as described in this paper (published 2014 in the IFIP-TCS conference proceedings).

Grez is written in Java. It should run on any computer with a Java runtime environment installed (version 8 or newer); we recommend Oracle's JRE (OpenJDK also works, but seems to have graphics glitches on some systems).

All external libraries required by Grez are included in the grez.jar file. If you want to compile and run the source code, the following external libraries are required:

• Google Guava, tested with version 14
• ANTLR 4, used for parsing output from external SMT solvers

For generating PDF reports, Grez calls the external pdflatex program. For this functionality, you need a working LaTeX distribution (including common LaTeX packages). The pdflatex program must be in the operating system's search path.

Grez User Manual

Please read the user manual to learn how to use Grez. Below are a few pointers on how the tool can be used.

Running Grez

In most operating systems, double-clicking on the grez.jar file will open Grez in GUI-mode. Using the GUI, the user can interactively select which search algorithm will be used and with which parameters, and inspect the termination and non-termination proofs found by the program.

To run the program from the command line, change to the directory where grez.jar is located, and type:

java -jar grez.jar

Input format

Graph transformation systems are written in a text-based input format (for now, even the GUI does not offer editing capabilities). A formal specification of the input format is given in the manual, but looking at the examples will give you enough info to start writing your own.

File	Description
grez.jar	Executable JAR-file
grez-src.jar	JAR file containing sources (requires external libraries to build)
grez-examples.zip	ZIP file with example GTSs
grez-manual.pdf	The Grez user manual

Grez is developed and maintained by H.J. Sander Bruggink.

Grez is currently in beta stage. If you find any bugs or other unexpected behavior, please send me an e-mail.

Of course, the software is provided "as-is", without any implied or expressed warranty of any kind. So don't sue me if it doesn't work as expected.