Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha84c/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

This version is a pure alpha release - it is not destined for the
Maude website though of course you may redistribute it under the GPL.
Because of this I have only made binaries for Linux and Darwin.

New Features
=============
(1) metaApply()/metaXapply() now output trace information for the rule
application when tracing is on (requested by Paco & Alberto Verdejo).

(2) The prelude now contains a module

fmod RANDOM is
  protecting NAT .
  op random : Nat -> Nat
	[special (id-hook RandomOpSymbol
		  op-hook succSymbol (s_ : Nat ~> NzNat))] .
endfm

The function random is the mapping from Nat into [0, 2^32-1] computed
by successive calls the Mersenne Twister Random Number Generator
(http://www-personal.engin.umich.edu/~wagnerr/MersenneTwister.html).
By default the seed 0 is used but a different seed, giving a different
function may be specified by the command line option

-random-seed=<int>

where <int> is an integer in [0, 2^32-1].

Although random is a purely functional, it caches the state of the
random number generator so evaluating random(0) is always fast, as is
evaluating random(n+1) if random(n) was the previous evaluation of
random. This feature was requested by Koushik Sen who also provided
the http link.

(3) The prelude now contains a module

mod COUNTER is
  protecting NAT .
  op counter : -> [Nat]
	[special (id-hook CounterSymbol
		  op-hook succSymbol (s_ : Nat ~> NzNat))] .
endm

For the rewrite and frewrite commands, counter has special rule
rewriting semantics: each time it has the opportunity to do a rule
rewrite, it rewrites to the next natural number, starting at 0.
The intention is that it can be used to generate new names and new
random numbers in programs that don't want to explicitly maintain this
state. It is reasonable for a program to use multiple counters; the
safe way to do this is to import renamed copies of COUNTER:

  pr COUNTER * (op counter to counter2) .

Counters are inert wrt to search, model checking and equational
rewriting. They may be used at the metalevel (always being set to 0 at
the start of each metaRewrite()/metaFrewrite() to maintain functional
behavior of the descent function).

The are potentially bad interactions with the debugger since another
rewrite/frewrite executed in the debugger will lose the counter state
of the interrupted rewrite/frewrite.

This issue of losing hidden state in the debugger has existed for a
long time wrt to the round robin next rule pointer. There are even
worse interactions possible using both the metalevel and the debugger
but they are quite subtle to set up. I don't have a solution that is
both clean and efficient in the metalevel case so I have punted on
this for the moment until I see where the metalevel is heading.

I am interested to know from the people who use the MOS oracle
"feature" of Qids (if you don't know, don't ask...) whether counters
make this hack redundant - I'd like to remove it in the next alpha
release.

Steven