Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha70/

or downloaded from

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

This version contains the first part of a major restructuring of the
Maude code to fix various extensibility limitations and performance
bottlenecks. Hopeful this overhaul should not have any visible
changes apart from (slightly) improved performance - but I may have
introduced some bugs - that's why it's important to have Maude Abusers
trying to break it. There are some visible changes in this version:

Bug fixes:

(1)	A bug in the grammar generator that add a spurious production
   	for every token containing "::". Provoked by the following
   	example:

	fmod FOO is
	  sorts Foo Bar .
	  op X::Foo : -> Bar .
	endfm

	red X::Foo[Foo] .  *** shouldn't parse

(2)	A bug in the DAG printer, causing floats, strings, quoted
	identifiers and variables to print incorrectly. Provoked by
	the following example:

	set print graph on .
	red in STRING : "a" .
	red in FLOAT : 1.0 .
	red in QID : 'a .
	red in FLOAT : X::Float .

(3)	A memory leak in metalevel where if a condition contained
	several fragments, and a later fragment contained an error the
	early fragements wouldn't be garbage collected.

(4)	A bug in the MSCP10 parser that caused memory corruption
	whenever the 1000th production in a grammar was a bubble
	(thanks go to Dilia for reporting the bug and Jose Quesada for
	fixing it).

New features:

(1)	ditto attribute. This can be used as the sole attribute of an
	operator, for which a subsort polymorphic instance has already
	appeared, either in the same module or as an import. It's just
	a shorthand to avoid writing out a long attribute list again
	and again, although it can be used to overload an imported
	operator without knowing the operators attributes.

	It is not allowed to combine ditto with other attributes or to
	use ditto on the first instance of an operator. Example of use:

	fmod DITTO-TEST is
	  sorts Foo Bar Baz .
	  subsort Foo < Bar .
	  op f : Foo Foo -> Foo [assoc comm] .
	  op f : Bar Bar -> Bar [ditto] .
	endfm

	Since it's just a shorthand (and would make processing of
	metamodules more complex), and it depends on the textual order
	of declarations (at the metalevel we use sets of operator
	declarations) it is not reflected in the metalevel.

	ditto is used to simplify prelude.maude and
	model-checker.maude

