Instructions for using the Maude Termination Tool

The Maude Termination Tool (MTT) is installed on the CSIL machines in the cs476 home directory /home/class/fa06/cs476. To use MTT, you will need to copy the files from /home/class/fa06/cs476/MTT/ into a directory writable by you, e.g. type cp -R /home/class/fa06/cs476/MTT ~. You also need to create a symbolic link to the Haskell libraries using the following commands: 

  mkdir -p ~/lib
  ln -s /home/class/fa06/cs476/lib/hugs/ ~/lib/hugs
You should now be able to run MTT running ./mtt from within ~/MTT

After MTT starts up, verify that the termination tools started up by checking the output windows at the bottom of the screen. There should be messages from CiME, MuTerm, and Maude. AProVE does not display text when it starts up. After this you are ready to start trying to out the termination checker. The examples for the course are in the directory examples.

Helpful Links