Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha123/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

This version fixes a critical bug and other issues.
In case you were wondering what happened to Alpha122,
that version had an experimental garbage collector
that ran into issues with C++ object memory layout
so I started a fresh source tree.

This version comes with Linux binaries only for the moment
due to my outdated Mac going away.

Rubén Rafael Rubio Cuéllar <rubenrub@ucm.es> has volunteered
to make the Mac binaries and I'll put them up as soon as
he does.

Bug fix
========

(1) A bug where the cannonical renaming generated for
instantiating a module can have op mapping specializations
that don't match the op being mapped because sorts are missed.
Illustrated by the following example:

fth FOO is
  sort Small .
  op a : -> Small .
endfth

fmod BAR{X :: FOO} is
  sort Big .
  subsort X$Small < Big .
  op f : Big -> Bool .
  eq f(a) = true .
endfm

fmod BAZ is
  sort Baz .
  op b : -> Baz .
endfm

view V from FOO to BAZ is
  sort Small to Baz .
  op a to b .
endv

fmod TEST is
  inc BAR{V} .
endfm

red b .

Here the mapping
  op a to b .
gets specialized to
  op a : -> Small to b .
which then fails to match a in 
  eq f(a) = true .
because import translation always takes the top sort, Big
in this case, when looking for a renaming. This is a
consequence of the new module system where the code is
shared between module instantiation and view instantiation.
With view instantiation there is no larger module that
could add sorts to a kind. Found by
Stephen Skeirik <skeirik2@illinois.edu>
The solution is that the op mapping specialization
code now looks at module into which the mapped operators
are being imported when deciding how to specialize.

Other changes
==============

(1) Maude no longer tears down and re-initializes BuDDy. Instead
BuDDy is initialized the first time it is used and is left alone,
even if there are no modules using it, as can happen with meta-modules
being created and destroyed. This seems to resolve the issue with
compiling under recent versions of gcc.

Also it's unclear if the previous fix of compiling with clang
was really a fix since an alternative fix that avoided increasing
the number of BDD variables mid-computation also seemed to work
and looked good under valgrind but still showed memory corruption
under Purify. Purify does not support clang. The above fix looks
good under Purify.

(2) There are changes to Maude's garbage collector to make it more
standards compliant, particularly with respect to strict aliasing.

Steven