MTT 1.5 (The Maude Termination Tool)

The MTT has been integrated inside the Maude Formal Environment. You may want to check the MFE web site to get the latest version of this tool.

MTT (Maude Termination Tool) is a tool that checks the termination of Maude equational specifications. Our current prototype tool MTT 1.5 takes Maude programs as inputs and tries to prove them terminating by using existing termination tools as back-end. 

MTT 5 includes several new features:

The tool implementation clearly distinguishes two parts: (1) a Maude specification implements the theory transformations, and (2) a Java application connects Maude and the back-end tools, and provides a graphical user interface. The following figure shows the current interactions between the tools.

The Java application is in charge of sending the Maude specification introduced by the user to Maude to perform transformations; depending on the selections, one transformation or another will be accomplished. The resulting unsorted unconditional rewriting system obtained from such transformations may be proved terminating by using any of the back-end tools available. The tool's output is given as result. Optionally, the intermediate specifications can be shown. 

 

On the installation of MTT 1.5

MTT is written in Java, you just need a single jar file to execute it (MTT.jar for JVM 1.5.0 or later). The tool however uses Maude to do part of the transformations, and termination tools, like CiME, AProVE, MuTerm, etc., to checking the termination of the specifications.

The tool will try to load the file with the Maude specification of the transformations (MTT-transformations.1.5d.maude) into Maude. You can copy it anywhere in your file system. You can indicate where it is located in the configuration menu.

MTT requires Maude and at least on back-end tool to be available in the system:

To execute MTT one just type

java -jar MTT5.jar

The first time MTT is executed you get into a configuration menu in which one must, at least, indicate the location of Maude. The back-end tools can be configured at (the first) start-up, or later using the Edit -> Preferences... menu. All this information is saved in a configuration file MTT.cfg (click here for a sample file; this cfg file should not be modified manually). If the configuration file is detected when started, the configuration is read from this file. 

To install a termination tool, go to the preferences menu (Edit -> preferences) and click on "Add tool". Give a name for it, click the accept button, and then select its panel to give the path of the runme file.
Samples

Check the MTT bench for several sample files and results using different alternative options.

Previous versions
MTT 1.3

New features available in MTT 1.3:

Files:

MTT 1.2

New features available in MTT 1.2:

Files:

 
Please, send any comments or questions to   18/02/2008