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:

• MTT 5 can check the termination of rewrite theories, and not only membership equational theories (like previous versions). There are still several restrictions in the Maude specification to be checked though:
• built-ins cannot be used,
• attributes owise and identity elements are not supported, 
• the specification must be in Full Maude notation (each module must be enclosed in parentheses and operator declarations must be in their single-token equivalent form, see the Maude official web site for further information).
• MTT 5 can use as back-end tool any termination tool supporting the TPDB syntax and following the rules for the Termination Competition (the executables of the tools that participated in the Termination Competition 2007 are available in its results section). In previous versions MTT it was able to interact with CiME, AProVE, and MuTerm, but now other formal tools, such as TTT, Termptation, etc. can be considered as well. In the MTT environment, Maude specifications can be proved terminating by using (any of these) distinct formal tools, allowing the user to choose the most appropriate tool for each particular case, a combination of them, or trying different alternatives in the case of a particular tool not being able to find a proof. 
• Moreover, MTT 5 provides a number of alternative transformations, between which one can choose the more appropriate for each particular case. Thus, one can proof the termination of a Maude specification by transforming a sugared rewrite theory (SRWT) into a context-sensitive term rewrite theory (CS-TRS), which can be handled by tools like AProVE and MuTerm combining different transformations. The complete set of transformations is shown in the following figure:
  
  
  
  Thus, e.g., a context-sensitive membership conditional term rewriting system (CS-MCTRS) can be transformed into a context-sensitive conditional term rewriting system (CS-CTRS) by using transformation A (which can be complete, discarding information on kinds Uk, or discarding all information on sorts U), or into a context-sensitive order-sorted conditional term rewriting system (CS-OSCTRS) by using the transformation OS. See [DLMMU04] and [...] for details. 

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. 

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:

• Maude is available at http://maude.cs.uiuc.edu. Use Maude 2.3 (or later) and Full Maude 2.3 (or later, the last version of Full Maude is available here).

• 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.

• Similarly for other back-end termination tools.

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. 

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

New features available in MTT 1.3:

• The declaration and rule for the equal operator is included only if used.
• The transformation from Unconditional to Conditional Rewrite Theory has been improved (arguments of the U operators have been optimized).
• Polymorphic operators are supported.
• Several bugs have been fixed.
• It also includes some minor cosmetic changes related to the user interface.

Files:

• MTT.jar
• MTT-transformations.1.3.maude
• Source files
• On its installation.
• You can find here a few very simple examples of how to use the tool. A test suite can be found here.

New features available in MTT 1.2:

• MTT 1.2 runs on Maude 2.2.
• AProVE can now be used as back-end tool for proving the termination of your specifications. You need the tool's jar file (get it from its web site).
• MTT 1.2 is a bit more robust and user friendly (give some additional information when crashes and is able to recover from some situations). It is still quite unstable though.
• The user has now some additional control (he can choose on whether using the and optimization, can choose not to use some of the termination tools, etc.)

Files:

• MTT.jar
• MTT-transformations.1.2.maude.tar.gz
• samples.tar.gz
• MTT 1.2 sources

Please, send any comments or questions to

18/02/2008