(2)	format attribute. Intended to control the character level 
	white space when printing terms for programming langauge like
	specifications. I notice many Maude users end up formatting
	Maude output manually - hopefully this will make things more
	automatic.

	Consider an operator with mixed fixed syntax:

	op (op_:_->_[_].) : Qid TypeList Type AttrSet -> OpDecl .

	There are 11 places where white space can be inserted:

	   op   _   :   _   ->   _   [   _   ]   .
	 ^    ^   ^   ^   ^    ^   ^   ^   ^   ^   ^

	A format attribute must have an instruction word for
	each of these places. For example:

	[format (d d d d d d s d d s d)]

	Instruction words are formed from the following alphabet:

	d	default spacing (must occur on it's own)
	+	increment global indent counter
	-	decrement global indent counter
	s	space
	t	tab
	i	number of spaces determined by indent counter
	n	newline

	Whether the format attribute is actually used when printing is
	controlled by the command:

	set print format on/off .

	The following additional alphabet can be used change the text
	color and style. They may be useful for putting markers in complex
	terms. They rely on ANSI escape sequences which are supported
	by most terminal emulators, most notably the linux console,
	xterm and DOS windows BUT not Emacs shell buffers unless you
	use ansi-color.el
	I've put a copy of this Emacs lisp file with the Maude
	distribution just in case your Emacs distribution lacks it.

	r	red
	g	green
	y	yellow
	b	blue
	m	magenta
	c	cyan
	u	underline
	!	bold
	o	revert to original color and style

	By default ANSI escape sequences suppressed if the environment
	variable TERM=dumb (Emacs does this) or standard output is not
	a terminal and allowed otherwise. This behavior can be
	overridden by the command line options -ansi-color and
	-no-ansi-color

	Note that the less program will not display ANSI escape
	sequences correctly unless you give it the -r flag.

	You are allowed to give a format attribute even if there is
	no mixfix syntax. In this case the format attribute must have
	two instruction words - one for before and one for after the
	operators name. For example:

	fmod COLOR-TEST is
	  sorts Color ColorList .
	  subsort Color < ColorList .
	  op red : -> Color [format (r! o)] .
	  op green : -> Color [format (g! o)] .
	  op blue : -> Color [format (b! o)] .
	  op yellow : -> Color [format (yu o)] .
	  op cyan : -> Color [format (cu o)] .
	  op magenta : -> Color [format (mu o)] .
	  op __ : ColorList ColorList -> ColorList [assoc] .
	endfm

	red red green blue yellow cyan magenta .

	There are some examples of format attributes in fmod LTL in
	model-checker.maude and fmod META-MODULE in prelude.maude

(3)	Rewrite (Rule) condition fragments now work
	The operatortion semanantics is an exhaustive breadthfirst
	search with full history caching to avoid cycles and repeated
	work (due to "diamonds"). The degenerate case (0 step
	rewriting or match without any rewrites) is allowed. If this
	is not what you want you can avoid it using the sort
	mechanism.

	This kind of rewrite search is used extensively in ELAN and I
	have translated a couple of ELAN examples into Maude:
	queens.maude and knight.maude

	Since we don't have a strategy language to prune the search and
	since full history caching is expensive you can't expect Maude
	to be competitive on these examples.

(4)	metaMatch/metaXmatch/metaSearch now accept a side condition;
	this can be a conjuction of condition fragments, just like the
	condition of a rule. They now look like

	op metaMatch : Module Term Term Condition MachineInt ~>
		       Substitution? .
	op metaXmatch : Module Term Term Condition MachineInt
		        MachineInt MachineInt ~> MatchPair? .
	op metaSearch : Module Term Term Condition Qid
			MachineInt MachineInt ~> ResultTriple? .

	The new symbol

	op nil : -> EqCondition .

	can be used in the case you don't want a condition. This
	becomes the identity of the conjunction symbol. Note that
	if you pass this constant as the condition argument of ceq
	(resp. crl, cmb) you will in fact end up with an eq (resp. rl,
	mb) rather the an error. I'm not sure whether this is a good
	idea - it happens by default since internally an unconditional
	statement is just a conditional statement with a zero length
	vector of condition fragments.

	There are some subtleties: substitutions can now contain variables
	that might only occur in the condition and different solutions
	might differ only in assignments to these variables.

(5)	There is now built in support for LTL sat solving; the
	interface to the sat solver is defined in fmod SAT-SOLVER in
	model-checker.maude For example

	fmod TEST is
	  inc SAT-SOLVER .
	  ops a b c d e p q r : -> Prop .
	endfm

	red satSolve([] a /\ <> b) .

	The sat checker treats alien subterms as propositions. If
	the formula is satisfiable it returns a model expressed as a
	lead-in and a cycle (much like the counterexamples produced by
	the model checker) where the states are conjunctions of
	literals. If a proposition is not mention in a conjunction then
	it is a don't care.

	Since tautolgy checking is the dual of sat solving, this module
	also defines a tautlogy checker in terms of the sat
	solver. For example:

	red tautCheck( (p U r) /\ (q U r) <-> ((p /\ q) U r) ) .

	If the given formula is a tautogy, tautCheck returns true;
	if not it returns a counterexample in the same style as the
	models produced by the sat solver.

Also there are a number of minor changes to model-checker.maude

(1)	precs of _->_ and _<->_ increased to 65, precs of _U_, _R_ and
   	_W_ reduced to 63. Hopefully this make parsing more intuitive.

(2)	_|->_ (leads to) operator added at Jose's request.

(3)	o_ operator becomes O_ at Jose's request.

(4)	_W_ no longer has the ctor attribute - this was a mistake
	pointed out by Jose.

(5)	counterExample becomes counterexample - for consistancy since
	counterexample is 1 word and not 2 as I originally thought.

(6)	sort Prop is moved to fmod LTL so it can be shared with
	fmod SAT-SOLVER.

Despite these change the old dekker.maude example still works so there
is no new version of this file.

Steven