Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha78/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

Bug fixes:
(1)	A warning is now generated for single argument empty syntax
	operators; these have never been allowed in eithe OBJ3 or
	Maude. Bug reported by Feng Chen.

The main change in this version is a new term representation along
with new matching and renormalization algorithms for the AC and ACU
theories. For some simple patterns, this enables rewrites that would
have taken time linear in the size of the subject (using the old
greedy matching) to execute in log time (using the new greedy
matching). This can be a big win if the subject has thousands of alien
subterms under an AC/ACU operator. In particular it is now feasible to
implement maps using AC or ACU rewriting - see mapExample.maude

So far the new method is only implemented for a small subset of
patterns and in particular it does not work at all for conditional
equations. Nor does it work for rules in model checking or search
where all matches are needed. In these cases the subject must be
converted to the old representation in order to use the old
algorithms, and thus things can get slower.

I expect to increase the subset of patterns handled and make the
heuristics for switching between representations smarter in future
versions. However since this is such a radical change to the guts of
the rewrite engine I am putting this version out so people can check
if anything is broken. Two changes that you may notice:

(1) The term ordering for terms headed by AC/ACU operators has changed
    slightly.

(2) The matches chosen and hence the sequence of rewrites may differ.

Neither of these should be a problem if your specification is
confluent.

There are some minor changes agreed at various Maude teleconferences:

(1) =>1 replaces => for one step search in search command. This is to
    avoid confustion with => in conditions which means search for 0 or
    more step proofs (=>* in search command). This also affect the XML
    output.

(2) fmod NUMBER-CONVERSION renamed to CONVERSION since Carolyn pointed
    out that it also involves strings. Unfortunately this breaks Full
    Maude.

(3) _|=_ which use to do double duty in the model checker is now just
    used for satisfaction and lives in fmod SATISFACTION. The operator
    to actually start the model checker is now:

    op modelCheck : State Formula ~> ModelCheckResult .

    This enables checking satisfaction without invoking the model
    checker.

(4) If you get an internal error, bug report address is now:
    maude-bugs@maude.cs.uiuc.edu


Steven