Maude-help mailing list

[Francisco Duran <duran AT lcc.uma.es>]

Hi Christian,

Finding an order to prove the termination of any speciication is 
nontrivial, but clearly doing it for conditional specifications is 
really challenging. Because of this, instead of moving the tools to 
Maude 2 what I've been doing recently is trying to use available 
termination tools as CiME or MU-TERM to not only do the check, but also 
finding the order.

Perhaps you may be interested in trying this new tool MTT 
(http://www.lcc.uma.es/~duran/MTT). This is a push-button tool, it we'll 
find the order to do the check, or we'll tell you that it cannot find 
such an order with the given restrictions. Currently it handles Maude 2 
specifications with the only restriction of not supporting overloaded 
operators, and some limitations on the rewriting attributes that can be 
used (only AC is supported).

The installation of MTT is rather simple, but you need to have also 
installed CiME and MU-TERM (this one only if you are using local 
strategies).

You may also be interested in reading som of the papers behind MTT, see 
e.g. http://www.lcc.uma.es/~duran/MTT/pepm04/.

Let me know if you have any problem with the tool, and please also if 
you succeed using it.

Best regards,

Paco


Christian Grothoff wrote:

> Dear Maude team,
>
> I am trying to use Maude to implement the decision procedure for a new type 
> system.  One important goal is to show that the procedure terminates.  For 
> that, I converted the code from Maude2 to Maude1 and tried to use the CR/KBC 
> tools that you have made available.  I used the tools from 
> http://maude.cs.uiuc.edu/maude1/tools/ together with the missing files 
> ext-bool.fm, strict-order.fm and weight.fm (also attached) which I gathered 
> from an earlier posting on the maude-help Maude mailinglist and Francisco 
> Duran's paper titled "Termination Checker and Knuth-Bendix Completion Tools 
> for Maude Equational Specifications".
>
> I have successfully used the tool to verify reasonably complex modules 
> (finding both equations that I had to change as well as examples where KBC 
> did not terminate [after 60 minutes]). Usually the tool gives either 
> termination or non-termination and then states either that an equation could 
> not be oriented (giving a critical pair) or says that KBC succeeded and 
> outputs the complete(d) equation system.
>
> However, when I try to run the tool on a trivial example with conditional 
> equations (ceq) it fails -- without error or completion (see attached output 
> run-test-output).  I have attached the minimal version of the code that I 
> used to run (ceq-test.fm), the shell-script I use to run maude (run-test; 
> maude1f is a shell script that invokes maude1 with the full-maude.maude file 
> as the first argument). The only example for ceq that comes with the tools is 
> a rather long example where KBC fails.  Can you tell me what I am doing 
> wrong?  I've tried various variations of the weight function implementation 
> without success.
>
> Also, I would be very interested in easier ways to run the CR/KBC tools, in 
> particular alternatives involving just using maude2 would be nice.  
>
> As a little bonus for reading my long E-mail, I've attached a little Java 
> wrapper around the Maude interpreter that I've been using to run "rew" 
> commands on maude from Java.  I've put it under the GPL -- just like Maude 
> itself.
>
> Thanks in advance!
>
> Best regards
>
> Christian Grothoff
>  
>
> ------------------------------------------------------------------------
>
> _______________________________________________
> Maude-help mailing list
> Maude-help AT maude.cs.uiuc.edu
> http://maude.cs.uiuc.edu/cgi-bin/mailman/listinfo/maude-help
>