Maude-help mailing list

[Christian Grothoff <christian AT grothoff.org>]

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
		     \||||||||||||||||||/
		   --- Welcome to Maude ---
		     /||||||||||||||||||\
	Maude version 1.0.5 built: Apr  5 2000 15:56:52
	     Copyright 1997-2000 SRI International
		   Wed Oct  5 14:46:28 2005

	Full Maude version 1.0.5 
	Copyright 1999-2000 SRI International 

ADVISORY: redefining module "AUXILIARY-FUNCTIONS".
ADVISORY: redefining module "EXT-TERM".
ADVISORY: redefining module "UNIFICATION".
ADVISORY: redefining module "MATCHING".
ADVISORY: redefining module "AUXILIARY-FUNCTIONS".
ADVISORY: redefining module "EXT-TERM".
ADVISORY: redefining module "UNIFICATION".
ADVISORY: redefining module "MATCHING".
ADVISORY: redefining module "CRITICAL-PAIR".
ADVISORY: redefining module "MODULE-PREPARATION".
ADVISORY: redefining module "AUXILIARY-FUNCTIONS".
ADVISORY: redefining module "EXT-TERM".
ADVISORY: redefining module "UNIFICATION".
ADVISORY: redefining module "MATCHING".
ADVISORY: redefining module "CRITICAL-PAIR".
ADVISORY: redefining module "MODULE-PREPARATION".
ADVISORY: redefining module "COHERENCE-CHECK".
ADVISORY: reparsing module CRC-DATABASE-HANDLING due to changes in imported
    modules.
ADVISORY: reparsing module CRC due to changes in imported modules.
ADVISORY: reparsing module CONFLUENCE-CHECK due to changes in imported modules.
ADVISORY: reparsing module DESCENT-CHECK due to changes in imported modules.
ADVISORY: reparsing module COHERENCE-CHECK-DATABASE-HANDLING due to changes in
    imported modules.
rewrites: 1364 in 0ms cpu (1ms real) (12629629 rewrites/second)

rewrites: 1094 in 9ms cpu (10ms real) (120127 rewrites/second)

Introduced module: crt
Reading in file: "lpo.fm"
Reading in file: "ext-bool.fm"
rewrites: 1059 in 1ms cpu (2ms real) (955776 rewrites/second)

Introduced module: EXT-BOOL
Done reading in file: "ext-bool.fm"
Reading in file: "strict-order.fm"
rewrites: 940 in 1ms cpu (2ms real) (848375 rewrites/second)

Introduced theory: STRICT-ORDER
Done reading in file: "strict-order.fm"
rewrites: 6686 in 13ms cpu (14ms real) (510148 rewrites/second)

Introduced module: LPO
Done reading in file: "lpo.fm"
rewrites: 938 in 1ms cpu (2ms real) (846570 rewrites/second)

Introduced module: GROUP-I-ORDER
rewrites: 1305 in 1ms cpu (2ms real) (1177797 rewrites/second)

Introduced module: GROUP-I-WEIGHT
Reading in file: "kbo.fm"
Reading in file: "ext-bool.fm"
rewrites: 1146 in 1ms cpu (2ms real) (1034296 rewrites/second)

ADVISORY: Module EXT-BOOL redefined 
Introduced module: EXT-BOOL
Done reading in file: "ext-bool.fm"
Reading in file: "strict-order.fm"
rewrites: 1116 in 1ms cpu (2ms real) (1007220 rewrites/second)

ADVISORY: Module STRICT-ORDER redefined 
ADVISORY: Module X :: STRICT-ORDER removed 
ADVISORY: Module LPO removed 
Introduced theory: STRICT-ORDER
Done reading in file: "strict-order.fm"
Reading in file: "weight.fm"
rewrites: 1076 in 0ms cpu (0ms real) (~ rewrites/second)

Introduced theory: WEIGHT-FUNCTION
Done reading in file: "weight.fm"
rewrites: 3620 in 5ms cpu (6ms real) (708831 rewrites/second)

Introduced module: WEIGHT
rewrites: 15925 in 25ms cpu (26ms real) (634361 rewrites/second)

Introduced module: KBO
Done reading in file: "kbo.fm"
rewrites: 493 in -1ms cpu (0ms real) (~ rewrites/second)

Introduced view: GROUP-I-ORDER
rewrites: 746 in 0ms cpu (0ms real) (~ rewrites/second)

Introduced view: GROUP-I-WEIGHT
rewrites: 44934 in 41ms cpu (42ms real) (1093231 rewrites/second)

Termination check of crt
ADVISORY: reparsing module COMPLETION due to changes in imported modules.
ADVISORY: reparsing module CRITICAL-PAIRS due to changes in imported modules.
rewrites: 44998 in 101ms cpu (103ms real) (445114 rewrites/second)

Knuth-Bendix completion of crt
Bye.

/**
 * 
 */
package org.grothoff;

import java.io.BufferedReader;
import java.io.DataOutputStream;
import java.io.IOException;
import java.io.InputStreamReader;

/**
 * Wrapper around Maude.  The idea is that you subclass this class,
 * overwrite initialize to load the required maude modules and then
 * use the "rew" function.
 * 
 * @author Christian Grothoff
 * @license GPL
 */
public abstract class MaudeWrapper {

