Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha92b/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

Bug fixes
----------
(1) A bug where the garbage collector was never called during a search
command where no equational rewrites took place. Provoked by an
example from Carolyn.

(2) A bug where the wrong "UNSTACKABLE" flag was being checked for the
second argument of a non-associative symbol that was C, U, and/or I.
This could cause missed rule rewrites in a number of situations, the
simplest being:

mod CUI-BUG is
  sort Foo .
  ops a b c d 1 : -> Foo .
  op f : Foo Foo -> Foo  [id: 1] .
  op g : Foo -> Foo .

  rl b => c .
  rl c => d .
endm

rew f(a, g(b)) .

Other changes
--------------
In this version I've reimplemented the state transistion graph class
used by the search command and the model checker with two
optimizations:

(1) It uses a weak form of hash consing where a hash cons'd copy is
made of the final reduced dag for each state. Thus subdags are
maximally shared within the state transition graph. This saves space
and speeds up the comparison of equal subdags. The downside is copying
takes time and produces more garbage so the time used may go up or
down depending on the example.

(2) It uses a unreducible/unstackable optimization similar to that
used in for the rewrite/frewrite commands where subdags that fail to
rewrite are flagged unrewritable to avoid checking them again, and
subdags that are flagged unrewritable and which fail to stack any
arguments are flagged unstackable so they are not stacked
(i.e. explored) again. This always seems to be a time win, but
especially so when hash consing is used since the sharing makes
finding a set unrewritable or unstackable flag more likely.

I've also changed the hash function on dags since the original one was
producing a lot of collisions.

I'm very interested to know what effect these changes have on large
search and model checking examples people may have.

At Santiago's request I've started supporting 32bit Linux again.

Steven