Dear Maude Abusers,

A new alpha release can be accessed at SRI-CSL in

~eker/public_html/Maude/Alpha66/

or downloaded from

http://www.csl.sri.com/~eker/Maude/Alpha66/


Currently only linux and solaris are supported. Since there are new
people on my "Maude Abusers" list I have put the release notes for
previous versions in

http://www.csl.sri.com/~eker/Maude/ReleaseNotes

The changes from Alpha65 are:

(1)	Break symbol facility - select and deselect break symbols
	with:

	break select foo bar baz .
	break deselect quux .

	The break facility is switched on and off with

	set break on/off .

	When it is on, executing a mb/eq/rl with a break symbol
	on top will put you in the debugger.

(2)	match/xmatch commands reimplemented. They may now have a
   	condition introduced by "such that" or equivalently "s.t.";
   	for example

	match [2] in FOO : X * (Y + Z) <=? (a + b) * (a + d)
	s.t. A:Nat + B:Nat := X /\ A:Nat = Y .

	Also you can continue to look for more solutions with

	cont 4 .

	for example. Parsing is also a little smart in that the fact
	that both sides of <=? must be in the same component is taken
	in to account when resolving ambiguities.

(3)	search command reimplemented. The new syntax is

	search [<# solutions>] in <module> :
	<start term> <relation> <pattern> such that <condition> .

	The "[<# solutions>]", "in <module> :" and "such that
	<condition>" parts are optional. "s.t." is an abbreviation for
	"such that". Possible relations are:

	=>	rewrites in exactly 1 step
	=>*	rewrites in 0 or more steps
	=>+	rewrites in 1 or more steps
	=>!	rewrites to normal form (i.e. a term in which no
		further rewrites are possible)

	For example:

	search [1] a * d + b * d + c * d + a * e + b * e + c * e =>+ X * Y
	such that W + Z := X .

	You can look for more solutions with the cont command as
	above. You may also interrupt a search in progress with ^C. In
	this case one of two things will happen dependeing on what
	Maude is doing at the instant you hit ^C. If Maude is not
	doing a rewrite, the command will exit. If maude is doing a
	rewrite you will end up in the debugger. In this latter case
	it is probably best to "abort ." since the debugger has no
	special support for search at the moment.

	When a search command terminates; either because there was a
	finite state graph and hence it can be determined there was
	no more solutions or because you used the "[<# solutions>]"
	part to limit the number of solutions found, the state graph
	is retained in memory until you switch modules or run another
	command the preforms rewriting. You can interrogate the state
	graph with the command:

	show path <state #> .

	which will show the sequence of states and rules going from
	the start term to the chosen state. Since the search command
	does a breadfirst search this will be a shortest path.

(4)	Timing reimplemented. Now if you do

	set timing off .
	set loop timing off .

	no calls to the system calls setitimer() or getitimer() will
	be made. This should enable the linux version of Maude to run
	under MS Windows using LINE (http://line.sourceforge.net/).
	Also the linux version should no longer report negative times.

Steven