On the installation of MTT 1.3 |
MTT is written in Java, you just need a single jar file to execute it (MTT.jar for JVM 1.5.0). The tool however uses Maude to do part of the transformations, and the tools CiME, AProVE, and MuTerm to do further transformations and checking the termination of the specifications.
The tool will try to load the file with the Maude specification of the transformations (MTT-transformations.1.3.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, CiME, AProVE, and MuTerm to be available in the system:
Maude is available at http://maude.cs.uiuc.edu. Use Maude 2.2 and Full Maude 2.2.a.
CiME is available at http://cime.lri.fr. We recomend CiME 2.02.
AProVE is available at http://www-i2.informatik.rwth-aachen.de/AProVE/. We recomend AProVE 1.2.
MuTerm is available at http://www.dsic.upv.es/~slucas/csr/termination/muterm/. Although the last version available is 4.0, we can only interact with previous versions (with no graphical interface). We recomend MuTerm 3.1. Follow the instructions in its web site for its installation. It is written in Haskell, and therefore you will need having a Haskell interpreter (we have tried Hugs98) running in your system.
To execute MTT one just type
java -jar MTT.jar
The first time MTT is executed you get into a configuration menu in which one must indicate the location of each of the tools and required files. All this information is saved in a configuration file MTT.cfg (click here for a sample file). If the configuration file is detected when started, the configuration is read from this file. One can later change the configuration of the tools by editing the configuration file or through the Edit -> Preferences... menu.
To alleviate the requirements on external tools, the application has the possibility of not connecting to those tools we are not interesting in using, and also includes support to connect to the external tools (Maude, CiME, or MuTerm---this facility is not available for AProVE yet) remotely. That is, the tool can interact with a local copy of the tool, which it internally executes, or with a remote copy of it. This feature is particularly attractive for those platforms for which there is no version available of some of the tools (including Maude itself). For example, one may be running MTT on a Windows box which connects to the external tools running on different machines. Any configuration is possible, if versions available fro the corresponding platforms. For example, MuTerm may be running on a Windows machine, CiME on a linux box, and Maude on a Solaris platform. Of course, the Java Runtime Environment is required for the execution of the jar file.
MTT cannot execute the tools on a different machine. What we do is to execute a tool server (a tool wrapper with which we interact via sockets) for the tool. Such tool servers can run on the same machine or in different machines. We give it a port on which it will be listening for connections. Of course, the system on which we start the tool server must have the tool available.
The tool server (ToolServer) is also written in Java (ToolServer.jar for JVM 1.5.0).
We can start a tool server with the following command:
java -jar ToolServer <tool> <port> <parameters_of_the_tool>
where <tool> is either Maude, CiME, or MuTerm, <port> is the port on which the tool server will be listening for connections, and <parameters_of_the_tool> are the parameters of the tools. Thus, we have the three possible cases:
java -jar ToolServer CiME <port> <CiME_location>
java -jar ToolServer Maude <port> <Maude_location> <FullMaude_location> <transf_file_location>
java -jar ToolServer MuTerm <port> <Haskell_location> <MuTerm_location>
Examples of use:
java -jar ToolServer CiME 60000 ~/cime2.02/cime
java -jar ToolServer Maude 61000 ~/alpha86a/maude.linux ~/fm212i/fm212i.maude ~/MTT-transf.maude
java -jar ToolServer MuTerm 62000 hugs ~/MU-TERM-3.0/MuTerm/MuTerm.hs