Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha69/

or downloaded from

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

This release fixes a serious bug in the metalevel that affects all
releases with the new metalevel. It can be provoked by the following
example:

mod FOO is
  sort Foo .
  ops a b c : -> Foo .
  op d : -> Bool .
  crl [1] : a => b if d .
  crl [1] : a => c if d .
  eq d = true .
endm

fmod BAR is
  inc META-LEVEL .
  op start : -> ResultTriple? .
  ceq start = metaApply(['FOO], 'a.Foo, '1, none, 1)
    if metaApply(['FOO], 'a.Foo, '1, none, 0) =/= failure .
endfm

break select d .
set break on .

red start .

where .
resume .
where .

The problem is that a pointer to the context created to evaluate the
condition is kept in the cached object for
  metaApply(['FOO], 'a.Foo, '1, none, 0)
When this object is pulled from the cache to evaluated
  metaApply(['FOO], 'a.Foo, '1, none, 1)
this context no longer exists when the "where" command tries to
accesses it.

The main change from Alpha68 is that the search code has been
integrated with the model checking code, fixing a number of
limitations in the process:

(1)	Counterexamples produced by the model checker now include
	rule labels. There are two special labels:
	"unlabeled" for rules that don't have a label and
	"deadlock" for self transitions added to deadlocked states.

(2)	You can now trace model checking; however the results can be
	hard to read. Rewrites proceed roughly depth first through the
	state graph with equation rewriting for testing propositions
	on states where such equations exist. This pattern of activity
	is complicated by the caching of previously seen rewrites
	(which are therefore not displayed in the trace), the 2nd
	depth first search for cycles and pruning due to the property
	automaton.

(3)	Rewrite counts for model checking are now correct.

(4)	^C and "abort ." now work for model checking except that the
	Buchi automtaton construction process cannot be interrupted.

(5)	The model checker now prints a warning rather than crashing if
	it is given an LTL formula not in negative normal form.

(6)	The search command now prints information about the number of
	rewrites as well as the number of states and timing. Like
	timing but unlike number of states, the rewrite count is reset
	by a continue. This is so that rewrites/second value makes
	sense. The "set show breakdown on." option now works with
	search.

(7)	"show path 0 ." is no longer is a syntax error.

(8)	There is a first attempt at a metaSearch descent function in
	the metalevel:

        op metaSearch : Module Term Term Qid MachineInt MachineInt
	  ~> ResultTriple? .

	The arguments are:
	Module :	The metamodule to work in.
	Term   :	The starting term for search.
	Term   :	The pattern to seach for.
	Qid    :	Kind of search; allowed values are
			'* : zero or more rewrites
			'+ : one or more rewrites
			'! : only match normal (unrewritable) forms
	MachineInt :	Depth of search, use maxMachineInt for
			unbounded. Terms will only be matched if they
			can be reached by this or fewer number of
			(rule) rewrites.
	MachineInt :	Solution number starting from 0.

	The return value uses the existing

	op {_,_,_} : Term Type Substitution -> ResultTriple [ctor] .

	constructor where:
	Term   :	Term matching the pattern.
	Type   :	Type of this term.
	Substitution :	Substitution produced by match.

	metaSearch uses caching so that extracting multiple solutions
	in solution number order is efficient.

	I'm not altogether satisfied with this design -  in particular
	there is no way to recover paths or the search graph - but
	I can't think of a better one that is functional.

	Also I could have a separate sort and constants for search
	type at the cost of putting yet more stuff into the metalevel
	signature.

(9)	There is a command
	  set verbose on .
	that enables informative messages that are not warnings
	(i.e. for errors in the input) or advisories (for strange
	situations that are likely errors but that can be handled in
	some way). The need for this is because built-in symbols such
	as _|=_ and metaSearch may produce potential useful
	information that I don't want to stick into the return result.
	But normally you don't want such symbols to have side
	effects - at start up, verbose messages are switched off.

Finally a couple of points about the model checker that were also
true of Alpha68 but perhaps I should point out explicitly:

(1)	The model checker is usable from the metalevel; since it is
	implemented as a special symbol rather than a command, there
	is no need for a new descent function. For example:

	fmod TEST is
	  inc MODEL-CHECKER .
	  ops a b c d e : -> Prop .
	  ops s t u v : -> State .

	  rl s => t .
	  rl t => s .
	  eq s |= a = true .
	  eq t |= b = true .
	endfm

	red in META-LEVEL :
	  metaReduce(['TEST],
	    '_|=_['s.State, '`[`]_['_\/_['a.Prop, 'b.Prop]]]) .

(2)	It is possible to use the model checker to define a "poor
   	mans" rule condition operator:

	fmod REWRITE-COND is
	  inc MODEL-CHECKER .
	  subsort State < Prop .
	  vars S S' : State .
	  eq S |= S = true .
	  op _=>*_ : State State -> Bool .
	  eq S =>* S' = (S |= [] ~ S') =/= true .
	endfm

	Each state S becomes a proposition that is true exactly in
	state S (note the power of having arbitrary terms for
	propositions). The existence of some path leading from state S
	to state S' is equivalent to the negation of, on all paths
	from state S, we never encounter state S'. The positive form
	of the latter is a statement in LTL and can be checked by the
	model checker.

	This technique has several major limitations:
	(a) No matching, both sides must be fully instantiated.
	(b) Only a single solution is searched for.
	(c) The set of reachable states from S must be finite
	    otherwise we don't get termination.
	(d) Both sides of =>* must belong to the sort State.

	Here's a really dumb example of how it can be used:

	mod TEST is
	  inc REWRITE-COND .
	  op f : MachineInt -> State .
	  ops g h : MachineInt MachineInt -> State .
	  vars N M : MachineInt .
	  rl f(N) => f(N / 2) .
	  rl f(N) => f((N + 1) / 2) .
	  crl g(N, M) => h(N, M) if f(N) =>* f(M) . 
	endm

	rew g(10, 4) .
	rew g(10, 3) .

Steven