Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha79/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

Bug fixes:
(1) Bug where pointer was printed in a "can't continue." message if
    cont .
    was typed after start up.

(2) iter matching against a bare variable with extension now works so
    for example you can do:

    mod ITER-SEARCH is
      inc NAT .
      op f : Nat -> Nat .
      var X : Nat .
      rl X => f(X) .
    endm
    search 6 =>1 X .

    Not so much a bug as an unimplemented corner case.

(3) A nasty bug in the ACU/AC sort calculation where I assumed that
    assignments to variables couldn't be in the error sort; this
    assumption no longer holds since we have variables at the kind
    level. This bug is exposed by the following code.

    fmod ACU-SORT-BUG is
      sort Foo .
      ops a b c d e : -> Foo .
      op k : -> [Foo] .
      op f : Foo Foo -> Foo [assoc comm] .
      var K : [Foo] .
      eq f(a, K) = K .
    endfm
    red f(a, b, c, k) .  *** result should be at kind level

(4) Similar bug in the AU/A sort calculation.

(5) Bug in ACU Red-Black matcher code that could miss matches against
    subjects of the form f(a, X), a ground, if the subject had a
    strange sort structure.

(6) Similar bug in specialized matcher for f(X, Y) case.

(7) Stale pointer bug in the code that echos match/search commands
    in the case that the pattern flattened or collapsed during
    normalization (reported by Christiano Braga).

(8) A nasty bug in the original greedy matcher, where it fails to find
    a match, but decides there is no match rather than running the
    full matcher.

    fmod GREEDY-BUG is
      sorts E1 E2 P T .
      subsort E2 < E1 P < T .
      op f : P P -> P [assoc comm] .
      op f : T T -> T [assoc comm] .
      op i : T -> T .
      op a : -> E2 .
      op b : -> E1 .
      ops c d : -> P .
      op ok : -> T .
      eq i(f(X:E1, X:E1, Y:P, Z:P)) = ok .
    endfm

    red i(f(a, a, b, b, c, d)) .
    match i(f(X:E1, X:E1, Y:P, Z:P)) <=? i(f(a, a, b, b, c, d)) .


The main change in this version is that I have implemented the new
AC/ACU representation and matching for a wider class of patterns.
I've also revamped the old AC/ACU matcher and made a few optimizations
in other places. To see how the recent changes have affected AC/ACU
rewriting I have run the last 3 alphas on the mapExample.maude that I
distributed with Alpha78 and 4 other AC/ACU benchmarks that I've put
in:

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

Here are the results I got on a 2.8GHz Xeon. Some of the benchmarks
are very stack intensive so remember to "unlimit stacksize" to avoid
a stack overflow segmentation fault. Also you need lots of RAM.
8 cpu minutes is where my patience gives out :)


Alpha79
--------
setHierarchy.maude
rewrites: 6667125 in 6550ms cpu (6560ms real) (1017881 rewrites/second)

simpleSet.maude
rewrites: 766675 in 2480ms cpu (2480ms real) (309143 rewrites/second)
rewrites: 833341 in 2670ms cpu (2670ms real) (312112 rewrites/second)

tautology.maude
rewrites: 554823 in 990ms cpu (990ms real) (560427 rewrites/second)

threeElt.maude
rewrites: 2192505 in 44780ms cpu (44770ms real) (48961 rewrites/second)

mapExample.maude
rewrites: 599 in 0ms cpu (0ms real) (~ rewrites/second)
rewrites: 5999 in 20ms cpu (10ms real) (299950 rewrites/second)
rewrites: 59999 in 210ms cpu (210ms real) (285709 rewrites/second)
rewrites: 599999 in 2820ms cpu (2830ms real) (212765 rewrites/second)


Alpha78
--------
setHierarchy.maude
rewrites: 6667125 in 109820ms cpu (109830ms real) (60709 rewrites/second)

simpleSet.maude
> 8 cpu minutes
> 8 cpu minutes

tautology.maude
rewrites: 554823 in 1550ms cpu (1550ms real) (357950 rewrites/second)

threeElt.maude
rewrites: 2192505 in 60800ms cpu (60790ms real) (36060 rewrites/second)

mapExample.maude
rewrites: 599 in 0ms cpu (10ms real) (~ rewrites/second)
rewrites: 5999 in 10ms cpu (10ms real) (599900 rewrites/second)
rewrites: 59999 in 220ms cpu (210ms real) (272722 rewrites/second)
rewrites: 599999 in 2820ms cpu (2820ms real) (212765 rewrites/second)


Alpha77
--------
setHierarchy.maude
rewrites: 6667218 in 48610ms cpu (48610ms real) (137157 rewrites/second)

simpleSet.maude
> 8 cpu minutes
> 8 cpu minutes

tautology.maude
rewrites: 554819 in 1560ms cpu (1560ms real) (355653 rewrites/second)

threeElt.maude
rewrites: 2193693 in 50690ms cpu (50700ms real) (43276 rewrites/second)

mapExample.maude
rewrites: 599 in 0ms cpu (0ms real) (~ rewrites/second)
rewrites: 5999 in 150ms cpu (140ms real) (39993 rewrites/second)
rewrites: 59999 in 55000ms cpu (55000ms real) (1090 rewrites/second)
> 8 cpu minutes


There are also some changes to the source code that should make
porting easier; in particular the #pragmas that caused linking
problems with certain versions of g++ are gone. I used g++ 3.2.

I notice that some people have been discouraged from using Alpha78
because it breaks FullMaude. A work around for Alpha79 is to run it
with the prelude.maude from Alpha77. Then fm75-5.maude should work as
it did in Alpha77.

Steven