Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha71/

or downloaded from

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

The main purpose of this release is to allow members of the biopathways
group to experiment with a first attempt at XML support for Maude
output. This is the only new feature and there will probably be at
least one more alpha release from the 71st source tree. There are no
changes to the model checker so use the model-checker.maude from
Alpha 70.

To enable XML output to a log file you use the -xml-log= command line
flag; for example:

maude.linux -xml-log=my.xml

An XML version of the output of commands that support XML will be
written to the named file.

Only 4 commands currently support XML: red, rew, frew & show search
graph . I have provisionally named the Maude XML application "maudeml"
and maudeml is used as the root element of the XML log file.

The first 3 commands all produce their output in the same format using
a <result> element. Consider the following example:

fmod FOO is
  sort Foo .
  ops a b c d e : -> Foo .
  op f : Foo -> Foo .
  op g : Foo Foo -> Foo .
  var X : Foo .
  eq f(X) = g(X, X) .
endfm

red f(a) .
set show breakdown on .
red f(a) .

This will produces an XML log file similar to:

<?xml version="1.0" encoding="US-ASCII" standalone="yes"?>
<maudeml>
 <result total-rewrites="1" real-time-ms="0" cpu-time-ms="0">
  <term op="g" sort="Foo">
   <term op="a" sort="Foo"/>
   <term op="a" sort="Foo"/>
  </term>
 </result>
 <result total-rewrites="1" mb-rewrites="0" eq-rewrites="1" rl-rewrites="0" real-time-ms="0" cpu-time-ms="0">
  <term op="g" sort="Foo">
   <term op="a" sort="Foo"/>
   <term op="a" sort="Foo"/>
  </term>
 </result>
</maudeml>

I have yet to attempt a DTD for maudeml however the current
implementation assumes a fragment something like:

<!ELEMENT maudeml ((result|graph)*)>

<!ELEMENT result (term)>
<!ATTLIST result
  total-rewrites	CDATA	#IMPLIED
  mb-rewrites		CDATA	#IMPLIED
  eq-rewrites		CDATA	#IMPLIED
  rl-rewrites		CDATA	#IMPLIED
  real-time-ms		CDATA	#IMPLIED
  cpu-time-ms		CDATA	#IMPLIED
  rewrites-per-second	CDATA	#IMPLIED
>

<!ELEMENT term (term*)>
<!ATTLIST term
  op			CDATA	#REQUIRED
  sort			CDATA	#IMPLIED
  syntactic-sort	CDATA	#IMPLIED
  kind			CDATA	#IMPLIED
>

<!ELEMENT rule (term,term,condition?)>
<!ATTLIST rule
  label			CDATA	#IMPLIED
>

<!ELEMENT condition ((equality-test|sort-test|assignment-test|rewrite-test)+)>
<!ELEMENT equality-test (term,term)>
<!ELEMENT assignment-test (term,term)>
<!ELEMENT rule-test (term,term)>
<!ELEMENT sort-test (term)>
<!ATTLIST sort-test
  sort			CDATA	#REQUIRED
>

The graph element (which is used to encode the output of show search
graph) follows the current graphml draft:

http://www.graphdrawing.org/graphml/

where nodes are have a data element with key "term" and edges have 1 or
more data elements with key "rule".

Note that this first draft for a fragment of maudeml is highly
provisional and will very likely to change in the near future. I
envision that maudeml will eventually  encompass all Maude i/o and
will allow modules, terms and results to be transferred between
interpeters using a protocol such as http.

There are also a couple of bug fixes:

(1)	A bug in the MSCP10 parser that caused memory corruption
	whenever the grammar contains exactly 4999 or 5000 symbol
	occurences in the rhs of the productions. Thanks go to Paco
	for reporting this one.

(2)	A bug in the abort handling of conditions (only visible for
	rewrite conditions at the metalevel). Basically I assumed that
	I could treat abort as success for faster stack unwinding
	which worked fine for Maude 1.0.* but is unsafe when a
	condition fragment is required to bind variables on success
	and can lead to dereferencing a null pointer in the metalevel.
	Thanks go to Alberto Verdejo for the following example:

	mod M is
	  pr MACHINE-INT .
	  sort S .
	  sort T .
	  subsort S < T .
	  ops a d : -> S .
	  ops b c : MachineInt -> T .
  
	  var I : MachineInt .
	  var X : S .
  
	  crl [one] : a => X if b(1) => X .
	  rl [two] : b(I) => c(I) .
	  rl [three] : c(I) => b(I + 1) .
	  rl [four] : b(1) => d .
	endm

	red in META-LEVEL : metaApply(['M],'a.S,'one, none, 1) .

	*** enter ^C and then 
	abort .

Steven