Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha88b/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

This version reports itself as Maude 2.3 and is a 2.3 release
candidate to go with the forthcoming Maude book.

Bug fixes
==========
(1) A bug in the search code where the replacement term shown during a
trace doesn't take the extension in to account. Exposed by:

mod FOO is
  sort Foo .
  ops a b c d e : -> Foo .
  op f : Foo Foo -> Foo [assoc comm] .
  rl f(a, b) => e [label 1].
endm

set trace on .

search f(a, b, c) =>+ X:Foo .

We see
  f(a, b, c)
  --->
  e
instead of
  f(a, b, c)
  --->
  f(c, e)
This bug also affected tracing in the model checker since the code is
shared.

(2) A similar bug in the strategy language implementation, exposed by

srew f(a, b, c) using 1 .

(3) Yet another version of the bug, this time in the metalevel,
exposed by

red in META-LEVEL : metaXapply(['FOO], 'f['a.Foo, 'b.Foo, 'c.Foo], '1,
none, 0, 0, 0) .

(4) The command
  set trace condition on/off .
was being ignored. Bug reported by Paco.

Changes
========
(1) Minor reorganization of model-checker.maude as proposed by Jose.
Prop is moved to SATISFACTION and its subsort declaration is moved to
MODEL-CHECKER. _|=_ is frozen and total and now takes Prop as its
second argument.

(2) Strategy test xmatch is renamed to amatch (anywhere match) and xmatch
is now match at top with extension (congruent to the xmatch command).

(3) The application of a label l in the strategy language can now take a
list of  substrategies to use for rewrite condition fragments with the
syntax
  l{s, t}
or
  l[X <- u, Y <- v]{s, t}
if a substitution is included. It is now required that the number of
substrategies exactly match the number of rewrite condition fragments
in a rule for the rule to be considered for application (this might be
relaxed in the future).
The strategic searches for rewrite condition fragments are interleaved
with other branches of the original search, including branches from
the same crl application in order to achieve fairness.
Since the strategy combinators not() and test() can prune their search
after achieving a single success, it is possible start several
infinite searches and yet still terminate if one succeeds:

mod COUNT is
  inc NAT .
  sort Foo .
  op f : Nat -> Foo .
  op success : -> Foo .

var N : Nat .
  rl N => N + 2 [label 2] .

  crl f(N) => success if N => 9 [label a] .
  crl f(N) => success if N => 10 [label a] .
endm

*** check interleave of two infinite seaches, 1 successful, 1 not
srew f(0) using test(a{2 *}) .

(4) srewrite now reports rewrite counts and timing.

Steven