	/**
	 * The name of the Maude binary (supposed to be in your PATH).
	 */
	private final static String MAUDE_COMMAND = "maude2";
	
	private final static boolean VERBOSE = false; 
	
	private final static boolean PRINT_MAUDE_STDERR = true;
	
	private final Process maude;
	
	protected final BufferedReader input;

	protected final BufferedReader error;
	
	protected final DataOutputStream output;	

	private final Thread errorHandler;
	
	/**
	 * Create a wrapper around maude. 
	 */
	public MaudeWrapper() {
		this(MAUDE_COMMAND);
	}
	
	/**
	 * Create a wrapper around maude. 
	 */
	public MaudeWrapper(String cmd) {
		try {
			maude = Runtime.getRuntime().exec(new String[] {
					cmd, 
					"-no-banner" });
			input = new BufferedReader(new InputStreamReader(maude.getInputStream()));
			error = new BufferedReader(new InputStreamReader(maude.getErrorStream()));
			output = new DataOutputStream(maude.getOutputStream());
			initializeMaude();
		} catch (IOException io) {
			throw new Error(io);
		}
		
		// handle stderr of Maude!
		errorHandler = new Thread() {
			public void run() {
				while (true) {
					try {
						String s = error.readLine(); //@nowarn
						if (PRINT_MAUDE_STDERR) 							
							System.err.println(s);
					} catch (IOException io) {
						return; // exit once Maude closes stderr!
					}
				}
			}
		};
		errorHandler.start();
	}
	
	/**
	 * Initialize the maude interpreter.  Typically contains statements like
	 * <code>
	 * output.writeBytes("load myMaudeModule.maude .\n");
	 * </code>
	 */
	protected abstract void initializeMaude() throws IOException;

	/**
	 * Kill the maude child process on exit.
	 */
	public void finalize() {
		try {
			output.close();
		} catch (IOException io) {
			maude.destroy();
			throw new Error(io);
		} finally {
			try {
				maude.waitFor();
				errorHandler.join();
			} catch (InterruptedException ie) {
				throw new Error(ie);
			}
		}
	}
	
	/**
	 * Run a rew command on maude.	 
	 * 
	 * @param expr maude expression to rewrite
	 * @return TRUE if the test succeeds, otherwise a String describing
	 *        conditions that would be needed to make the test succeed
	 */
	public final String runRew(String expr) {
		try {
			output.writeBytes("rew " + expr + " .\n");
			output.flush();
			String s = null;
			do {
				s = input.readLine();
				if (VERBOSE)
					System.err.println("MAUDE: " + s);
				if (s == null)
					throw new Error("Failed to obtain result from maude!");
			} while (! s.startsWith("result "));
			return s.substring(6); // cut of "result "
		} catch (IOException io) {
			throw new Error(io);
		}			
	}
	
} // end of MaudeWrapper
loop init .

(fmod crt is

pr MACHINE-INT    .
sorts place point region distribution .

op empty :         -> region       [ctor] .
op _to_  : region place -> distribution   .
op _|_   : distribution place -> region   .

vars r    : region .
vars p pp : place  .

ceq (r to p) | pp = empty  if p =/= pp .

endfm)

in lpo.fm

(fmod GROUP-I-ORDER is
   pr QID .
   op _>>_ : Qid Qid -> Bool .
   eq '_=/=_ >> '_|_   = true .
 endfm)

(fmod GROUP-I-WEIGHT is
   pr QID .
   pr MACHINE-INT .
   op weight : Qid -> MachineInt .
   op weight0 : -> MachineInt .
   eq weight0 = 1 .
   eq weight('_|_)    = 1 .
   eq weight('_to_)   = 1 .
   eq weight('_=/=_)   = 1 .
 endfm)

in kbo.fm

(view GROUP-I-ORDER from STRICT-ORDER to GROUP-I-ORDER is
   op _>>_ to _>>_ .
 endv)

(view GROUP-I-WEIGHT from WEIGHT-FUNCTION to GROUP-I-WEIGHT is
   op weight to weight .
   op weight0 to weight0 .
 endv)

(check termination crt
            with KBO[GROUP-I-ORDER, GROUP-I-WEIGHT]
                    * (op _>kbo_ to _>>>_) .)

(complete crt
            with KBO[GROUP-I-ORDER, GROUP-I-WEIGHT]
                    * (op _>kbo_ to _>>>_) .)

Attachment: run-test
Description: application/shellscript

(fth STRICT-ORDER is
  *** A strict order is a transitive and irreflexive relation.
 pr QID .
 op _>>_ : Qid Qid -> Bool .
 vars A B C : Qid .
 ceq A >> B = false if B >> A .
 ceq A >> C = true if A >> B and B >> C .
endfth)
(fmod EXT-BOOL is
  op _andThen_ : Bool Bool -> Bool [assoc strat (1 0 2 0) prec 55] .
  op _orElse_ : Bool Bool -> Bool [assoc strat (1 0 2 0) prec 59] .
  var B : Bool .
  eq false andThen B = false . 
  eq true andThen B = B .
  eq true orElse B = true .
  eq false orElse B = B .
endfm)
(fth WEIGHT-FUNCTION is
   pr QID .
   pr MACHINE-INT .
   op weight0 : -> MachineInt .
   op weight : Qid -> MachineInt .
endfth)