|MTT 1.5 (The Maude Termination 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:
AProVE is available at http://www-i2.informatik.rwth-aachen.de/AProVE/. The Termination Competition version (for linux) is available here. Use the runme script as executable. Download the files aprove.jar and runme (for linux, modify it if in a different platform) in the same directory.
MuTerm is available at http://www.dsic.upv.es/~slucas/csr/termination/muterm/. We recommend MuTerm 4.4. The Termination Competition version (for linux) is available here. Use the runme script as executable. Download the files muterm, bc2sat, sat, and runme (for linux, modify it if in a different platform) in the same directory.
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.
Check the MTT bench for several sample files and results using different alternative options.
New features available in MTT 1.3:
New features available in MTT 1.2:
|Please, send any comments or questions to||18/02/2008|