Dear Maude (ab-)users A new alpha release, ~eker/AlphaRelease62/ is available. For people on this list who don't have a CSL account it's ftp-able from ftp.csl.sri.com in pub/users/eker/MaudeAbusers/alphaRelease62.tar.gz This version has a first approximation to the Maude 2.0 syntax, semantics and metalevel. Some Caveats: ============= Rewrite conditions still are not implemented (though they parse). The new rewrite semantics for unbound variables is not implemented. The compiler does not work in this version. meta-apply/meta-xapply/meta-match/meta-xmatch are not implemented. specials in the meta level are not implemented (those that worked in the old metalevel *might* work since I left this code in). meta-pretty-print has problems with kinds. meta-replace and meta-substitute are not implemented - but they could easily be written in Maude. I have made several changes to Narciso's spec for the Maude 2.0 meta level: (1) the sorts_. constructor is eliminated - the syntax now goes into the mod/fmod construtors. (2) sortInKind and sameComponent have been replaced by the more general sameKind operator. (3) completeName is lifted to types for simplicity. (4) the metalevel is now split into 3 modules for metaterms, metamodules and descent functions. I have only built a version for Linux. Some example reductions in the new metalevel: select META-LEVEL . red meta-reduce( fmod 'FOO is protecting 'MACHINE-INT . sorts none . none op 'fact : 'MachineInt -> 'MachineInt [none] . none eq 'fact['0.MachineInt] = '1.NzMachineInt . ceq 'fact['X:MachineInt] = '_*_['X:MachineInt, 'fact['_-_['X:MachineInt,'1.NzMachineInt]]] if '_>=_['X:MachineInt, '0.MachineInt] = 'true.Bool /\ '_<_['X:MachineInt, '20.MachineInt] = 'true.Bool . endfm, 'fact['21.NzMachineInt]) . red meta-reduce( fmod 'FOO is protecting 'STRING . sorts none . none none none none endfm, '"this is\na string".String) . red meta-reduce( fmod 'FOO is protecting 'FLOAT . sorts none . none none none none endfm, '_+_['1.0.Float,'1.0.Float]) . red completeName( fmod 'FOO is protecting 'BOOL . sorts 'NzNat ; 'Nat ; 'NzInt . subsort 'NzNat < 'Nat . subsort 'NzNat < 'NzInt . none none none endfm, '`[NzInt`]) . red meta-rewrite( mod 'FOO is nil sorts 'Foo . none op 'a : nil -> 'Foo [none] . op 'b : nil -> 'Foo [none] . none none rl ['c]: 'a.Foo => 'b.Foo . rl ['c]: 'b.Foo => 'a.Foo . endm, 'a.Foo, 2) . Steven Dear Maude Abusers, A new alpha release can be downloaded from http://www.csl.sri.com/~eker/Maude/Alpha63a/ Currently only linux is supported. This fixes numerous bugs is the last alpha release caused by the new treatment of conditions, variables and left->right sharing of common subexpressions. The fact that _only_ Mark-Oliver reported these bugs leads me to suspect that noone else tried the last alpha release. Here is a summary of changes (other than bug fixes) from the last alpha release: (1) Various things are renamed as agreed in previous discussions (see prelude.maude). (2) The leastSort function now takes membership axioms into account (I agreed this change of semantics with Jose yesterday). (3) Instead of returning error* for badly formed arguments, the descent functions first try any user equations, and failing that return an unreduced function call at the kind level; for example: select META-LEVEL . red metaReduce( fmod 'FOO is protecting 'MACHINE-INT . sorts 'Foo . none op 'a : nil -> 'Bar [none] . none none endfm, '_+_['1.MachineInt,'12.NzMachineInt]) . (4) metaParse now takes an extra argument of sort Type? which gives the component to which the result should parse; the constant anyType allows any component - the old behavior. In the case that metaParse fails it now returns noParse(n) if there was no parse where n in the index of the first bad token (counting from 0), or the number of tokens in the case of unexpected end of input; or ambiguity(r1, r2) if there were multiple parses, where r1 and r2 are the result pairs correspond to two distinct parses. Examples: red metaParse( fmod 'FOO is protecting 'MACHINE-INT . sorts 'Foo . none op '1 : nil -> 'Foo [none] . none none endfm, '1 '+ '12, anyType) . *** OK red metaParse( fmod 'FOO is protecting 'MACHINE-INT . sorts 'Foo . none op '1 : nil -> 'Foo [none] . none none endfm, '1 '+ '+ '12, anyType) . *** bad token red metaParse( fmod 'FOO is protecting 'MACHINE-INT . sorts 'Foo . none op '1 : nil -> 'Foo [none] . none none endfm, '1 '+ '2 '+, anyType) . *** unexpected end of input red metaParse( fmod 'FOO is protecting 'MACHINE-INT . sorts 'Foo . none op '1 : nil -> 'Foo [none] . none none endfm, '1, anyType) . *** ambiguity red metaParse( fmod 'FOO is protecting 'MACHINE-INT . sorts 'Foo . none op '1 : nil -> 'Foo [none] . none none endfm, '1, 'Foo) . *** OK red metaParse( fmod 'FOO is protecting 'MACHINE-INT . sorts 'Foo . none op '1 : nil -> 'Foo [none] . none none endfm, '1, '`[MachineInt`]) . *** OK Please try this version and remember to report bugs! Steven Dear Maude Abusers, A new alpha release can be accessed at SRI in ~eker/public_html/Maude/Alpha63b/ or downloaded from http://www.csl.sri.com/~eker/Maude/Alpha63b/ Currently only linux is supported. There are 4 changes from Alpha63a: (1) A bug reported by Paco which caused condition fragment trace information to be printed if the interpreter was processing a condition fragment at the instant a ^C interrupt was received is fixed. (2) A bug reported by Paco where an internal error can arise from repeated sequence of (a) rewriting in a module with t1 := t2 type condition fragments and (b) rentering (replacing) the module is fixed. (3) Loop mode now omits spaces around tokens ( , ) { } [ ] The Qids '\( '\, '\) '\{ '\} '\[ '\] provide the old behavior when printed in loop mode. This change was requested by Jose. (4) The module META-TERM now contains the sorts GroundTerm and GroundTermList with appropriate subsorting and operator declarations. This change was requested by Jose. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI in ~eker/public_html/Maude/Alpha63c/ or downloaded from http://www.csl.sri.com/~eker/Maude/Alpha63c/ Currently only linux is supported. The changes from Alpha63b are: (1) Operations op metaReplace : Context Term -> Term . op metaSubstitute : Term Substitution -> Term . removed from fmod META-TERM; these will be part of a library module being written in Maude by Jose. (2) Idempotence axioms added for set constructors: eq A:Assignment ; A:Assignment = A:Assignment . eq S:Sort ; S:Sort = S:Sort . eq S:SubsortDecl S:SubsortDecl = S:SubsortDecl . eq A:Attr A:Attr = A:Attr . eq M:MembAx M:MembAx = M:MembAx . eq E:Equation E:Equation = E:Equation . eq R:Rule R:Rule = R:Rule . (3) Descent functions op wellFormed : Module -> Bool . op wellFormed : Module Term ~> Bool . op getKind : Module Type ~> Kind . op getKinds : Module ~> KindSet . op maximalSorts : Module Kind ~> SortSet . op minimalSorts : Module Kind ~> SortSet . added to fmod META-LEVEL along with new constructor declarations sorts KindSet . subsort Kind < KindSet . op empty : -> KindSet [ctor] . op _&_ : KindSet KindSet -> KindSet [ctor assoc comm id: empty] . eq K:Kind & K:Kind = K:Kind . (4) Sort test meta level constructors op _::_ : GroundTerm Sort -> GroundTerm [ctor] . op _::_ : Term Sort -> Term [ctor] . op _:::_ : GroundTerm Sort -> GroundTerm [ctor] . op _:::_ : Term Sort -> Term [ctor] . are removed. Sort test are now considered to be regular operators with meta names like '_::`MachineInt so the meta term '0.NzMachineInt ::: 'NzMachineInt is now written as '_:::`NzMachineInt['0.NzMachineInt]) This gives a more uniform, easier to process meta-syntax and resolves a problem with sort test operators within contexts. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI in ~eker/public_html/Maude/Alpha63d/ or downloaded from http://www.csl.sri.com/~eker/Maude/Alpha63d/ This is a very minor update to Alpha63c: (1) A bug in the loop mode printing has been fixed so that for example '\`[ prints as [ with spaces around it (whereas '`[ prints as [ without spaces). (2) A bug in the lexical analyser has been fixed so that the character sequences `( and `) occuring in a multiline comment do not count towards balenced paretheses for determining the end of the comment. (3) At Jose's suggestion I have added extra projection functions to fmod META-MODULE in prelude.maude Steven Dear Maude Abusers, A new alpha release can be accessed at SRI in ~eker/public_html/Maude/Alpha63e/ or downloaded from http://www.csl.sri.com/~eker/Maude/Alpha63e/ Currently only linux is supported. The changes from Alpha63d are: (1) The following descent functions are now implemented: op wellFormed : Module Substitution ~> Bool . op metaApply : Module Term Qid Substitution MachineInt ~> ResultTriple? . op metaXapply : Module Term Qid Substitution MachineInt MachineInt MachineInt ~> Result4Tuple? . They support caching in the case that multiple solutions are extracted in order. There are some subtle issues that arise if the interpreter is ^C interrupted midway through a metaApply and the metamodule it is working on is invalidated by changing a module in the database that it depends on. (2) Operators whose sort structure allows a collapse from the kind level to an "output-sort" no longer generate a warning. Back in Feb 97 (accoding to my ChangeLog) we made a decision that collapsing from an error sort to an non-output-sort (i.e. a sort that the operator could not produce) was OK because this trivially happens when new sorts are added above in the component. I have been unable to reconstruct the justification for making a distinction between the non-output-sort case and the output-sort case and since we now allow rewriting at the kind level I cannot think of anything that might break. Incidently there was a bug in the output-sort computation loop that could cause memory corruption if the two argument components differed (as they can with a one sided identity). (3) Several memory leaks plugged. (4) A serious bug in the compilation of conditional collapse rules, provoked by an example such as: mod FOO is sort Foo . op a : -> Foo . op b : -> Foo . op f : Foo Foo -> Foo [comm] . crl [k] : f(Y:Foo, Y:Foo) => Y:Foo if Y:Foo =/= a . endm rew f(b, b) . has been fixed. There are still several things in the metalevel that remain to be implemented - the metaMatch/metaXmatch operators and some of the specials in metamodules. I've slightly modified an old example to demonstrate metaXapply: fmod ALL-ONE-STEP-REWRITES is including META-LEVEL . sort TermSet . subsort Term < TermSet . op _|_ : TermSet TermSet -> TermSet [assoc comm id: mt ctor] . op mt : -> TermSet [ctor] . var T : Term . var M : Module . var L : Qid . var N : MachineInt . op findAllRews : Module Term Qid -> TermSet . op findAllRewsAux : Module Term Qid MachineInt -> TermSet . eq findAllRews(M, T, L) = findAllRewsAux(M, T, L, 0) . eq findAllRewsAux(M, T, L, N) = if metaXapply(M, T, L, none, 0, maxMachineInt, N) :: Result4Tuple then (getTerm(metaXapply(M, T, L, none, 0, maxMachineInt, N)) | findAllRewsAux(M, T, L, N + 1)) else mt fi . endfm red findAllRews(mod 'FOO is protecting 'BOOL . sorts 'Foo ; 'Bar . subsort 'Bar < 'Foo . op 'a : nil -> 'Foo [none] . op 'b : nil -> 'Foo [none] . op 'c : nil -> 'Foo [none] . op 'f : 'Foo 'Foo -> 'Foo [assoc comm] . none none rl ['k] : 'f['X:Foo, 'Y:Foo] => 'X:Foo . rl ['k] : 'a.Foo => 'c.Foo . endm, 'f['a.Foo, 'b.Foo], 'k) . Steven Dear Maude Abusers, A new alpha release can be accessed at SRI in ~eker/public_html/Maude/Alpha64/ or downloaded from http://www.csl.sri.com/~eker/Maude/Alpha64/ Currently only linux and solaris are supported. The changes from Alpha63e are: (1) The special/hook mechanism has been reimplemented in what should be a more extensible way. All hooks now work at the metalevel and hook names have changed. In particular qidSymbol must be used rather than qidBaseSymbol in bubbles. (2) metaMatch and metaXmatch implemented (3) The garbage collector mark phase has been reimplemented to use less stack space for very deep terms in cases where the previous tail recursive approach failed (typically lists where the list constructor has an identity but no other attributes). (4) getName and getType are now implemented via maude strings rather than being builtin. (5) [_] : Qid -> Module implemented in maude. (6) Identity clashes detected. (7) match/xmatch commands now use the same code as metaMatch and metaXmatch and handle ^C interrupts more cleanly There are also various bug fixes: (1) No longer crashes if user tries to make a sort test at the meta level without defining SystemTrue and SystemFalse. (2) Fixed bug in op wellFormed : Module Substitution ~> Bool . that could cause memory corruption. (3) Fixed memory leaks in metaApply and metaXapply. (4) Output buffer is now flushed before reading input, even if output is not going to a tty. (5) Fixed bug in the statement importation code that leaves the imported module in a bad state and which causes importation to fail if the statements of a module are imported twice in succession without any intervening signature importation (which would return the imported module to a good state) from that module. (6) .*** and .--- are no longer considered to be the end of a command followed by a comment when encountered in a command, outside of parentheses. (7) Fixed wrap-around bug for string built-ins that was provoked by using very large numbers (typically maxMachineInt) to stand in for infinity or "end of string". Steven Various examples: red in META-LEVEL : metaReduce( fmod 'FOO is including 'BOOL . sorts 'MI . none op 'mi : nil -> 'MI [special(id-hook('MachineIntegerSymbol, nil))] . op '< : 'MI 'MI -> 'MI [special(id-hook('MachineIntegerOpSymbol, '<) op-hook('machineIntegerSymbol, 'mi, nil, 'MI) term-hook('trueTerm, 'true.Bool) term-hook('falseTerm, 'false.Bool))] . none none endfm, '<['9.MI, '10.MI]) . red in META-LEVEL : metaParse( fmod 'FOO is including 'QID-LIST . sorts 'Token ; 'Foo . none op 'tokens : 'Qid -> 'Token [special(id-hook('Bubble, '0 '10) op-hook('qidSymbol, ', nil, 'Qid) op-hook('nilQidListSymbol, 'nil, nil, 'QidList) op-hook('qidListSymbol, '__, 'QidList 'QidList, 'QidList) id-hook('Exclude, 'assoc 'com 'memo))] . op '`[_`] : 'Token -> 'Foo [none] . none none endfm, '`[ 'a 'b 'c '`] , anyType) . red in META-LEVEL : metaReduce( fmod 'FOO is nil sorts 'Foo ; 'Bool . none op 'true : nil -> 'Bool [special(id-hook('SystemTrue, nil))] . op 'false : nil -> 'Bool [special(id-hook('SystemFalse, nil))] . op 'a : nil -> 'Foo [none] . none none endfm, '_::`Foo['a.Foo]) . red in META-LEVEL : metaReduce( fmod 'FOO is nil sorts 'Foo ; 'Bool . none op 'itef : 'Bool 'Universal 'Universal -> 'Universal [special(id-hook('BranchSymbol, nil) term-hook('trueTerm, 'true.Bool) term-hook('falseTerm, 'false.Bool))] . op 'true : nil -> 'Bool [none] . op 'false : nil -> 'Bool [none] . op 'a : nil -> 'Foo [none] . op 'b : nil -> 'Foo [none] . none none endfm, 'itef['false.Bool, 'a.Foo, 'b.Foo]) . red in META-LEVEL : metaReduce( fmod 'FOO is nil sorts 'Foo ; 'Bit . none op '= : 'Universal 'Universal -> 'Bit [special(id-hook('EqualitySymbol, nil) term-hook('equalTerm, '1.Bit) term-hook('notEqualTerm, '0.Bit))] . op '1 : nil -> 'Bit [none] . op '0 : nil -> 'Bit [none] . op 'a : nil -> 'Foo [none] . op 'b : nil -> 'Foo [none] . none none endfm, '=['a.Foo, 'b.Foo]) . red in META-LEVEL : metaMatch(fmod 'FOO is protecting 'BOOL . sorts 'Foo ; 'Bar . subsort 'Bar < 'Foo . op 'a : nil -> 'Foo [none] . op 'b : nil -> 'Foo [none] . op 'f : 'Foo 'Foo -> 'Foo [comm] . none none endfm, 'f['X:Foo, 'Y:Foo], 'f['a.Foo, 'b.Foo], 1) . red in META-LEVEL : metaXmatch( fmod 'FOO is protecting 'BOOL . sorts 'Foo ; 'Bar . subsort 'Bar < 'Foo . op 'a : nil -> 'Foo [none] . op 'b : nil -> 'Foo [none] . op 'c : nil -> 'Foo [none] . op 'f : 'Foo 'Foo -> 'Foo [assoc comm] . none none endfm, 'f['X:Foo, 'Y:Foo], 'f['a.Foo, 'b.Foo, 'c.Foo, 'c.Foo], 0, 100, 0) . Dear Maude Abusers, A new alpha release can be accessed at SRI in ~eker/public_html/Maude/Alpha65/ or downloaded from http://www.csl.sri.com/~eker/Maude/Alpha65/ Currently only linux and solaris are supported. The changes from Alpha64 are: (1) There is a new attribute "frozen" that prevents an operators arguments from being rewritten by rules. Note that using this attribute effectively changes the denotational as well as the operational semantics of the frozen operator by disallowing the congruence proof rule for rl/crls. This is an extension of rewriting logic recently suggested by Jose. The frozen attribute is reflected by op frozen : -> Attr [ctor] . and is supported by all commands and descent functions that use rules. (2) There is a new command set show breakdown on/off . that causes a breakdown of mb applications, equational rewrites and rule rewrites to be printed after the "rewrites:" line but before the "result" line. mb applications are now counted in the main rewrite total. (3) The is a new command line flag "-interactive" that causes Maude to treat stdin/stdout/stderr as a tty and generate prompts even if isatty() returns false. This may be useful if Maude is being controlled by another process via pipes/fifos etc. (4) There is a new command for "position fair" rule rewriting; it has 3 forms: frewrite [nrRewrites, rewritesPerPosition] term . frewrite [nrRewrites] term . frewrite term . frew is an abbreviation for frewrite; the "debug" and "in :" modifiers are supported as they are for rewrite. Unlike rewrite which uses a leftmost outermost strategy for applying rules and reduces the whole term with equations after each succcessful rule rewrite, frewrite attempts to be position fair by making a number of depth first traversals of the term, and on each traversal, each position that existed at the start of the traversal is entitled to at most rewritesPerPosition rule rewrites when its turn comes around. After a rule rewrite succeeds, only the subterm that was rewritten is reduced with equations in order to avoid destroying positions that haven't yet had their turn for the current traversal. Traversals are made until nrRewrites rule rewrites have been made or until no more rewrites are possible. In the 2nd and 3rd forms, rewritesPerPosition defaults to 1. In the 3rd form nrRewrites defaults to infinity. The continue command works with frewrite in the same ways as it works with rewrite. In particular, considerable extra information about the current traversal is saved by the frewrite so that frewrite [n, k] t . continue m . produces the same final answer as frewrite [s, k] t . if s = n + m. The are a couple of caveats with frewrite: (a) If position fair rewriting stops mid traversal (typically the case with the 1st and 2nd forms) then the sort of the (incompletely reduced) result has not been calculated and is printed as "(sort not calculated)". (b) Position fair rewriting is not substitution fair; this is particularly apparent if you have an AC soup of messages and objects. Fair rewriting is reflected by op metaFrewrite : Module Term MachineInt MachineInt ~> ResultPair which is the meta equivalent of the first form of frewrite except that a final (semantic) sort calculation is performed at the end in order to produce a correct ResultPair. (5) Greedy matching is used for rules in situations (currently rewrite/metaRewrite and frewrite/metaFrewrite with non-conditional rules) where only a single matching substitution is required. With A/AC/ACU etc operators this may result in different substitutions being chosen and improved matching speed. (6) rewrite, continue and now frewrite take 64bit rather than 32bit integers. There are also various bug fixes: (1) abort works properly within the rewrite command in some cases where it used to run out of memory or crash. (2) rewrite/metaRewrite (and now frewrite/metaFrewrite) reset the round robin pointers in the rule tables to give reproducible (i.e. functional) results. (3) multiple files specified on the command line are now read in correctly; previously the 2nd and subsequent files would be read in after hitting eofs, even if the eof in question was not from the previous command line file but a file imported by a previous command line file. Steven Various examples: fmod FAIR is pr MACHINE-INT . sort Foo . op i : MachineInt -> Foo . op j : Foo -> Foo [frozen] . op f : Foo Foo -> Foo . var M : NzMachineInt . var X : Foo . rl i(M) => i(M - 1) . rl f(X, i(0)) => X . endfm set trace on . set trace whole on . frew f(f(i(2), i(1)), f(j(i(3)), i(2))) . rew f(f(i(2), i(1)), f(j(i(3)), i(2))) . set trace off . frew [1, 1] f(f(i(2), i(1)), f(j(i(3)), i(2))) . cont 3 . fmod ALL-ONE-STEP-REWRITES is including META-LEVEL . sort TermSet . subsort Term < TermSet . op _|_ : TermSet TermSet -> TermSet [assoc comm id: mt ctor] . op mt : -> TermSet [ctor] . var T : Term . var M : Module . var L : Qid . var N : MachineInt . op findAllRews : Module Term Qid -> TermSet . op findAllRewsAux : Module Term Qid MachineInt -> TermSet . eq findAllRews(M, T, L) = findAllRewsAux(M, T, L, 0) . eq findAllRewsAux(M, T, L, N) = if metaXapply(M, T, L, none, 0, maxMachineInt, N) :: Result4Tuple then (getTerm(metaXapply(M, T, L, none, 0, maxMachineInt, N)) | findAllRewsAux(M, T, L, N + 1)) else mt fi . endfm set show breakdown on . red findAllRews(mod 'FOO is protecting 'BOOL . sorts 'Foo ; 'Bar . subsort 'Bar < 'Foo . op 'a : nil -> 'Foo [none] . op 'b : nil -> 'Foo [none] . op 'c : nil -> 'Foo [none] . op 'f : 'Foo 'Foo -> 'Foo [assoc comm] . op 'g : 'Foo -> 'Foo [none] . none none rl ['k] : 'f['X:Foo, 'Y:Foo] => 'X:Foo . rl ['k] : 'a.Foo => 'c.Foo . endm, 'f['a.Foo, 'g['a.Foo]], 'k) . red findAllRews(mod 'FOO is protecting 'BOOL . sorts 'Foo ; 'Bar . subsort 'Bar < 'Foo . op 'a : nil -> 'Foo [none] . op 'b : nil -> 'Foo [none] . op 'c : nil -> 'Foo [none] . op 'f : 'Foo 'Foo -> 'Foo [assoc comm] . op 'g : 'Foo -> 'Foo [frozen] . none none rl ['k] : 'f['X:Foo, 'Y:Foo] => 'X:Foo . rl ['k] : 'a.Foo => 'c.Foo . endm, 'f['a.Foo, 'g['a.Foo]], 'k) . fmod TEST is pr META-LEVEL . op m : -> Module . eq m = (mod 'FAIR is protecting 'MACHINE-INT . sorts 'Foo . none op 'i : 'MachineInt -> 'Foo [none] . op 'f : 'Foo 'Foo -> 'Foo [none] . none none rl ['k] : 'i['M:NzMachineInt] => 'i['_-_['M:NzMachineInt, '1.NzMachineInt]] . rl ['k] : 'f['X:Foo, 'i['0.MachineInt]] => 'X:Foo . endm) . op t : -> Term . eq t = 'f['f['i['2.NzMachineInt], 'i['1.NzMachineInt]], 'f['i['3.NzMachineInt], 'i['2.NzMachineInt]]] . endfm red metaFrewrite(m, t, 1, 1) . red metaFrewrite(m, t, 2, 1) . red metaFrewrite(m, t, 3, 1) . red metaFrewrite(m, t, 4, 1) . red metaFrewrite(m, t, 5, 1) . red metaFrewrite(m, t, 6, 1) . red metaFrewrite(m, t, 7, 1) . red metaFrewrite(m, t, 8, 1) . red metaFrewrite(m, t, 9, 1) . red metaFrewrite(m, t, 10, 1) . red metaFrewrite(m, t, 11, 1) . red metaFrewrite(m, t, 0, 1) . set show breakdown off . Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in ~eker/public_html/Maude/Alpha66/ or downloaded from http://www.csl.sri.com/~eker/Maude/Alpha66/ Currently only linux and solaris are supported. Since there are new people on my "Maude Abusers" list I have put the release notes for previous versions in http://www.csl.sri.com/~eker/Maude/ReleaseNotes The changes from Alpha65 are: (1) Break symbol facility - select and deselect break symbols with: break select foo bar baz . break deselect quux . The break facility is switched on and off with set break on/off . When it is on, executing a mb/eq/rl with a break symbol on top will put you in the debugger. (2) match/xmatch commands reimplemented. They may now have a condition introduced by "such that" or equivalently "s.t."; for example match [2] in FOO : X * (Y + Z) <=? (a + b) * (a + d) s.t. A:Nat + B:Nat := X /\ A:Nat = Y . Also you can continue to look for more solutions with cont 4 . for example. Parsing is also a little smart in that the fact that both sides of <=? must be in the same component is taken in to account when resolving ambiguities. (3) search command reimplemented. The new syntax is search [<# solutions>] in : such that . The "[<# solutions>]", "in :" and "such that " parts are optional. "s.t." is an abbreviation for "such that". Possible relations are: => rewrites in exactly 1 step =>* rewrites in 0 or more steps =>+ rewrites in 1 or more steps =>! rewrites to normal form (i.e. a term in which no further rewrites are possible) For example: search [1] a * d + b * d + c * d + a * e + b * e + c * e =>+ X * Y such that W + Z := X . You can look for more solutions with the cont command as above. You may also interrupt a search in progress with ^C. In this case one of two things will happen dependeing on what Maude is doing at the instant you hit ^C. If Maude is not doing a rewrite, the command will exit. If maude is doing a rewrite you will end up in the debugger. In this latter case it is probably best to "abort ." since the debugger has no special support for search at the moment. When a search command terminates; either because there was a finite state graph and hence it can be determined there was no more solutions or because you used the "[<# solutions>]" part to limit the number of solutions found, the state graph is retained in memory until you switch modules or run another command the preforms rewriting. You can interrogate the state graph with the command: show path . which will show the sequence of states and rules going from the start term to the chosen state. Since the search command does a breadfirst search this will be a shortest path. (4) Timing reimplemented. Now if you do set timing off . set loop timing off . no calls to the system calls setitimer() or getitimer() will be made. This should enable the linux version of Maude to run under MS Windows using LINE (http://line.sourceforge.net/). Also the linux version should no longer report negative times. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in ~eker/public_html/Maude/Alpha67/ or downloaded from http://www.csl.sri.com/~eker/Maude/Alpha67/ This release has just 3 minor changes from Alpha66 that have been requested by various `hardcore' Maude users: (1) [requested by Merrill & Kemal] It is now possible to print out the current search graph generated by the search command with the command: show search graph . This command may be used whether or not the search is complete (in the case you have given a bound on the number of solutions); naturally only the portion of the graph actually constructed can be output. The format is a sequence of states, each with 0 or more arcs that look like: state , : arc ===> state () ... () : arc ===> state () ... () State numbers start at 0. Arc numbers for each state start at 0. If it is possible to reach the same next state via multiple rules, this is treated as a single arc with a list of rules. If it is possible to reach the same next state via the same rule with multiple substitutions, this is not explicitly represented (since we are not outputting substitutions). This feature is the main reason for the release. (2) [requested by Carolyn] The trace select facility now also recognizes rule labels rather than just top symbols; so if you keep your rule labels disjoint from your operator names you can selectively trace rules via their label. The recent break select facility now also works in the same way for consistancy. (3) [requested by Jose] If you `in' a file that does not end in a newline, Maude will fake a newline. This allows a command at the end of such a file to be recongnized as such (the `.' at the end of a command must be followed by a newline in order to be recognized as the end of a command rather than as user syntax). Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in ~eker/public_html/Maude/Alpha68/ or downloaded from http://www.csl.sri.com/~eker/Maude/Alpha68/ This release has just one change from Alpha67: the incorporation of an LTL model checker for a finite fragment of rewriting logic. To use the model checker you must load the file model-checker.maude You might also want the file dekker.maude that gives a slightly more realistic example of how to use the model checker. The syntax of LTL formula is given in the LTL module. The available operators are: True true False false ~ f not f /\ g and f \/ g or f -> g implies f <-> g iff @ f next (f holds in the next state) [] f always (f holds now and in all future states) <> f eventually (eventually we will reach a state where f holds) f U g strong until (f holds in all states until the first state where g holds and g will eventually hold) f W g weak until (f holds in all states until the first state where g holds but g need not eventually hold) f R g release (g holds now and in all states upto and including the first state in which f holds but f need not eventually hold) The elementary propositions are just terms (often constants) of sort Prop whose semantics are given by the user. Here's an example: mod TEST is inc MODEL-CHECKER . ops s t : -> State . rl s => t . rl t => s . ops a b : -> Prop . eq s |= a = true . eq t |= b = true . endm Here we have a trivial system with just 2 states, s and t, such that s always goes to t and t always goes to s. There are just two propositions, a and b. a is only true in s and b is only true in t. The semantics of propositions are defined by writing equations of the form eq |= = . where evaluates to true when the proposition matching holds in the state matching . It is only necessary to define the true case, anything else is assumed to be false. Note that since propositions can be arbitrary ground terms we can define parameterized families of propositions with a single equation (see the Dekker algorithm example). To check if a given LTL formula holds in the state transition graph from a given starting state we do a reduction: red |= . For example: red s |= [] <> a . *** a holds infinitely often - true red s |= [] <> b . *** b holds infinitely often - true red s |= [] a . *** a always holds - false red s |= [] (a \/ b) . *** (a or b) always holds - true When the formula is false, a counterexample is produced rather than false. A counterexample is an infinite sequence of states that can be generated in the system and which violates the checked property. A counterexample is presented as a pair of finite lists of states. The second list is a infinite cycle; the first list is a sequence that starts from the start state and reaches the first state of the cycle. Counterexamples are returned as terms using the constructors: op nil : -> StateList [ctor] . op __ : StateList StateList -> StateList [ctor assoc id: nil] . op counterExample : StateList StateList -> Result [ctor] . Here's a slightly more complex example: mod TEST2 is inc MODEL-CHECKER . ops a b : -> Prop . ops s t u v : -> State . rl s => t . rl s => u . rl u => v . rl v => s . rl t => s . rl t => t . eq s |= a = true . eq t |= b = true . endm red s |= <>[] b . *** eventually we reach a state where b *** holds forever - false red s |= []<> a . *** a holds infinitely often - false red s |= <>[] b \/ []<> a . *** one or other of the two previous *** formulae holds - true There are a couple of caveats: (1) The set of reachable states must be finite (otherwise the model check may not halt). (2) LTL formula apply to infinite traces; finite traces (i.e. deadlocks) are a problem. This is dealt with by adding self loops to deadlocked states. There is a module LTL-SIMPLIFIER that can optionally be included along with MODEL-CHECKER; it attempts to rearrange and simplify LTL formulae in order to produce smaller Buchi automata. Known problems: =============== (1) The rewrites used to compute transitions in the state graph are not counted. (2) The model checker responds badly to ^C interrupts. (3) Model checking cannot be traced in a useful way. (4) Counterexamples only list states and not labels, rules, or substitutions; already this looks rather ugly so it's not clear just what is the best format for counter-examples. (5) Buchi automaton generation is highly suboptimal (though better than many existing Buchi automaton-based LTL model checkers). This translates to more space/time usage and longer counter-examples than strictly necessary. (6) No self test for Buchi automaton generation; this is the area where unsoundedness is most likely to arise in a Buchi automaton-based LTL model checker. Design Issues ============= There are a number of UI issues with the model checker and Maude in general on which I would like input from Maude users. (1) To what extent should stuff be put in the prelude (e.g. strings) as opposed to in a library file (e.g. this version of the model checker)? (2) Is it the right thing that model checking is done by special reduce semantics for the _|=_ as opposed to special rewrite semantics for this symbol or a special command (like search)? (3) Should counterexamples be returned as terms (can be processed by user code, but ugly) or arbitrary print out (as a side effect but might be more readable)? (4) Would search be better if it were implemented by a special operator that return it's result as a term rather than as a command which prints it's result on the screen? Or should we have a metaSearch operator which works with meta-terms? (5) What info should go into each step of a counterexample? (6) Would it be useful to have a verbose mode where stuff is printed as the model check proceeds? what stuff would be useful? Some possibilities: (a) # states in very weak alternating automaton. (b) # states & # acceptance sets in generalized Buchi automaton. (c) # states and # accepting states in standard Buchi automaton. (d) # states explore in state transition graph. Could also wrap this stuff into the result term. Steven 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 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 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 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: I have yet to attempt a DTD for maudeml however the current implementation assumes a fragment something like: 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 Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in ~eker/public_html/Maude/Alpha71a/ or downloaded from http://www.csl.sri.com/~eker/Maude/Alpha71a/ Bug fixes: 1 A really nasty bug deep within the AU greedy matcher where a matching function that can return true/false/UNDECIDED was declared as returning bool - with the effect that when it failed as UNDECIDED (no match found, but match might exist) the rest of the AU greedy matcher saw this as a success. This results in unbound variables, missing matching subproblems and general anarchy. It is provoked by a really pathological example from Dilia which contains a pattern simple enough to trick the system into building a AU greedy matching automaton for it but complex enough to be able to fail with UNDECIDED on certain subjects. 2 A wrap around bug where highly ambiguous (billions of parses) terms/statements/commands causes MSCP10 to return a -ve number of parses which was handled ungracefully by the rest of the system - the fix is to treat -ve number of parses as equal to 2. This was provoked by a slight modification to Dilia's example. Incidentally Dilia's example also has 89 user sorts in a single connected component and exposes a performance problem with associative sort checking for which I don't have a fix at the moment - the naive n^3 algorithm is noticeably slow for n=89. 3 A bug in the metalevel parser provoked by the following example of Paco; run right after startup: red in META-LEVEL : metaParse(fmod 'FOO is nil sorts 'Foo . none op 'f : nil -> 'Foo [none] . none none endfm, 'f, 'Foo) . New features: 1 There are several changes to the XML support at Carolyn's request: (a) The XML output stream is flushed after every 2nd level closing tag. (b) XML output is now implemented for the following additiona commands: show search path . search { if } . (c) Each command that produces XML output will also produce an XML echo of that command if set show command on . which is the default. 2 A first version of profiling is implemented. Profiling is turn on and off by set profile on/off . When profiling is switched on, a count is kept of the number of executions of each mb/eq/rl. This can be displayed by show profile { } . The profile information is assciated with each module and is usually cleared at the start of any command that can do rewrites except continue. This behaviour can be changed with set clear profile on/off . For unconditional statements, the profile information is just the number of rewrites using that statement. For conditional statements there is also the number of matches since not every match leads to a rewrite due to condition failure. Also when searching, there can be multiple rewrites for each match since the condition may be solved in multiple ways. Also, there is a table that for each condition fragment gives (a) the number of times the fragment was initially tested (b) the number of times the fragment was test due to backtracking (c) the number of times the fragment succeeded (d) the number of times the fragment failed Normally (a) + (b) = (c) + (d). Special rewrites such as built-in rewrites and memoized rewrites are also tracked, but as these are associated with symbols rather than statements. For conciseness, symbols with no special rewrites, and statements that are not matched are omitted. Like tracing and break symbols/labels, switching profiling on substantially reduces performance. There are some limitations; metalevel rewrites are not displayed due to the ephemeral nature of metamodules. Also condition fragments associated with a match or search command are not tracked (though any rewrites initiated by such a fragment are). If you turn profiling on or off in the debugger you may get inconsistant results. 3 At Carolyn's request the metalevel now has "ascent" functions for uping stuff from the module database: op upMbs : Qid Bool ~> MembAxSet . op upEqs : Qid Bool ~> EquationSet . op upRls : Qid Bool ~> RuleSet . The first argument is the name of a module in the database. The second argument is true if imported statements are to be including. A module may examine itself: mod INTROSPECTION is inc META-LEVEL . op rules : -> RuleSet . rl rules => upRls('INTROSPECTION, false) . endm rew rules . mod SELF-REFLECTION is inc INTROSPECTION . op allRules : -> RuleSet . rl allRules => upRls('SELF-REFLECTION, true) . op myRules : -> RuleSet . rl myRules => upRls('SELF-REFLECTION, false) . endm rew myRules . rew allRules . 4 Loop mode now recognizes several special Qids in addition to '\t and '\n : '\s (forced) space '\r red '\g green '\y yellow '\b blue '\m magenta '\c cyan '\u underline '\! bold '\o revert to original color and style 5 The format attribute is now supported at the metalevel: op format : QidList -> Attr [ctor] . metaPrettyPrint() uses the above special Qids to approximate how the object level pretty-printer handles formatting instructions. Also I have changed the way Maude searches for files slightly: For prelude.maude it now checks: (a) the directories in the MAUDE_LIB environment variable (b) the directory containing the executable (c) the current directory For files specified by a bare file name, it checks (with .maude, .fm, .obj extensions if the filename does have one of these extensions): (a) the current directory (b) the directories in the MAUDE_LIB environment variable (c) the directory containing the executable In both cases (c) is an addition to the previous behaviour. Since some users just put library files such as model-checker.maude (there will be others in the near future) in the same directory as the executable rather than setting MAUDE_LIB this should enable Maude to find such files, e.g. with load model-checker Of course sticking configuration & library files in a bin directory is frowned upon. Also this might help with finding the prelude under windoze where the executable finding code breaks. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in ~eker/public_html/Maude/Alpha73/ or downloaded from http://www.csl.sri.com/~eker/Maude/Alpha73/ Running this new version is complicated by the fact it uses dynamic libraries, (gmp 4.1 and its C++ bindings) that will not be installed on most machines. Thus you may need to install them by one of these methods: (1) Obtain the source code from http://www.swox.com/gmp/ Configure with --enable-cxx for C++ support. Compile it with g++ 2.95.3 (because the C++ ABI changes with every compiler release you need the same g++ as I used to compile Maude). Install the two shared objects produced some place where your dynamic linker can find them. If you cannot write to system library directories and your sysadmins won't install them for you, you can always place them in ~/lib and point the LD_LIBRARY_PATH environment variable at this directory. (2) If this fails, you can get the shared objects I use from http://www.csl.sri.com/~eker/Maude/Lib/Linux/ or http://www.csl.sri.com/~eker/Maude/Lib/Solaris/ as appropriate and put them in ~/lib Then make the symbolic links and set LD_LIBRARY_PATH ln -s ~/lib/libgmp.so.3.3.0 ~/lib/libgmp.so.3 ln -s ~/lib/libgmpxx.so.3.0.2 ~/lib/libgmpxx.so.3 setenv LD_LIBRARY_PATH ~/lib Note also the the linux version is now dynamically linked whereas previous versions were statically linked and in particular you will need the libstdc++.so.3 that comes with g++ 2.95.3. If you run into linking problems you can use the ldd command to see what shared objects are needed. BTW I will be offline from Sat June 22 thru Sun July 7 so if you are going to try this new version I suggest install it before noon PST friday in case you need email support. Bug fixes: 1 A bug in sortLeq which caused unpredictable behavior when the two sorts were in different kinds - reported by Carolyn. 2 A bug which caused a incomplete module terminated by ctrl-D to not be discarded, causing unpredictable behavior - reported by Carolyn. 3 A bug where memoized rewrites were not counted - reported by Carolyn. Minor changes: 1 show all . and show ops . now display format attributes; further more generated gather info is only displayed if the op has arguments. 2 show all . now puts multiple subsorts in a single subsort declaration where possible. There are a number of major changes in this version, the last two of which will break most existing Maude code, however the existing model-checker.maude can be used unmodified. The iter theory =============== Unary operators may be declared to belong to the iter (short for iterated function symbol) theory. op f : Foo -> Foo [iter] . The sole purpose of this theory is to permit the efficient i/o and manipulation of very large stacks of functions symbols. The term f(f(f(X:Foo))) can be input as f^3(X:Foo) and will be output in that form. A term such as f^1234567890123456789(X:Foo) is too large to be input, output or manipulated is regular notation but can be input and output in this compact notation and certain (built in) manipulations may be efficient. The precise form the of compact iter theory notation is the prefix name of the operator followed by: ^[1-9][0-9]* (in lex regular expression notation) without no intervening white space. Note that f^0123(X:Foo) is not acceptable. Of course regular notation (and mixfix notation if appropriate) can still be used. Sort computations using subsort polymorphism are efficient: subsorts Odd Even < Foo . op f : Odd -> Even [ditto] . op f : Even -> Odd [ditto] . red f^1234567890123456789(X:Odd) . Membership axioms headed by iter operators are neither efficient nor correct (the same is true of assoc operators since we started allowing declarations at the kind level). Correctness may eventually be fixable, efficiency will not be. The situation with matching and rewriting is analogeous to the assoc theory - proper subterms of s^3(X:Foo), such as s^2(X:Foo) and s(X:Foo) can be matched and rewritten by means of extension. However for the pupose of calculating term depth, if the top level is 0, X:Foo is at level 1, not level 3. Fair rewriting treats a whole stack of iter operartors as a single position for the purposes of position fairness (again this is analogeous to the assoc case). The iter attribute is reflected by op iter : -> Attr [ctor] . A term such as f^1234567890123456789(X:Odd) is metarepresented as 'f^1234567890123456789['X:odd] metaParse() understands the compact iter theory notation and metaPrettyPrint() uses it. A version of the notation is also supported by the -xml-log command line flag, using the number attribute: The built in NATs ================= This is the primary application of the iter theory - an algebraic specification of the natural numbers that supports efficient builtin representation and operations. The natural numbers are constructed as follows: sorts Zero NzNat Nat . subsort Zero NzNat < Nat . op 0 : -> Zero [ctor] . op s_ : Nat -> NzNat [ctor iter special (...)] . Natural numbers can be input, and by default will be output in normal decimal notation; however 42 is just an alternative concrete syntax for s_^42(0). The command set print number on/off . controls whether decimal notation is used by the pretty printer. Note that redundant notation such as 00042 is not acceptable. metaParse() and metaPrettyPrint() support decimal notation however there is no other reflection of it - the metarepresentation of 42 is 's_^42['0.Zero] not '42.NzNat Nor is there XML support for it. Most of the usual arithmetic and bitwise operators are provided. They are not defined algebraically but could be given an algebraic definition by the user if desired. The operation semantics for most of the builtin operators is that you only get builtin behaviour when all the arguments are actually natural numbers. The exception is AC builtin operators which will compute as much as possible on natural number arguments and leave other arguments unchanged; so for example: red in NAT : gcd(gcd(12, X:Nat), 15) . results in: result Nat: gcd(X:Nat, 3) If the builtin operator does not disappear due to builtin semantics then user equations are tried. You can define functions on the Nats by matching into the sucessor notation; for example: fmod FACT is inc NAT . op _! : Nat -> NzNat . var N : Nat . eq 0 ! = 1 . eq (s N) ! = (s N) * N ! . endfm red 100 ! . red 1000 ! . It is even possible to get a specification of Z_{3} by fmod MOD3 is inc NAT . eq 3 = 0 . endfm However. apart from it's poor efficiency, this "writes up" from NzNat to Nat. Note that to avoid producing negative numbers, negation, subtraction and bitwise not are not provided. There is however symmetric difference: op sd : Nat Nat -> Nat [comm special (...)] . There is a limit on exponentiation in that builtin behavior will not occur if the first agumnent is > 1 and the second argument is too large. Similarly left shift does not work if the first argument is >= 1 and the second argument is too large. Currently "too large" means greater than 1000000 but this may change. Warning: it is easy to fill your machine's memory by generating huge natural numbers. Modular exponentiation op modExp : Nat Nat NzNat ~> Nat [special (...)] . has no such limits and may be useful for cryptographic algorithms. The built in INTs ================= The integers are constructed on top of the natural numbers as follows: sorts NzInt Int . subsort NzNat < NzInt Nat < Int . op -_ : NzNat -> NzInt [ctor special (...)] . Integers can be input, and by default are output in normal decimal notation; however -42 is just an alternative concrete syntax for - 42 which itself is just an alternative concrete syntax for - s_^42(0). As with NATs this notation is supported by metaParse() and metaPrettyPrint() but not by the metaterm representation or XML. Many of the operations in NAT extend to the integers, and a few new ones are provided. Bitwise operations on negative integers use the 2's complement representation. The built in RATs ================= The rationals are constructed on top of the integers and natural numbers as follows: sorts NzRat Rat . subsorts NzInt < NzRat Int < Rat . op _/_ : NzInt NzNat -> NzRat [ctor prec 31 gather (E e) special (...)] . Rationals can be input, and by default are output in normal decimal notation; however -5/42 is equivalent to -5 / 42 which is equivalent to - 5 / 42 which really denotes - s_^5(0) / s_^42(0). As with NATs and INTs this notation is supported by metaParse() and metaPrettyPrint() but not by the metaterm representation or XML. The numerator and denominator of a rational may contain common factors but these are removed by a single builtin rewrite whenever the rational is reduced (_/_ is not a free constructor). Some of the operations in INT are extended to rationals and a few new ones are provided. However unlike operations on the NATs and INTs these are defined in Maude by equations and may do some rewriting even when their arguments are not properly constructed rationals. Note that the choice of equations for defining operations on the rationals is motivated by performance - simpler equations are possible in many cases but they turn out to have a big performance penalty. op trunc : Rat -> Int . rounds its argument towards 0. op frac : Rat -> Rat . gives the fraction part of its argument and this always has the same sign as its argument. MachineInts replaced by number hierarchy ======================================== This is the most far reaching change since most of the builtin operations (except the model checker and sat solver) are affected to some extent and have their semantics subtly or not so subtly altered. fmod FLOAT is unaffected except some special hooks are renamed for consistancy. fmod STRING now protects NAT rather than MACHINE-INT. Nats are used in place of MachineInts which means that operations can no longer take nehative arguments. The String <-> MachineInt conversion functions are deleted. fmod FLOAT-CONVERSION is deleted. fmod NUMBER-CONVERSION is added to consolidate all the conversion functions between the 3 major builtin data types (Nats/Ints/Rats, Floats and Strings). op float : Rat -> Float . Computes the nearest Float to a given Rat. If the absolute value of the Rat falls outside the range representable by IEEE-754 double precision finite floating point numbers, Infinity or -Infinity is returned as appropriate. This seems consistant since Infinity & -Infinity are used to handle out-of-range situations in the Float world. op rat : FiniteFloat -> Rat . Converts finite Floats to Rats exactly (since every IEEE-754 finite floating point number is a rational number). Of course if the result happens to be a Nat or an Int that is what you get. rat(Infinity) and rat(-Infinity) do not reduce since they have no reasonable representation in the Rat would. It is intended that float(rat(F:FiniteFloat)) = F:FiniteFloat though I am relying on a 3rd party library (GNU gmp) for the yucky bit twiddling and I have not checked it's correctness. Also note that counterintuitive results are possible when converting from the approximate world of Floats to the exact world of Rats: red rat(1.1) . gives result NzRat: 2476979795053773/2251799813685248 This is because 1.1 cannot be represented exactly as a Float and the nearest Float is 1.100000000000000088817841970012523233890533447265625 which is the above rational. op string : Rat NzNat ~> String Converts a Rat to a String using a given base which must lie in the range 2,...,36. Of course Rats that are really Nats or Ints are converted to string representations of Nats or Ints so red string(-1, 10) . gives result String: "-1" op rat : String NzNat ~> Rat Converts a String to a Rat using a given base which must lie in the range 2,...,36. Of course if the result happens to be a Nat or an Int that is what you get. Currently the function is very strict about what strings are converted: the string must be something that the Maude parse would recognize as a Nat, Int or Rat. This could be changed to a more generous interpretation in the future. op string : Float -> String . op float : String ~> Float . These work as they did in FLOAT-CONVERSION. In particular float(string(F:Float)) == F:Float . op <_,_,_> : Int String Int -> DecFloat [ctor] . op decFloat : Float Nat -> DecFloat . DecFloats provide the means for arbirary formating of Floats as they did in FLOAT-CONVERSION. A DecFloat consists of a sign (1, 0 or -1), a String of digits and a decimal point position (0 is just in front of first digit, -ve is to the left, +ve is to the right). Thus < -1, "123", 11 > represents -1.23e10 . decFloat(F, N) converts F to a decFloat, rounding to N significant digits using the IEEE-754 "round to nearest" rule with trailing zeros if need. If N is 0, an _exact_ DecFloat representation of F is produced - this may require hundreds of digits. For any well formed Nat N: decFloat(Infinity, N) = < 1,"Infinity",0 > and decFloat(-Infinity, N) = < -1,"Infinity",0 > In fmod QID, the only operations that depended on MACHINE-INT were the deprecated backward compatibility operations so these are deleted. In fmod META-TERM some function definitions are rewritten to avoid the need for maxMachineInt. In fmod META-MODULE, Nats replace MachineInts and NatLists replace MachineIntLists: sort NatList . subsort Nat < NatList . op __ : NatList NatList -> NatList [ctor assoc] . op strat : NatList -> Attr [ctor] . op prec : Nat -> Attr [ctor] . In fmod META-LEVEL we need a notion of unbounded that was previously supplied by maxMachineInt. We use: sort Bound . subsort Nat < Bound . op unbounded : -> Bound . Also Nat replaces MachineInt in: op noParse : Nat -> ResultPair? [ctor] . The descent functions with modified semantics are: op metaRewrite : Module Term Bound ~> ResultPair . op metaFrewrite : Module Term Bound Nat ~> ResultPair . Rewrite limit is a Bound; it must be >= 1 and may be unbounded. Gas is now a Nat and must be >= 1. op metaApply : Module Term Qid Substitution Nat ~> ResultTriple? . op metaXapply : Module Term Qid Substitution Nat Bound Nat ~> Result4Tuple? . op metaMatch : Module Term Term Condition Nat ~> Substitution? . op metaXmatch : Module Term Term Condition Nat Bound Nat ~> MatchPair? . op metaSearch : Module Term Term Condition Qid Bound Nat ~> ResultTriple? . Last argument is always the solution number which is now a Nat. For metaXapply() and metaXmatch() the minimum depth is now a Nat. For metaXapply(), metaXmatch() and metaSearch() the maximum depth is now a Bound and can take the value unbounded. Statement Attributes ==================== Statements can now take attributes; currently only two statement attributes are available - more are planned. They are label, which is followed by an identifier and metadata which is followed by string. For example: eq foo = bar [label e1 metadata "lemma 1"] . cmb a : b if c [label m1] . rl quux => baz [metadata "\cite{Bloggs:2001}"] . Note that membership axioms and equations can now take labels rather than just rules. One use for such labels is in conjunction with the tracer/debugger. For example set trace on . set trace select on . trace select e1 . would cause selective tracing of rewrites that have e1 as top symbol _or_ involve a statement labeled e1 such as the equation above. In a similar vein it is possible to break into the debugger when a given labeled statement is about to execute: set break on . break select e1 . There will be other applications for labeled equations in the future. The old style rule labels are now supported as syntactic sugar, even for membership axioms and equations: eq [e1]: foo = bar [metadata "lemma 1"] . cmb [m1]: a : b if c . The metadata attribute is intended to hold data about the statement in whatever syntax the user cares to create/parse. It is like a comment that is carried around with the statement. Usual string escape conventions apply. Statement attributes and the new syntax for labels is reflected by the following changes to the metasignature: op label : Qid -> Attr [ctor] . op metadata : String -> Attr [ctor] . op mb_:_[_]. : Term Sort AttrSet -> MembAx [ctor] . op cmb_:_if_[_]. : Term Sort EqCondition AttrSet -> MembAx [ctor] . op eq_=_[_]. : Term Term AttrSet -> Equation [ctor] . op ceq_=_if_[_]. : Term Term EqCondition AttrSet -> Equation [ctor] . op rl_=>_[_]. : Term Term AttrSet -> Rule [ctor] . op crl_=>_if_[_]. : Term Term Condition AttrSet -> Rule [ctor] . There is no distinction at the sort level between statement and operator attributes but of course you should only pass operator attributes to operators and statement attributes to statements. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in ~eker/public_html/Maude/Alpha75a/ or downloaded from http://www.csl.sri.com/~eker/Maude/Alpha75a/ This version needs the same dynamic libraries as Alpha73. Bug fixes: 1 Bug in the tracing of polymorphic ops: set trace on . set trace select on . red in BOOL : true == false . Reported by Paco. 2 Bug in the metalevel uping of constants and variables at the kind level cause (illegal) Qids like 'a.'[Foo`] rather than 'a.`[Foo`] - reported by Paco. Other changes: 1 Free theory uses new style order-sorted discrimination nets for equational rewriting. This allows subsumed equations to be discarded. 2 Interpretation of discrimination nets optimized. 3 Special handling for free theory ternary symbols. 4 Substitution coloring; this helps with a performance bug noted in earlier release notes where there is a equation with a huge ground rhs. This would previously force all substitutions to have a slot for every subterm in such a rhs. Substitution coloring allows slots to be reused. 5 Two of the four pretty pinters rewritten to handle more disambiguation corner cases. There are 11 classes of operator that have special i/o representation and disambiguation needs: Polymorphs sort tests itor symbols variables flattened assoc symbols nats ints rats floats strings qids The last 3 have always been handled. The first 3 are still not handled. The middle 5 are now handled correctly by the object level. The two remaining pretty printers (metaPrettyPrint and term graph pretty printer) still need to be rewritten. The following ambiguous examples shows some of the corner cases now handled. fmod OVERLOAD is pr NUMBER-CONVERSION . sorts Foo Bar . ops 1 -42 1/2 N:Nat : -> Foo . op a : -> Foo . op a : -> Bar . op f : Foo Foo -> Foo [assoc] . op f : Bar Bar Bar -> Bar . endfm red 1 . red -42 . red 1/2 . red N:Nat . red f(a, a, a) . There are some new error messages for cases where a signature is created such that no disambiguation is possible. 6 Ctor declarations are now stored and printed out correctly with show all . whereas previously they were just comments. Ditto attribute does not copy ctor attribute but allows a ctor attribute to be included - this is because subsort polymorphic overloaded operators may reasonably have differing ctor status. 7 Term coloring partly implemented. This feature was called ctor debugging in previous discussions. The command is set print color on . Symbols within terms that are being executed (i.e. in trace or the final result of a reduce) are colored as follows: reduced, ctor not colored reduced, non-ctor, strangeness below blue reduced, non-ctor, no strangeness below red unreduced, no reduced above green unreduced, reduced directly above magenta unreduced, reduced not directly above cyan Strangeness is a colored operator. The idea is that red and magenta indicate initial locus of a bug while blue and cyan indicate secondary damage. Green denotes reduction pended and cannot appear in final result. It is instructive to run a trace of a reduction involving lazy operators: fmod SIEVE is pr NAT . sort List . subsort Nat < List . op nil : -> List [ctor]. op _,_ : Nat List -> List [ctor prec 31 gather (e E) strat (1 2 0)] . op l : Nat List -> List [ctor strat (0)] . op force : List Nat -> List . op ints-from : Nat -> List [ctor] . op sieve : List -> List . op filter : List Nat -> List . var N M : Nat . var L : List . eq ints-from(N) = l(N, ints-from(s(N))) . *** infinite list of Nats eq sieve(l(N, L)) = l(N, sieve(filter(L, N))) . *** the actual sieve eq filter(l(N, L), M) = if M divides N then filter(L, M) else l(N, filter(L, M)) fi . eq force(L, 0) = nil . eq force(l(N, L), s(M)) = N, force(L, M) . *** force lazy list endfm set trace on . set trace whole on . set print color on . red force(sieve(ints-from(2)), 10) . There is also Jose's missing case example: fmod NAT-MSET-MIN is sorts Nat NatMSet . subsort Nat < NatMSet . op 0 : -> Nat [ctor] . op s : Nat -> Nat [ctor] . op _ _ : NatMSet NatMSet -> NatMSet [assoc comm ctor] . op _<_ : Nat Nat -> Bool . op min : NatMSet -> Nat . vars N M : Nat . var S : NatMSet . eq 0 < s(N) = true . eq s(N) < 0 = false . eq s(N) < s(M) = N < M . eq min(N N S) = min(N S) . ceq min(N M S) = min(N S) if N < M . ceq min(N M) = N if N < M . eq min(N) = N . endfm set print color on . red min(s(0) s(s(0))) . red min(s(s(0)) min(s(0) s(0))) . Color & style due to format attributes are implicitly turned off to avoid confusion when "print color" is on. Operators that have assoc or iter attributes need to have all of their declarations have ctor or be without ctor. For other operators, if they have both with and without ctor declarations, ctorness is computed from arguments sorts. Finally there is a command introduced in Alpha73 that I forgot to document: set print rat off . switches off the special printing for _/_ in fmod RAT. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha76/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha76/ My Maude alpha release site now requires authentication: User Name: maudeabuser Password: bughunter The linux version is statically linked, while the solaris version only depends are standard solaris dynamic libraries - you should not have to install any shared objects to run these versions. This and future alpha releases include the source tree (alpha76.src.tar.gz). This is done for several reasons: (1) To allow static binaries while preserving your right to link against newer versions of GNU LGPL'd libraries it uses. (2) My hard drive died during the level 0 backup while I was at WRLA 2002 and this has left me paranoid about having the only Maude source tree on my local disk. (3) To allow white box testing. (4) Several people have expressed an interest in porting it to their favorite platform - although this may be premature as the source tree is rather messy and I'm planning a big reorganization before the end of the year. Note that the source code is not yet under the GNU GPL, and like the binaries should not be redistributed. Currently it only compiles with g++ 2.95.3. I will be moving it to a newer C++ compiler/stdc++ library in the near future. Other requirements are recent versions of bison and flex and the following 3rd party libraries: Doug Lea's malloc (ftp://g.oswego.edu/pub/misc/malloc.c) BuDDy (http://www.itu.dk/research/buddy/) Tecla (http://www.astro.caltech.edu/~mcs/tecla/) GNU GMP (http://www.swox.com/gmp/) I have mirrored them in: http://www.csl.sri.com/~eker/Maude/Lib/Src Bug fixes: (1) We used to allow iter operators with more or less than one argument which could provoke internal errors: fmod SUCC-BUG is sort Foo . op crash : -> Foo [iter] . endfm (2) The following example used to take O(n^3) time to abort due to a cascade of eager big num computations that are redone and thrown away during the stack unwinding (n = # of stack frames). fmod FACT is pr NAT . op _! : Nat -> NzNat . vars N M : Nat . eq 0 ! = s 0 . eq (s N) ! = s N * N ! . endfm red 10000 ! . ^C abort . The bug is now partly fixed by an extra test for abort in ACU_NumberOpSymbol; however the cascade of AC normalization is still O(n^2) (but far less noticable). A better ACU representation will eventually get this down to O(n log n) which will be unnoticable to the interactive user. (3) The performance bug noted in the Alpha71a release notes wrt associativity checking for kinds with many user sorts (Dilia's example) is mostly resolved by replacing the O(n^3) algorithm with a O(k.n^2) algorithm where k is the width of the sort diagram generated for the associative operator. k is bounded by the number of user sorts, n, and when n is large, k is typically much smaller. (4) We now check that terms kinds agree in eq/ceq/rl/crl meta-statements and =/:=/=> meta-condition fragments and metaMatch/metaXmatch/metaSearch descent functions. We also that term and sort kinds agree in mb/cmb meta-statements and : meta-condition fragments. The first of this large family of related bugs was reported by Peter. (5) The check for collapsing to a larger or incomparable sort via idempotence was the wrong way around. (6) Some missing operator sort declarations added to the prelude. Other changes: (1) Command line editing is supported using Tecla. There are a large number of commands and options - see http://www.astro.caltech.edu/~mcs/tecla/ for details. Basics: left/right arrow keys to move within line, up/down arrow keys for history and tab for file name completion. Also you get a continuation prompt rather than a blank line when Maude is expecting more input. (2) The line wrapper now notices changes in the terminal width (courtesy of Tecla). (3) The line wrapper uses a new algorithm that avoids inserting a newline when the next token (say a Nat or a String) is so long that it will hardwrap anyhow. (4) You can now use \ in String constants (just like in C++): red in STRING : "'The time has come,' the Walrus said, \ 'To talk of many things: \ Of shoes and ships and sealing wax, \ Of cabbages and kings; \ Of why the sea is boiling hot, \ And whether pigs have wings.'" . (5) The frozen attribute takes a list of numbers to freeze individual arguments; e.g.: op i : Foo Foo Foo -> Foo [frozen (1 3)] . Frozen on it's own freezes all arguments as before. The metalevel now only supports the list of numbers version: op frozen : NatList -> Attr [ctor] . though there is a nasty but temporary hack to allow the current version of Full Maude to run. This change necessitated replacing the frewrite algorithm - this is a good place to look for bugs. (6) There is a new attribute owise (or otherwise) that is only permitted for equations. An owise equation will only be applied at a redex if no regular equations apply at that redex. This feature should be used with care as it can make your specifications harder to analyze. In some ways it a bit like cut in Prolog or goto in C++. The reflection is op owise : -> Attr [ctor] . (7) The remaining ANSI escape sequences are now available in the format attribute as follows: p black (for pitch black... b is already used.) w white P Background black R Background red G Background green Y Background yellow B Background blue M Background magenta C Background cyan W Background white ? Dim f Blink (for flash... b is already used.) x Reverse video h Hidden I've included a modified version of interfere.maude from the WRLA 2002 demo to show what tricks are possible. (8) Warnings and advisories now have a more standardized form. Quoting of user identifiers used be very inconsistent, as well as confusing since ' and " can legally appear in identifiers. Instead color is used: Warning: red Advisory: green User identifiers: magenta However quoting of whole statments on lines of their own are not colored. (9) Compilation of operator declarations is now done lazily just as compilation of eqs/rls/mbs has been done for some time. This now means that some warnings and advisories will only show up when you actually do a reduction in a module. The benefit is a saving of cpu cycles and memory for loading large programs (such as Full Maude) where execution occurs in the last module. (10) There are a slew of under-the-hood changes such as an optimization in the main AC/ACU matcher, a new memory allocation mechanism for dag nodes and linking against newer 3rd party libraries. Hopefully these shouldn't have introduced any new bugs... Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha76a/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha76a/ This is an urgent bug fix release that just includes binaries and the changed source files. See Alpha76 for everything else. Bug fixes: (1) metaXmatch() complains about kind clashes between the pattern and subject terms; but this is perfectly legal for metaXmatch(). I overdid the checking introduced for bug fix (4) from Alpha76. Thanks to Carolyn for spotting this. (2) Tecla does not play well with Emacs (or vice versa depending on your point of view). There are two new command line flags: -tecla Use Tecla -no-tecla Don't use Tecla The default is to use Tecla unless: (a) standard input is not a tty; or (b) TERM environment variable is set to emacs or dumb. Thanks to Joe Hendrix for spotting this bug. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha77/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha77/ Alpha release site authentication: User Name: maudeabuser Password: bughunter Bug fixes: (1) A bug when reading files that don't end in with a newline. Maude usually fakes a newline in this case, but if the is an in/load near the end of the offending file, the flag to fake a newline will be set before the included file is read and then overwritten by the handling of the included file before the newline is faked. This is now fixed by stacking the flag. This bug was found by Peter. (2) There was a portability bug in the memory management that meant Maude would not work unless compiled with g++ 2.95.3. This is partly fixed by a rewrite of the memory manager. Although it's still not 100% ANSI compliant it should port to most platforms now. There are no new features but there are a lot of changes under the hood: (1) It's now compiled with g++ 3.2 and the ANSI compliant libstdc++ version 3. This may give a performance gain for some examples. I will probably remove support for the non-ANSI compliant libstdc++ version 2 in the near future. (2) In full AC/ACU matching, element variables are now pushed in to the bipartite graph problem rather than the Diophantine system problem in order to reduce the search space. This should help with Merrill's "killer rules" during search/model checking. (3) Iterators used for A/AU/AC/ACU arguments lists; this may improve performance. SPEED_HACKs removed from A/AU/AC/ACU code. (4) More special casing for full AC/ACU matching. (5) AC/ACU subpatterns of the form f(X, t) where t is ground and X is not yet bound now get to use greedy matching even if X occurs elsewhere in pattern or condition - since subpatterns with this form can match in at most one way. (6) A number of low level changes to the AC/ACU code to avoid unnecessary copying and unpredicatable branches. (7) Matching a variable with extension (i.e. at the top) against an AC/ACU subject is now a little smarter. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha78/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha78/ Alpha release site authentication: User Name: maudeabuser Password: bughunter Bug fixes: (1) A warning is now generated for single argument empty syntax operators; these have never been allowed in eithe OBJ3 or Maude. Bug reported by Feng Chen. The main change in this version is a new term representation along with new matching and renormalization algorithms for the AC and ACU theories. For some simple patterns, this enables rewrites that would have taken time linear in the size of the subject (using the old greedy matching) to execute in log time (using the new greedy matching). This can be a big win if the subject has thousands of alien subterms under an AC/ACU operator. In particular it is now feasible to implement maps using AC or ACU rewriting - see mapExample.maude So far the new method is only implemented for a small subset of patterns and in particular it does not work at all for conditional equations. Nor does it work for rules in model checking or search where all matches are needed. In these cases the subject must be converted to the old representation in order to use the old algorithms, and thus things can get slower. I expect to increase the subset of patterns handled and make the heuristics for switching between representations smarter in future versions. However since this is such a radical change to the guts of the rewrite engine I am putting this version out so people can check if anything is broken. Two changes that you may notice: (1) The term ordering for terms headed by AC/ACU operators has changed slightly. (2) The matches chosen and hence the sequence of rewrites may differ. Neither of these should be a problem if your specification is confluent. There are some minor changes agreed at various Maude teleconferences: (1) =>1 replaces => for one step search in search command. This is to avoid confustion with => in conditions which means search for 0 or more step proofs (=>* in search command). This also affect the XML output. (2) fmod NUMBER-CONVERSION renamed to CONVERSION since Carolyn pointed out that it also involves strings. Unfortunately this breaks Full Maude. (3) _|=_ which use to do double duty in the model checker is now just used for satisfaction and lives in fmod SATISFACTION. The operator to actually start the model checker is now: op modelCheck : State Formula ~> ModelCheckResult . This enables checking satisfaction without invoking the model checker. (4) If you get an internal error, bug report address is now: maude-bugs@maude.cs.uiuc.edu Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha79/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha79/ Alpha release site authentication: User Name: maudeabuser Password: bughunter Bug fixes: (1) Bug where pointer was printed in a "can't continue." message if cont . was typed after start up. (2) iter matching against a bare variable with extension now works so for example you can do: mod ITER-SEARCH is inc NAT . op f : Nat -> Nat . var X : Nat . rl X => f(X) . endm search 6 =>1 X . Not so much a bug as an unimplemented corner case. (3) A nasty bug in the ACU/AC sort calculation where I assumed that assignments to variables couldn't be in the error sort; this assumption no longer holds since we have variables at the kind level. This bug is exposed by the following code. fmod ACU-SORT-BUG is sort Foo . ops a b c d e : -> Foo . op k : -> [Foo] . op f : Foo Foo -> Foo [assoc comm] . var K : [Foo] . eq f(a, K) = K . endfm red f(a, b, c, k) . *** result should be at kind level (4) Similar bug in the AU/A sort calculation. (5) Bug in ACU Red-Black matcher code that could miss matches against subjects of the form f(a, X), a ground, if the subject had a strange sort structure. (6) Similar bug in specialized matcher for f(X, Y) case. (7) Stale pointer bug in the code that echos match/search commands in the case that the pattern flattened or collapsed during normalization (reported by Christiano Braga). (8) A nasty bug in the original greedy matcher, where it fails to find a match, but decides there is no match rather than running the full matcher. fmod GREEDY-BUG is sorts E1 E2 P T . subsort E2 < E1 P < T . op f : P P -> P [assoc comm] . op f : T T -> T [assoc comm] . op i : T -> T . op a : -> E2 . op b : -> E1 . ops c d : -> P . op ok : -> T . eq i(f(X:E1, X:E1, Y:P, Z:P)) = ok . endfm red i(f(a, a, b, b, c, d)) . match i(f(X:E1, X:E1, Y:P, Z:P)) <=? i(f(a, a, b, b, c, d)) . The main change in this version is that I have implemented the new AC/ACU representation and matching for a wider class of patterns. I've also revamped the old AC/ACU matcher and made a few optimizations in other places. To see how the recent changes have affected AC/ACU rewriting I have run the last 3 alphas on the mapExample.maude that I distributed with Alpha78 and 4 other AC/ACU benchmarks that I've put in: http://www.csl.sri.com/~eker/Maude/Benchmarks/ Here are the results I got on a 2.8GHz Xeon. Some of the benchmarks are very stack intensive so remember to "unlimit stacksize" to avoid a stack overflow segmentation fault. Also you need lots of RAM. 8 cpu minutes is where my patience gives out :) Alpha79 -------- setHierarchy.maude rewrites: 6667125 in 6550ms cpu (6560ms real) (1017881 rewrites/second) simpleSet.maude rewrites: 766675 in 2480ms cpu (2480ms real) (309143 rewrites/second) rewrites: 833341 in 2670ms cpu (2670ms real) (312112 rewrites/second) tautology.maude rewrites: 554823 in 990ms cpu (990ms real) (560427 rewrites/second) threeElt.maude rewrites: 2192505 in 44780ms cpu (44770ms real) (48961 rewrites/second) mapExample.maude rewrites: 599 in 0ms cpu (0ms real) (~ rewrites/second) rewrites: 5999 in 20ms cpu (10ms real) (299950 rewrites/second) rewrites: 59999 in 210ms cpu (210ms real) (285709 rewrites/second) rewrites: 599999 in 2820ms cpu (2830ms real) (212765 rewrites/second) Alpha78 -------- setHierarchy.maude rewrites: 6667125 in 109820ms cpu (109830ms real) (60709 rewrites/second) simpleSet.maude > 8 cpu minutes > 8 cpu minutes tautology.maude rewrites: 554823 in 1550ms cpu (1550ms real) (357950 rewrites/second) threeElt.maude rewrites: 2192505 in 60800ms cpu (60790ms real) (36060 rewrites/second) mapExample.maude rewrites: 599 in 0ms cpu (10ms real) (~ rewrites/second) rewrites: 5999 in 10ms cpu (10ms real) (599900 rewrites/second) rewrites: 59999 in 220ms cpu (210ms real) (272722 rewrites/second) rewrites: 599999 in 2820ms cpu (2820ms real) (212765 rewrites/second) Alpha77 -------- setHierarchy.maude rewrites: 6667218 in 48610ms cpu (48610ms real) (137157 rewrites/second) simpleSet.maude > 8 cpu minutes > 8 cpu minutes tautology.maude rewrites: 554819 in 1560ms cpu (1560ms real) (355653 rewrites/second) threeElt.maude rewrites: 2193693 in 50690ms cpu (50700ms real) (43276 rewrites/second) mapExample.maude rewrites: 599 in 0ms cpu (0ms real) (~ rewrites/second) rewrites: 5999 in 150ms cpu (140ms real) (39993 rewrites/second) rewrites: 59999 in 55000ms cpu (55000ms real) (1090 rewrites/second) > 8 cpu minutes There are also some changes to the source code that should make porting easier; in particular the #pragmas that caused linking problems with certain versions of g++ are gone. I used g++ 3.2. I notice that some people have been discouraged from using Alpha78 because it breaks FullMaude. A work around for Alpha79 is to run it with the prelude.maude from Alpha77. Then fm75-5.maude should work as it did in Alpha77. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha80/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha80/ Alpha release site authentication: User Name: maudeabuser Password: bughunter Bug fixes: (1) A bug in the AU greedy matcher provoked by: fmod AU_GREEDY_BUG is op l : List List -> List [assoc id: nil] . op nil : -> List . sort List Elt . subsort Elt < List . ops a b : -> Elt . var E : Elt . var M N : List . op f : List -> List . eq f(l(E, M, N)) = M . endfm red f(l(a, b)) . (2) A really subtle bug in the AU Boyer-Moore based matcher provoked by: mod AU_META is sort S . op l : S S -> S [assoc] . ops a b c d e : -> S . op g : S -> S . rl [1]: l(g(a), g(X:S)) => e . endm red in META-LEVEL : metaXapply( ['AU_META], 'l['b.S, 'g['a.S], 'g['b.S], 'c.S, 'd.S], '1, none, 0, 0, 0) . red in META-LEVEL : metaXapply( ['AU_META], 'l['b.S, 'g['a.S], 'g['b.S], 'c.S, 'd.S], '1, 'X:S <- 'b.S, 0, 0, 0) . The problem is that since g(X:S) subsumes g(a) so when g(X:S) fails to match something we get a shift of 2. However in the second example g(X:S) fails to match g(a) because X:S is bound, and we cannot assume that the subpattern g(a) will fail on subject g(a) (i.e. a shift of 1). Shifting by 2 causes us to miss the match. The problem is that subsumption doesn't take account of variables being bound by some external agency (the META-LEVEL). The Boyer-Moore based AU matcher is probably overkill... does anyone have real examples with an A/AU pattern where shifting the pattern versus the subject benefits from the Boyer-Moore shift table? Changes ======== (1) The big change is a new term representation along with new matching and renormalization algorithms for the A and AU theories. For some simple patterns, this enables rewrites that would have taken time linear in the size of the subject (using the old greedy matching) to execute in constant time (using the new greedy matching). This can be a big win if the subject has thousands of alien subterms under an A/AU operator. In particular you can now reverse an associative list in linear time using any of the 3 obvious algorithms - see revExample.maude - and remember to "unlimit stacksize". The new representation is only supported for A/AU symbols that: (a) don't have a 1-sided identity; and (b) don't have equations that rewrite at the top. (2) Some optimizations to reduce the number and size of stack frames needed for deep recursions. (3) For my convenience: set print color on . now colors terms appearing in modules by operator theory according to the following scheme (previously only rewritten terms were colored according their reduction status): AC red ACU magenta A green AU, AUl, AUr cyan C, CU, CI CUI blue U, Ur, Ul, I, UI, UrI, UlI yellow iter, free black This color scheme may need to change if more theories are added. (4) At Jose's request: eq f => g = [] (f -> g) . eq f <=> g = [] (f <-> g) . added to model-checker.maude (5) fmod EXT-BOOL added to prelude.maude Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha80a/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha80a/ Alpha release site authentication: User Name: maudeabuser Password: bughunter Bug fixes: =========== (1) A bug where metadata was not copied on importation: fmod METADATA is sort Foo . ops a b : -> Foo . eq a = b [metadata "bar"] . endfm fmod IMPORTER is inc METADATA . endfm show all . red in META-LEVEL : upEqs('IMPORTER, true ) . Changes ======== (1) The AC/ACU theory now uses a simpler, faster version of red-black trees where the size of subtrees are no longer stored in each node. I've eliminated much special case code that no longer gives a performance win. One user visible change is that AC/ACU contexts at the metalevel are no longer flattened. For example: reduce in META-LEVEL : metaXmatch(fmod 'FOO is protecting 'BOOL . sorts 'Foo ; 'Bar . subsort 'Bar < 'Foo . ((op 'f : 'Foo 'Foo -> 'Foo [assoc comm] . op 'c : nil -> 'Foo [none] .) op 'b : nil -> 'Foo [none] .) op 'a : nil -> 'Foo [none] . none none endfm, 'f['X:Foo,'Y:Foo], 'f['a.Foo,'b.Foo,'c.Foo,'c.Foo], nil, 0, s_^100(0), s_^30(0)) . used to produce: rewrites: 1 in 0ms cpu (2ms real) (~ rewrites/second) result MatchPair: { 'X:Foo <- 'b.Foo ; 'Y:Foo <- 'a.Foo,'f['c.Foo,'c.Foo,[]]} but will now produce: rewrites: 1 in 0ms cpu (3ms real) (~ rewrites/second) result MatchPair: { 'X:Foo <- 'b.Foo ; 'Y:Foo <- 'a.Foo,'f['f['c.Foo,'c.Foo],[]]} (2) There is a first implementation of object-message rewriting. The special behaviour is associated with configuration constructors which must be AC and may optionally have an identity. op c : Foo Foo -> Foo [ctor config assoc comm] . Configuration only have their special behavior wrt arguments that have object and message constructors on top. Object and message constructors must have at least one argument: op ob : Bar -> Foo [ctor object]. op m : Bar -> Foo [ctor msg]. An operator can have at most one of the 3 new attributes: config, object and msg. For object constructors, the first argument is considered to be the objects name. For message constructors, the first argument is considered to be the messages target. There may be multiple configuration, object and message constructors. A rule is consider to be an object-message rule if all the following hold: (a) Its lhs has a configuration constructor on top with two arguments A and B (b) A and B are stable (cannot change their top symbol under a substitution). (c) A has a message constructor on top. (d) B has an object constructor on top. (e) The first arguments of A and B are identical. The new behavior appears with the command frewrite and the descent function metaFrewrite(). When the fair traversal attempts to perform a single rewrite on a term headed by a configuration constructor, the following happens: (a) Arguments headed by object constructors are collected. It is a runtime error for more than one object to have the same name. (b) For each object, messages with its name as first argument are collected and placed in a queue. (c) Any remaining argments are placed on a remainder list. (d) For each object, and for each message in its queue, an attempt is made to deliver the message by performing a rewrite with an object-message rule. If all applicable rules fail, the message is placed on the remainder list. If a rule succeeds, the rhs is constructed, reduced, and the result is searched for the object. Any other arguments in the result configuration go onto the remainder list. If the object cannot be found, any messages left in its queue go onto the remainder list. Once its message queue is exhausted, the object itself is placed on the remainder list. (e) A new term is constructed using the configuration constructor on top of the arguments in the remainder list. This is reduced, and a single rewrite using the non-message-object rules is attempted. There is no restriction on object names, other than uniqueness. An object may change its object constructor during the course of a rewrite and delivery of any remaining message will still be attempted. If the configuration constructor changes during the course of a rewrite, the resulting term is considered alien, and does not participate any further in the object-message rewriting for the original term. The order in which objects are considered and messages delivered is system dependent, but note that newly created message are not delivered until some future visit to the configuration (though all arguments including new messages and alien configurations could potentially participate in the single non-message-object rewrite attempt. Message delivery is "just" rather than "fair" - in order for message delivery to be guarenteed, an object must always be willing to accept the message. If multiple object-message rules contain the same message constructor they are tried in a round robin fashion. Non-message-object rules are also tried in a round robin fashion for the single non-message-object rewrite attempt. The counting of object-message rewrites is strange: For the purposes of the rewrite argument given to frewrite, a visit to a configuration that results in one or more rewrites counts as a single rewrite; though for other accounting purposes all rewrites are counted. Finally, for tracing, profiling and breakpoints only, there is a fake rewrite at the top of the configuration in the case that object-message rewriting takes place but the single non-message-object rewrite attempt fails. It is not included in the reported rewrite total, but is inserted to keep tracing consistent. Object-message rewriting is reflected by op config : -> Attr [ctor] . op object : -> Attr [ctor] . op msg : -> Attr [ctor] . in fmod META-MODULE. (3) The nonexec statement attribute is supported. Inadmissable rules, equations and memberships are required to use it. When a statement has the nonexec attribute, it is not used for rewriting. Nonexec rules can be used by metaApply()/metaXapply() and nonexec statements can be upped with the ascent functions. As a temporary backward compatibility hack for FullMaude users, inadmissable rules that don't use nonexec get a warning, but then the nonexec attributed is then added rather than ignoring the rule. The nonexec statement attribute is reflected by op nonexec : -> Attr [ctor] . in fmod META-MODULE. Paco has released Full Maude 80-1 which is compatible with Alpha80/80a and I have put this in the release directory. You should not use an older prelude.maude with Alpha80a since the metalevel hooks have changed. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha80b/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha80b/ Alpha release site authentication: User Name: maudeabuser Password: bughunter This version claims to be Maude 2.0 at startup - this is because unless any show stoppers are reported before I leave for Spain it is what we will release at RTA 2003. Bug fixes: =========== (1) A bug where the bug reporting address was not always printed when Maude crashed. This was caused by the line wrapper being in a bad state - it is now bypassed with a system call. Bug reported by Ambarish. (2) The special hook mechanism no longer crashes if there is a missing sort; but bad hooks is still a good way to corrupt memory. Bug reported by Christiano Braga. Changes: ========= The most important change is that this version is released under the GNU GPL - see the source tree for details - so you may redistribute it. The other major change is that the persistent AC/ACU rewriting now supports conditional rewriting for certain patterns - though this is more of a proof of concept than comprehensive implementation. There are several minor changes: op extending_. : ModuleExpression -> Import [ctor] . is added to fmod META-MODULE. For associative and iterated operators (assoc & iter attributes) the operational semantics of mbs/cmbs is tidied up. It is now an error to have both non-kind declaractions and mbs/cmbs for the same associative or iterated operator but non-kind declaractions can be converted to mbs as long as there is a kind declaractions. So instead of fmod ASSOC-MB1 is sort Foo . op f : Foo Foo -> Foo [assoc comm] . op e : -> [Foo] . ops a b c d : -> Foo . mb f(a, e) : Foo . endfm red f(a, b, e) . red f(a, b, e, a) . red f(e, b, e, a) . red f(a, b, e, e, a) . red f(a, a, b, e, e, a) . write fmod ASSOC-MB2 is sort Foo . op f : [Foo] [Foo] -> [Foo] [assoc comm] . op e : -> [Foo] . ops a b c d : -> Foo . mb f(X:Foo, Y:Foo) : Foo . mb f(a, e) : Foo . endfm red f(a, b, e) . red f(a, b, e, a) . red f(e, b, e, a) . red f(a, b, e, e, a) . red f(a, a, b, e, e, a) . and instead of fmod ITER-MB1 is sort Foo . op f : Foo -> Foo [iter] . op e : -> [Foo] . mb f(e) : Foo . endfm red f(e) . red f(f(e)) . red f(f(f(e))) . write fmod ITER-MB2 is sort Foo . op f : [Foo] -> [Foo] [iter] . op e : -> [Foo] . mb f(X:Foo) : Foo . mb f(e) : Foo . endfm red f(e) . red f(f(e)) . red f(f(f(e))) . For this build I have removed the integrated compiler and MOS oracles - though the code is still in the source tree. These features are not officially part of the release and will not be documented in the manual. I have also removed the Full Maude hack from prelude.maude - the 2.0 release of Full Maude should not need it. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha81/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha81/ Alpha release site authentication: User Name: maudeabuser Password: bughunter This version reports itself as Maude 2.0.1 and will be released as such if no show stoppers are found. Bug fixes: (1) A critical bug in the AC/ACU matcher (reported by Paco) triggered by the following example: fmod AC-BUG is inc NAT . sorts NatSet State . subsort Nat < NatSet . op i : Nat -> Nat . op g : NatSet NatSet -> NatSet [assoc comm] . op f : NatSet NatSet -> State . var X : Nat . vars S T : NatSet . endfm match f(g(X, S), g(i(X), T)) <=? f(g(0, 1), g(g(i(1), i(2), i(3), i(4), i(5), i(6), i(7), i(8)), i(9)) ) . (2) A bug where Maude would go into infinite recursion when a unary operator had empty syntax (reported by "Sylvan S. Pinsky" ): fmod BUG is sorts T A . subsorts T < A . op __ : A A -> A . ops pl(_) +(_) : T -> A . vars g h : A . endfm red h g . Other Changes ============== The big change is that the builld system now uses autoconf/automake for easier porting. There are also many portability fixes. There are ready made binaries for: maude.darwin Darwin (Mac OSX), dynamically linked maude.freeBSD i86 Free BSD, dynamically linked maude.linux i86 Linux, statically linked maude.macLinux Mac Linux, statically linked maude.alpha DEC Alpha OSF, statically linked maude.solaris Sparc Solaris, dynamically linked So far I've failed to make it build on AIX (insufficient memory to link), HPUX (math library issues) and SGI/IRIX (g++/libstdc++ issues). There are now --help and --version command line flags. The internal ordering on Qids is now alphabetical at Manuels request. Previously it was based on the order the underlying identifiers had been seen which caused reproducibility problems for proof scripts. I will be out of town and off line for the next 2 weeks, though I may be able to read email sent to steveneker@att.net (no large files!). Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha82/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha82/ 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 Solaris - I will make a MacOSX binary in the near future. Bug fixes ========== (1) Infinity and -Infinity now work on MacOSX (and FreeBSD) - previously Infinity was converted to 0. Reported by Carolyn. (2) Various bugs in show module (and show all) commands fixed. Reported by Narciso. (3) Break points no longer cause an internal error when executing builtin function symbols. Reported by Christiano Braga. (4) metaPrettyPrint() now handles variables at the kind level correctly. Reported by Joe Hendrix. (5) Printing a sort redeclaration warning from the metalevel no longer causes an internal error. Reported by Peter Olveczky. (6) Various files (ChangeLogs and compiler code) that were accidently left out of the last source tree are included - automake files are fixed. Other changes ============== (1) The semantics over owise equations wrt operator level strategies has changed. Now owise equations can only be used in evaluating the final 0 of a strategy. This change was suggested by Joe Hendrix. (2) The Int operators quo, rem, gcd, lcm, divides now work on Rats. quo gives the number of whole times a rational can be divided by another, rem gives the rational remainder. divides returns true if a rational divides a rational a whole number of times. gcd returns the largest rational that divides into each of its arguments a whole number of times while lcm returns the smallest rational that is an integer multiple of its arguments. (3) Ctor coloring is now supported for iter symbols: set print color on . fmod ITER-COLOR is sorts Nat0 Nat1 Nat2 Nat . subsort Nat0 Nat1 Nat2 < Nat . op s_ : Nat0 -> Nat1 [iter ctor] . op s_ : Nat1 -> Nat2 [iter ctor] . op s_ : Nat2 -> Nat0 [iter] . op 0 : -> Nat0 [ctor] . endfm red s 0 . red s s 0 . red s s s 0 . red s s s s 0 . (4) META-LEVEL has two new polymorpic functions: op upTerm : Universal -> Term [special (...)] . op downTerm : Term Universal -> Universal [special (...)] . upTerm() converts a term into it's meta-representation, while downTerm() converts a meta-term into a regular term. They can handle regular terms at the kind level. The 2nd argument to downTerm is a term belonging to the appropriate component that is returned should the meta-term not represent a valid term in that component. fmod UP-DOWN-TEST is inc META-LEVEL . sort Foo . ops a b c d e : -> Foo . op f : Foo Foo -> Foo . eq c = d . endfm red upTerm(upTerm(f(a, f(b, c)))) . red downTerm(downTerm(upTerm(upTerm(f(a, f(b, c)))), X:Term), a) . (5) The configuration now supports building without Tecla (--with-tecla=no). Requested by Ambarish. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha83/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha83/ 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, Solaris and Darwin. Bug fixes ========== (1) A bug in the meta-context code where iter operators were not properly handled. Reported by Alberto Verdejo, and provoked by the following example: red in META-LEVEL : metaXmatch(mod 'SORTING is protecting 'BOOL . protecting 'STRING . protecting 'NAT . sorts 'Pair ; 'PairSet . subsort 'Pair < 'PairSet . op '<_;_> : 'Nat 'String -> 'Pair [none] . op '__ : 'PairSet 'PairSet -> 'PairSet [assoc comm id('empty.PairSet)] . op 'empty : nil -> 'PairSet [none] . none none rl '__['<_;_>['J:Nat,'X:String],'<_;_>['I:Nat,'Y:String]]=> '__['<_;_>[ 'J:Nat,'Y:String],'<_;_>['I:Nat,'X:String]] [label('switch)] . endm, '__['<_;_>['B:Nat,'C:String],'<_;_>['A:Nat,'D:String]], '__['<_;_>['s_['0.Zero],'"d".Char],'__['<_;_>['s_^2['0.Zero], '"b".Char],'__['<_;_>['s_^3['0.Zero],'"a".Char],'<_;_>['s_^4['0.Zero], '"c".Char]]]], '_and_['_<_['B:Nat,'A:Nat],'_>_['C:String,'D:String]] = 'true.Bool, 0, unbounded, 0) . (2) A bug in the handling of bubbles at the object level where adding an "Exclude" id-hook caused the bubble property to be ignored. Provoked by the following example: fmod BUBBLE-TEST is inc QID-LIST . sort Text . op text : QidList -> Text [special ( id-hook Bubble (1 -1 ( )) id-hook Exclude ( x y z ) op-hook qidSymbol ( : ~> Qid) op-hook qidListSymbol (__ : QidList QidList ~> QidList))] . op f : Text -> Bool . endfm red f( a c b ) . Other changes ============== (1) Polymorphic operators are now declared explicitly by the polymorphic (abbreviates to poly) attribute. This take a set of integers enclosed in parentheses that indicates which arguments are polymorphic; 0 indicates the range. For polymorphic operators that are not constants, at least one argument should be polymorphic to avoid ambiguities. Since there are no polymorphic equations, polymorphic operators are limited to constructors and builtins. Polymorphs are always instantiated with the polymorphic arguments going to the kind level which further limits their generality. The sort name in a polymorphic position is purely a place holder - any legal type name could be used but it seems a useful convention to use "Universal". One reasonable use for polymorphic operators beyond the existing builtins is to define hetrogeneous lists: fmod HET-LIST is inc CONVERSION . sort List . op nil : -> List . op __ : Universal List -> List [ctor poly (1)] . endfm red 4 "foo" 4.5 1/2 nil . The polymorphic attribute is reflected by: op poly : NatList -> Attr [ctor] . (2) The show all and show mod commands now print out the special attribute and its hooks. (3) The set of ascent functions is completed with: op upModule : Qid Bool ~> Module . op upImports : Qid ~> ImportList . op upSorts : Qid Bool ~> SortSet . op upSubsortDecls : Qid Bool ~> SubsortDeclSet . op upOpDecls : Qid Bool ~> OpDeclSet . These work in an analogous fashion to the existing ascent functions. Note that upImports() does not take a Bool since it is not useful to query the imports of a flattened module. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha83a/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha83a/ 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, Solaris and Darwin. Since this version contains a lot of new code and will likely be used as the basis for a 2.1 release at WRLA 2004 I would appreciate people trying to break it. Also the linux version was built on my Mandrake 9.2 home box rather than on my Red Hat 7.3 desktop so I'm hoping it will resolve the tecla/library issue people have been complaining about under newer linux distros. Bug fixes ========== (1) An internal error that occurred when bubbles were imported: fmod FOO is inc QID . sorts Token Foo . op token : Qid -> Token [special(id-hook Bubble (1 1) op-hook qidSymbol ( : ~> Qid))] . op [_] : Token -> Foo . endfm fmod BAR is inc FOO . endfm (2) An nasty memory corruption bug when copying persistent representations of dag nodes. Copying of dags only occurs for non-eager strategies and conditional membership axioms (because cmbs can potentially be applied in lazy subdags) to avoid side effects in shared subdags. Thus this problem only shows up in rare examples such as one by Jose, and the effect of the memory corruption may not be immediately visible even then. (3) An internal error that occurred when a meta-module is incompletely pulled down, and one of the modules it depended on is overwritten: red in META-LEVEL : metaReduce( fmod 'FOO is including 'NAT . sorts 'Foo . none none none X:EquationSet endfm, '0.Nat) . fmod NAT is endfm Other changes ============== The main change is a major overhaul of the module system which now supports simple module expressions formed by summation and renaming. Module expressions can only be used in importation statements. The they have the syntax: ::= | "(" ")" | "+" | "*" := "(" { "," }* ")" := "sort" "to" | "label" "to" | "op" | "op" ":" * "->" := "to" [ "[" + "]" ] + is associative; * binds tighter than + and groups to the left. The only attributes currently allowed are prec, gather and format - the idea is that when you rename an operator, the old syntactic properties may no longer be legal and are reset to defaults unless you explicitly set them with these attributes. Modules are constructed for each subexpression of a module expression and so each signature must be legal. Modules and module expressions are cached both to save time and so that the same module corresponding to a module expression will not be imported twice via a diamond import. Mutually or self recursive imports occurring through module expressions are detected and disallowed. Cached modules generated by module expressions that no longer have any users (if the module(s) containing the module expression have been replaced) are deleted. When a named module A, used in a module expression is replaced, any modules generated for module expressions that (possibly indirectly) depend on A are deleted and any named modules that (possibly indirectly) depend on A are reevaluated if you attempt to use them. Here the notion of "depends on" is transitive through arbitrary nesting of importation and module expressions. Summations are flattened before being evaluated so A + (B + C) creates a single new module A + B + C, which is considered to be an otherwise empty module that includes A, B and C. A summation is an fmod if all the summands are fmods and a mod otherwise. Renaming a module that has imports is a subtle issue. To avoid duplicating imported modules unnecessarily and ending up with a lot of duplicated contents (say many identical copies of BOOL), the module importation structure is maintained throughout the renaming. A module expression A * R evaluates to A if A contains no contents that are affected by R. Otherwise A * R evaluates to a new module A * R' where R' is obtained by deleting those renaming items that don't affect A, and canonizing the types in operator renamings wrt A (see later). If A imports modules B and C, A * R' will import modules found by evaluating B * R' and C * R'. Operators with the poly attribute are only affected by operator renamings that don't specify types. Renaming a module does not change its module type. There are some subtle cases to handle. Consider: fmod A is sort Foo . op a : -> Foo . op f : Foo -> Foo . endfm fmod B is including A . sort Bar . subsort Foo < Bar . op f : Bar -> Bar . endfm fmod C is inc B * (op f : Bar -> Bar to g) . endfm Here the f in A looks as though is isn't affected by the renaming, but because of the subsort declaration in B, it should be renamed for consistency. This is handled is by canonizing the type Bar occurring in the renaming (op f : Bar -> Bar to g) to the kind expression [Foo,Bar] which includes _all_ of the sorts in the kind [Bar] occurring in B. Thus B * (op f : Bar -> Bar to g) evaluates to a new module B * (op f : [Foo,Bar] -> [Foo,Bar] to g) which includes the module expression A * (op f : [Foo,Bar] -> [Foo,Bar] to g) which evaluates to a new module A * (op f : [Foo] -> [Foo] to g) in which f has been renamed. Consider also: fmod A is sorts Foo Bar . endfm fmod B is inc A . op f : Foo -> Foo . endfm fmod C is inc A . subsort Foo < Bar . op f : Bar -> Bar . endfm It is _not_ the case that (B + C) * (op f : Bar -> Bar to g) and (B * (op f : Bar -> Bar to g)) + (C * (op f : Bar -> Bar to g)) evaluate to the same module because in the latter, the f occurring in B will not be renamed. Hence in general * does not distribute over +. Note that this behavior differs from Full Maude where both module expressions evaluate to the same module - which module depends on the order that Full Maude sees the module expressions. Module expressions are reflected in the metalevel through the new META-MODULE declarations: sorts Renaming RenamingSet . subsort Renaming < RenamingSet . op sort_to_ : Qid Qid -> Renaming [ctor] . op op_to_[_] : Qid Qid AttrSet -> Renaming [ctor format (d d d d s d d d)] . op op_:_->_to_[_] : Qid TypeList Type Qid AttrSet -> Renaming [ctor format (d d d d d d d d s d d d)] . op label_to_ : Qid Qid -> Renaming [ctor] . op _,_ : RenamingSet RenamingSet -> RenamingSet [ctor assoc comm prec 43 format (d d ni d)] . op _+_ : ModuleExpression ModuleExpression -> ModuleExpression [ctor assoc comm] . op _*(_) : ModuleExpression RenamingSet -> ModuleExpression [ctor prec 39 format (d d s n++i n--i d)] . in the obvious way. Bashing together of previously unrelated sorts operators and used to be regarded as illegal; however it is now legal and the previous warnings have been downgraded to advisories: fmod FOO is sort Foo . op a : -> Foo . endfm fmod BAR is sort Foo . op a : -> Foo . endfm fmod BAZ is inc FOO + BAR . endfm Note that you get two sets of advisories - one for (FOO + BAR) and one for BAZ. There is a new command show modules . which shows the named and created modules currently in the system. The latter are ephemeral and the garbage collection policy for created modules may change. Operators with the poly attribute may now be ad hoc overloaded (but not subsort polymorphic overloaded). This is not recommended since it can lead to ambiguities for parsing and pretty-printing. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha84/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha84/ Alpha release site authentication: User Name: maudeabuser Password: bughunter This version reports itself as Maude 2.1 and will be released as such if no show stoppers are found between now and next Thursday. This version has binaries for Mac/Linux, HP-Alpha/OSF and x86/Free BSD in addition to the usual platforms. Bug fix ======== A bug in the post syntax error clean up code which freed module expression structures that it should not, resulting in memory corruption, random warnings, and an internal error following a syntax error. Reported by Azadeh Farzan and Carolyn. For example: fmod FOO is protecting NAT . op f : -> Nat Nat . endfm fmod FOO is endfm Other changes ============== This version uses recently released Tecla 1.5.0 which resolves various issues on newer linux versions. Unfortunately I haven't been able to get this Tecla version to build under Panther so the Darwin binary still uses Tecla 1.4.1. The is also to possibility that the Darwin binary may not run under earlier MacOS X versions. There is now a rudimentary test suite in the source tree; use make check to run it after building from source. In order to support automated testing the is a new command line flag -no-banner which suppresses the banner (which will differ between versions making output comparison harder). Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha84b.1/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha84b.1/ Alpha release site authentication: User Name: maudeabuser Password: bughunter This version is a slightly patched version of Alpha84b to fix a critical bug in the AU sort calculation code reported by Jon Haugsand. A simplified version of his example that exposes the problem is fmod SORT-INT is pr INT . sorts Seq Pseq Tree . subsorts Int < Pseq < Seq . op ntree : -> Tree [ctor] . op tree : Tree Int Tree -> Tree [ctor] . op nil : -> Seq . op __ : Seq Seq -> Seq [assoc id: nil ctor] . op __ : Pseq Pseq -> Pseq [assoc id: nil ctor] . vars M N : Int . vars S : Seq . vars F G : Tree . op downto : Nat Nat -> Seq . eq downto(M, N) = if M <= N then downto(M + 1,N) M else nil fi . op itree : Tree Int -> Tree . eq itree(ntree,N) = tree(ntree,N,ntree) . eq itree(tree(F,M,G),N) = if M >= N then tree(itree(F,N),M,G) else tree(F,M,itree(G,N)) fi . op seqtotree : Seq -> Tree . eq seqtotree(N) = tree(ntree,N,ntree) . eq seqtotree(N S) = itree(seqtotree(S),N) . endfm red seqtotree(downto(1,6)) . So far I have had no reports at all about Alpha84b. I would like to know if it breaks Full Maude in anyway. This new version also reports itself as 2.1.1 and I would like to release it as such in the next week or so unless anyone finds a show stopper. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha84b.2/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha84b.2/ Alpha release site authentication: User Name: maudeabuser Password: bughunter This release is a slightly patched version of Alpha84b.1 to fix a critical bug in the operator renaming reported by Paco: fmod FOO is sorts Bar Foo . subsorts Bar < Foo . op foo : Foo -> Foo . op foo : -> Foo . endfm fmod BAZ is inc FOO * (op foo : Bar -> Bar to bar). endfm show all . show modules . This new version also reports itself as 2.1.1 and I would like to release it as such in the next week or so unless anyone finds a show stopper. I will release a snapshot of my development tree (alpha84c) with experimental features in the near future. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha84b/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha84b/ Alpha release site authentication: User Name: maudeabuser Password: bughunter This version reports itself as Maude 2.1.1 and will be released as such if no show stoppers are found in the next week or so. It is intended as bug fix release. Currently there are no Darwin or FreeBSD binaries because of configuration issues on our Darwin and FreeBSD servers - hopefully this will be fixed by next week. Bug fixes ========== (1) A bug where upModule() generated the wrong meta-hooks for special operators of classes ACU_NumberOpSymbol and CUI_NumberOpSymbol. This also shows up with the "show all" command. Reported by Nathalie Sznajder and Paco. (2) A bug whether certain legal label names such as sort could not be parsed in label renamings. (3) The situation where two ad hoc overloaded operators have the same domain kinds but different ranges now causes a warning to be emitted as does the case where the arities differ but might look the same because of associativity: fmod FOO is sorts Foo Bar . op f : Foo -> Foo . op f : Foo -> Bar . endfm fmod BAR is sorts Foo Bar . op f : Foo Foo -> Foo [assoc] . op f : Foo Foo Foo -> Bar . endfm These cases are illegal but are handled correctly at the object level. They always break the metalevel because of ambiguity and this needs to be made clear in the manual. This inconsistancy was reported by Nathalie Sznajder and Olaf Owe. (4) There is now rudimentary checking of the consistancy for bubble hooks since users are expected write these themselves; Thanks to Fabricio Chalub for pointing out that the previous version crashes on (bad) examples from the manual. (5) A bug where an module with a missing identity could be imported, causing an internal error: fmod M is sort S . op __ : S S -> S [assoc id: ] . endfm fmod N is pr M . endfm Reported by Kazuhiro Ogata. Other changes ============== (1) Symmetric with set include FOO on/off . we now have set protect FOO on/off . and set extend FOO on/off . A module may only be auto-imported in one mode. Furthermore the prelude is changed so that BOOL is now auto-protected rather than auto-included. (2) Syntax for theories is supported. Currently this is mostly syntactic sugar except that the rules for importation that we agreed upon in Barcelona are now enforced by warnings and the module type of a summation is correctly calculated. Basically we have a lattice: th / \ fth mod \ / fmod where summation corresponds to join and a module may only import a module of less or equal type. Furthermore theories may only be imported via the including importation mode. Theories are reflected by constructors: fth_is_sorts_.____endfth and th_is_sorts_._____endth The are now extra subsorts: SModule FTheory STheory. Module is now used as the top sort rather than to represent system modules. This choice was made to avoid breaking stuff that expects Module to be the most general sort. The subsort relations are: subsorts FModule < SModule < Module . subsorts FTheory < STheory < Module . op [_] : Qid -> Module . is redefined so that it works with all kinds of modules without producing warnings. (3) The surface parser now supports overparsing - i.e. it deliberately parses more than the legal syntax in order to recover gracefully from common errors. Currently it recognizes rls/crls in fmods/fths, theories and modules terminated with the wrong keyword and the missing space before the period ending a statement. In order to make this possible there are minor restrictions on the legal syntax which should only affect pathological examples: < -> ~> are prohibited as sort names. Tokens ending in a period in the rhs of a eq/rl/mb or the condition of a ceq/crl/cmb cannot be followed by a keyword unless they are inside of parentheses; eg the following is not allowed: eq c = d. eq . It must be rewritten as eq c = (d. eq) . Steven 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= where 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 Dear Maude (ab-)users A new alpha release, ~eker/AlphaRelease62/ is available. For people on this list who don't have a CSL account it's ftp-able from ftp.csl.sri.com in pub/users/eker/MaudeAbusers/alphaRelease62.tar.gz This version has a first approximation to the Maude 2.0 syntax, semantics and metalevel. Some Caveats: ============= Rewrite conditions still are not implemented (though they parse). The new rewrite semantics for unbound variables is not implemented. The compiler does not work in this version. meta-apply/meta-xapply/meta-match/meta-xmatch are not implemented. specials in the meta level are not implemented (those that worked in the old metalevel *might* work since I left this code in). meta-pretty-print has problems with kinds. meta-replace and meta-substitute are not implemented - but they could easily be written in Maude. I have made several changes to Narciso's spec for the Maude 2.0 meta level: (1) the sorts_. constructor is eliminated - the syntax now goes into the mod/fmod construtors. (2) sortInKind and sameComponent have been replaced by the more general sameKind operator. (3) completeName is lifted to types for simplicity. (4) the metalevel is now split into 3 modules for metaterms, metamodules and descent functions. I have only built a version for Linux. Some example reductions in the new metalevel: select META-LEVEL . red meta-reduce( fmod 'FOO is protecting 'MACHINE-INT . sorts none . none op 'fact : 'MachineInt -> 'MachineInt [none] . none eq 'fact['0.MachineInt] = '1.NzMachineInt . ceq 'fact['X:MachineInt] = '_*_['X:MachineInt, 'fact['_-_['X:MachineInt,'1.NzMachineInt]]] if '_>=_['X:MachineInt, '0.MachineInt] = 'true.Bool /\ '_<_['X:MachineInt, '20.MachineInt] = 'true.Bool . endfm, 'fact['21.NzMachineInt]) . red meta-reduce( fmod 'FOO is protecting 'STRING . sorts none . none none none none endfm, '"this is\na string".String) . red meta-reduce( fmod 'FOO is protecting 'FLOAT . sorts none . none none none none endfm, '_+_['1.0.Float,'1.0.Float]) . red completeName( fmod 'FOO is protecting 'BOOL . sorts 'NzNat ; 'Nat ; 'NzInt . subsort 'NzNat < 'Nat . subsort 'NzNat < 'NzInt . none none none endfm, '`[NzInt`]) . red meta-rewrite( mod 'FOO is nil sorts 'Foo . none op 'a : nil -> 'Foo [none] . op 'b : nil -> 'Foo [none] . none none rl ['c]: 'a.Foo => 'b.Foo . rl ['c]: 'b.Foo => 'a.Foo . endm, 'a.Foo, 2) . Steven Dear Maude Abusers, A new alpha release can be downloaded from http://www.csl.sri.com/~eker/Maude/Alpha63a/ Currently only linux is supported. This fixes numerous bugs is the last alpha release caused by the new treatment of conditions, variables and left->right sharing of common subexpressions. The fact that _only_ Mark-Oliver reported these bugs leads me to suspect that noone else tried the last alpha release. Here is a summary of changes (other than bug fixes) from the last alpha release: (1) Various things are renamed as agreed in previous discussions (see prelude.maude). (2) The leastSort function now takes membership axioms into account (I agreed this change of semantics with Jose yesterday). (3) Instead of returning error* for badly formed arguments, the descent functions first try any user equations, and failing that return an unreduced function call at the kind level; for example: select META-LEVEL . red metaReduce( fmod 'FOO is protecting 'MACHINE-INT . sorts 'Foo . none op 'a : nil -> 'Bar [none] . none none endfm, '_+_['1.MachineInt,'12.NzMachineInt]) . (4) metaParse now takes an extra argument of sort Type? which gives the component to which the result should parse; the constant anyType allows any component - the old behavior. In the case that metaParse fails it now returns noParse(n) if there was no parse where n in the index of the first bad token (counting from 0), or the number of tokens in the case of unexpected end of input; or ambiguity(r1, r2) if there were multiple parses, where r1 and r2 are the result pairs correspond to two distinct parses. Examples: red metaParse( fmod 'FOO is protecting 'MACHINE-INT . sorts 'Foo . none op '1 : nil -> 'Foo [none] . none none endfm, '1 '+ '12, anyType) . *** OK red metaParse( fmod 'FOO is protecting 'MACHINE-INT . sorts 'Foo . none op '1 : nil -> 'Foo [none] . none none endfm, '1 '+ '+ '12, anyType) . *** bad token red metaParse( fmod 'FOO is protecting 'MACHINE-INT . sorts 'Foo . none op '1 : nil -> 'Foo [none] . none none endfm, '1 '+ '2 '+, anyType) . *** unexpected end of input red metaParse( fmod 'FOO is protecting 'MACHINE-INT . sorts 'Foo . none op '1 : nil -> 'Foo [none] . none none endfm, '1, anyType) . *** ambiguity red metaParse( fmod 'FOO is protecting 'MACHINE-INT . sorts 'Foo . none op '1 : nil -> 'Foo [none] . none none endfm, '1, 'Foo) . *** OK red metaParse( fmod 'FOO is protecting 'MACHINE-INT . sorts 'Foo . none op '1 : nil -> 'Foo [none] . none none endfm, '1, '`[MachineInt`]) . *** OK Please try this version and remember to report bugs! Steven Dear Maude Abusers, A new alpha release can be accessed at SRI in ~eker/public_html/Maude/Alpha63b/ or downloaded from http://www.csl.sri.com/~eker/Maude/Alpha63b/ Currently only linux is supported. There are 4 changes from Alpha63a: (1) A bug reported by Paco which caused condition fragment trace information to be printed if the interpreter was processing a condition fragment at the instant a ^C interrupt was received is fixed. (2) A bug reported by Paco where an internal error can arise from repeated sequence of (a) rewriting in a module with t1 := t2 type condition fragments and (b) rentering (replacing) the module is fixed. (3) Loop mode now omits spaces around tokens ( , ) { } [ ] The Qids '\( '\, '\) '\{ '\} '\[ '\] provide the old behavior when printed in loop mode. This change was requested by Jose. (4) The module META-TERM now contains the sorts GroundTerm and GroundTermList with appropriate subsorting and operator declarations. This change was requested by Jose. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI in ~eker/public_html/Maude/Alpha63c/ or downloaded from http://www.csl.sri.com/~eker/Maude/Alpha63c/ Currently only linux is supported. The changes from Alpha63b are: (1) Operations op metaReplace : Context Term -> Term . op metaSubstitute : Term Substitution -> Term . removed from fmod META-TERM; these will be part of a library module being written in Maude by Jose. (2) Idempotence axioms added for set constructors: eq A:Assignment ; A:Assignment = A:Assignment . eq S:Sort ; S:Sort = S:Sort . eq S:SubsortDecl S:SubsortDecl = S:SubsortDecl . eq A:Attr A:Attr = A:Attr . eq M:MembAx M:MembAx = M:MembAx . eq E:Equation E:Equation = E:Equation . eq R:Rule R:Rule = R:Rule . (3) Descent functions op wellFormed : Module -> Bool . op wellFormed : Module Term ~> Bool . op getKind : Module Type ~> Kind . op getKinds : Module ~> KindSet . op maximalSorts : Module Kind ~> SortSet . op minimalSorts : Module Kind ~> SortSet . added to fmod META-LEVEL along with new constructor declarations sorts KindSet . subsort Kind < KindSet . op empty : -> KindSet [ctor] . op _&_ : KindSet KindSet -> KindSet [ctor assoc comm id: empty] . eq K:Kind & K:Kind = K:Kind . (4) Sort test meta level constructors op _::_ : GroundTerm Sort -> GroundTerm [ctor] . op _::_ : Term Sort -> Term [ctor] . op _:::_ : GroundTerm Sort -> GroundTerm [ctor] . op _:::_ : Term Sort -> Term [ctor] . are removed. Sort test are now considered to be regular operators with meta names like '_::`MachineInt so the meta term '0.NzMachineInt ::: 'NzMachineInt is now written as '_:::`NzMachineInt['0.NzMachineInt]) This gives a more uniform, easier to process meta-syntax and resolves a problem with sort test operators within contexts. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI in ~eker/public_html/Maude/Alpha63d/ or downloaded from http://www.csl.sri.com/~eker/Maude/Alpha63d/ This is a very minor update to Alpha63c: (1) A bug in the loop mode printing has been fixed so that for example '\`[ prints as [ with spaces around it (whereas '`[ prints as [ without spaces). (2) A bug in the lexical analyser has been fixed so that the character sequences `( and `) occuring in a multiline comment do not count towards balenced paretheses for determining the end of the comment. (3) At Jose's suggestion I have added extra projection functions to fmod META-MODULE in prelude.maude Steven Dear Maude Abusers, A new alpha release can be accessed at SRI in ~eker/public_html/Maude/Alpha63e/ or downloaded from http://www.csl.sri.com/~eker/Maude/Alpha63e/ Currently only linux is supported. The changes from Alpha63d are: (1) The following descent functions are now implemented: op wellFormed : Module Substitution ~> Bool . op metaApply : Module Term Qid Substitution MachineInt ~> ResultTriple? . op metaXapply : Module Term Qid Substitution MachineInt MachineInt MachineInt ~> Result4Tuple? . They support caching in the case that multiple solutions are extracted in order. There are some subtle issues that arise if the interpreter is ^C interrupted midway through a metaApply and the metamodule it is working on is invalidated by changing a module in the database that it depends on. (2) Operators whose sort structure allows a collapse from the kind level to an "output-sort" no longer generate a warning. Back in Feb 97 (accoding to my ChangeLog) we made a decision that collapsing from an error sort to an non-output-sort (i.e. a sort that the operator could not produce) was OK because this trivially happens when new sorts are added above in the component. I have been unable to reconstruct the justification for making a distinction between the non-output-sort case and the output-sort case and since we now allow rewriting at the kind level I cannot think of anything that might break. Incidently there was a bug in the output-sort computation loop that could cause memory corruption if the two argument components differed (as they can with a one sided identity). (3) Several memory leaks plugged. (4) A serious bug in the compilation of conditional collapse rules, provoked by an example such as: mod FOO is sort Foo . op a : -> Foo . op b : -> Foo . op f : Foo Foo -> Foo [comm] . crl [k] : f(Y:Foo, Y:Foo) => Y:Foo if Y:Foo =/= a . endm rew f(b, b) . has been fixed. There are still several things in the metalevel that remain to be implemented - the metaMatch/metaXmatch operators and some of the specials in metamodules. I've slightly modified an old example to demonstrate metaXapply: fmod ALL-ONE-STEP-REWRITES is including META-LEVEL . sort TermSet . subsort Term < TermSet . op _|_ : TermSet TermSet -> TermSet [assoc comm id: mt ctor] . op mt : -> TermSet [ctor] . var T : Term . var M : Module . var L : Qid . var N : MachineInt . op findAllRews : Module Term Qid -> TermSet . op findAllRewsAux : Module Term Qid MachineInt -> TermSet . eq findAllRews(M, T, L) = findAllRewsAux(M, T, L, 0) . eq findAllRewsAux(M, T, L, N) = if metaXapply(M, T, L, none, 0, maxMachineInt, N) :: Result4Tuple then (getTerm(metaXapply(M, T, L, none, 0, maxMachineInt, N)) | findAllRewsAux(M, T, L, N + 1)) else mt fi . endfm red findAllRews(mod 'FOO is protecting 'BOOL . sorts 'Foo ; 'Bar . subsort 'Bar < 'Foo . op 'a : nil -> 'Foo [none] . op 'b : nil -> 'Foo [none] . op 'c : nil -> 'Foo [none] . op 'f : 'Foo 'Foo -> 'Foo [assoc comm] . none none rl ['k] : 'f['X:Foo, 'Y:Foo] => 'X:Foo . rl ['k] : 'a.Foo => 'c.Foo . endm, 'f['a.Foo, 'b.Foo], 'k) . Steven Dear Maude Abusers, A new alpha release can be accessed at SRI in ~eker/public_html/Maude/Alpha64/ or downloaded from http://www.csl.sri.com/~eker/Maude/Alpha64/ Currently only linux and solaris are supported. The changes from Alpha63e are: (1) The special/hook mechanism has been reimplemented in what should be a more extensible way. All hooks now work at the metalevel and hook names have changed. In particular qidSymbol must be used rather than qidBaseSymbol in bubbles. (2) metaMatch and metaXmatch implemented (3) The garbage collector mark phase has been reimplemented to use less stack space for very deep terms in cases where the previous tail recursive approach failed (typically lists where the list constructor has an identity but no other attributes). (4) getName and getType are now implemented via maude strings rather than being builtin. (5) [_] : Qid -> Module implemented in maude. (6) Identity clashes detected. (7) match/xmatch commands now use the same code as metaMatch and metaXmatch and handle ^C interrupts more cleanly There are also various bug fixes: (1) No longer crashes if user tries to make a sort test at the meta level without defining SystemTrue and SystemFalse. (2) Fixed bug in op wellFormed : Module Substitution ~> Bool . that could cause memory corruption. (3) Fixed memory leaks in metaApply and metaXapply. (4) Output buffer is now flushed before reading input, even if output is not going to a tty. (5) Fixed bug in the statement importation code that leaves the imported module in a bad state and which causes importation to fail if the statements of a module are imported twice in succession without any intervening signature importation (which would return the imported module to a good state) from that module. (6) .*** and .--- are no longer considered to be the end of a command followed by a comment when encountered in a command, outside of parentheses. (7) Fixed wrap-around bug for string built-ins that was provoked by using very large numbers (typically maxMachineInt) to stand in for infinity or "end of string". Steven Various examples: red in META-LEVEL : metaReduce( fmod 'FOO is including 'BOOL . sorts 'MI . none op 'mi : nil -> 'MI [special(id-hook('MachineIntegerSymbol, nil))] . op '< : 'MI 'MI -> 'MI [special(id-hook('MachineIntegerOpSymbol, '<) op-hook('machineIntegerSymbol, 'mi, nil, 'MI) term-hook('trueTerm, 'true.Bool) term-hook('falseTerm, 'false.Bool))] . none none endfm, '<['9.MI, '10.MI]) . red in META-LEVEL : metaParse( fmod 'FOO is including 'QID-LIST . sorts 'Token ; 'Foo . none op 'tokens : 'Qid -> 'Token [special(id-hook('Bubble, '0 '10) op-hook('qidSymbol, ', nil, 'Qid) op-hook('nilQidListSymbol, 'nil, nil, 'QidList) op-hook('qidListSymbol, '__, 'QidList 'QidList, 'QidList) id-hook('Exclude, 'assoc 'com 'memo))] . op '`[_`] : 'Token -> 'Foo [none] . none none endfm, '`[ 'a 'b 'c '`] , anyType) . red in META-LEVEL : metaReduce( fmod 'FOO is nil sorts 'Foo ; 'Bool . none op 'true : nil -> 'Bool [special(id-hook('SystemTrue, nil))] . op 'false : nil -> 'Bool [special(id-hook('SystemFalse, nil))] . op 'a : nil -> 'Foo [none] . none none endfm, '_::`Foo['a.Foo]) . red in META-LEVEL : metaReduce( fmod 'FOO is nil sorts 'Foo ; 'Bool . none op 'itef : 'Bool 'Universal 'Universal -> 'Universal [special(id-hook('BranchSymbol, nil) term-hook('trueTerm, 'true.Bool) term-hook('falseTerm, 'false.Bool))] . op 'true : nil -> 'Bool [none] . op 'false : nil -> 'Bool [none] . op 'a : nil -> 'Foo [none] . op 'b : nil -> 'Foo [none] . none none endfm, 'itef['false.Bool, 'a.Foo, 'b.Foo]) . red in META-LEVEL : metaReduce( fmod 'FOO is nil sorts 'Foo ; 'Bit . none op '= : 'Universal 'Universal -> 'Bit [special(id-hook('EqualitySymbol, nil) term-hook('equalTerm, '1.Bit) term-hook('notEqualTerm, '0.Bit))] . op '1 : nil -> 'Bit [none] . op '0 : nil -> 'Bit [none] . op 'a : nil -> 'Foo [none] . op 'b : nil -> 'Foo [none] . none none endfm, '=['a.Foo, 'b.Foo]) . red in META-LEVEL : metaMatch(fmod 'FOO is protecting 'BOOL . sorts 'Foo ; 'Bar . subsort 'Bar < 'Foo . op 'a : nil -> 'Foo [none] . op 'b : nil -> 'Foo [none] . op 'f : 'Foo 'Foo -> 'Foo [comm] . none none endfm, 'f['X:Foo, 'Y:Foo], 'f['a.Foo, 'b.Foo], 1) . red in META-LEVEL : metaXmatch( fmod 'FOO is protecting 'BOOL . sorts 'Foo ; 'Bar . subsort 'Bar < 'Foo . op 'a : nil -> 'Foo [none] . op 'b : nil -> 'Foo [none] . op 'c : nil -> 'Foo [none] . op 'f : 'Foo 'Foo -> 'Foo [assoc comm] . none none endfm, 'f['X:Foo, 'Y:Foo], 'f['a.Foo, 'b.Foo, 'c.Foo, 'c.Foo], 0, 100, 0) . Dear Maude Abusers, A new alpha release can be accessed at SRI in ~eker/public_html/Maude/Alpha65/ or downloaded from http://www.csl.sri.com/~eker/Maude/Alpha65/ Currently only linux and solaris are supported. The changes from Alpha64 are: (1) There is a new attribute "frozen" that prevents an operators arguments from being rewritten by rules. Note that using this attribute effectively changes the denotational as well as the operational semantics of the frozen operator by disallowing the congruence proof rule for rl/crls. This is an extension of rewriting logic recently suggested by Jose. The frozen attribute is reflected by op frozen : -> Attr [ctor] . and is supported by all commands and descent functions that use rules. (2) There is a new command set show breakdown on/off . that causes a breakdown of mb applications, equational rewrites and rule rewrites to be printed after the "rewrites:" line but before the "result" line. mb applications are now counted in the main rewrite total. (3) The is a new command line flag "-interactive" that causes Maude to treat stdin/stdout/stderr as a tty and generate prompts even if isatty() returns false. This may be useful if Maude is being controlled by another process via pipes/fifos etc. (4) There is a new command for "position fair" rule rewriting; it has 3 forms: frewrite [nrRewrites, rewritesPerPosition] term . frewrite [nrRewrites] term . frewrite term . frew is an abbreviation for frewrite; the "debug" and "in :" modifiers are supported as they are for rewrite. Unlike rewrite which uses a leftmost outermost strategy for applying rules and reduces the whole term with equations after each succcessful rule rewrite, frewrite attempts to be position fair by making a number of depth first traversals of the term, and on each traversal, each position that existed at the start of the traversal is entitled to at most rewritesPerPosition rule rewrites when its turn comes around. After a rule rewrite succeeds, only the subterm that was rewritten is reduced with equations in order to avoid destroying positions that haven't yet had their turn for the current traversal. Traversals are made until nrRewrites rule rewrites have been made or until no more rewrites are possible. In the 2nd and 3rd forms, rewritesPerPosition defaults to 1. In the 3rd form nrRewrites defaults to infinity. The continue command works with frewrite in the same ways as it works with rewrite. In particular, considerable extra information about the current traversal is saved by the frewrite so that frewrite [n, k] t . continue m . produces the same final answer as frewrite [s, k] t . if s = n + m. The are a couple of caveats with frewrite: (a) If position fair rewriting stops mid traversal (typically the case with the 1st and 2nd forms) then the sort of the (incompletely reduced) result has not been calculated and is printed as "(sort not calculated)". (b) Position fair rewriting is not substitution fair; this is particularly apparent if you have an AC soup of messages and objects. Fair rewriting is reflected by op metaFrewrite : Module Term MachineInt MachineInt ~> ResultPair which is the meta equivalent of the first form of frewrite except that a final (semantic) sort calculation is performed at the end in order to produce a correct ResultPair. (5) Greedy matching is used for rules in situations (currently rewrite/metaRewrite and frewrite/metaFrewrite with non-conditional rules) where only a single matching substitution is required. With A/AC/ACU etc operators this may result in different substitutions being chosen and improved matching speed. (6) rewrite, continue and now frewrite take 64bit rather than 32bit integers. There are also various bug fixes: (1) abort works properly within the rewrite command in some cases where it used to run out of memory or crash. (2) rewrite/metaRewrite (and now frewrite/metaFrewrite) reset the round robin pointers in the rule tables to give reproducible (i.e. functional) results. (3) multiple files specified on the command line are now read in correctly; previously the 2nd and subsequent files would be read in after hitting eofs, even if the eof in question was not from the previous command line file but a file imported by a previous command line file. Steven Various examples: fmod FAIR is pr MACHINE-INT . sort Foo . op i : MachineInt -> Foo . op j : Foo -> Foo [frozen] . op f : Foo Foo -> Foo . var M : NzMachineInt . var X : Foo . rl i(M) => i(M - 1) . rl f(X, i(0)) => X . endfm set trace on . set trace whole on . frew f(f(i(2), i(1)), f(j(i(3)), i(2))) . rew f(f(i(2), i(1)), f(j(i(3)), i(2))) . set trace off . frew [1, 1] f(f(i(2), i(1)), f(j(i(3)), i(2))) . cont 3 . fmod ALL-ONE-STEP-REWRITES is including META-LEVEL . sort TermSet . subsort Term < TermSet . op _|_ : TermSet TermSet -> TermSet [assoc comm id: mt ctor] . op mt : -> TermSet [ctor] . var T : Term . var M : Module . var L : Qid . var N : MachineInt . op findAllRews : Module Term Qid -> TermSet . op findAllRewsAux : Module Term Qid MachineInt -> TermSet . eq findAllRews(M, T, L) = findAllRewsAux(M, T, L, 0) . eq findAllRewsAux(M, T, L, N) = if metaXapply(M, T, L, none, 0, maxMachineInt, N) :: Result4Tuple then (getTerm(metaXapply(M, T, L, none, 0, maxMachineInt, N)) | findAllRewsAux(M, T, L, N + 1)) else mt fi . endfm set show breakdown on . red findAllRews(mod 'FOO is protecting 'BOOL . sorts 'Foo ; 'Bar . subsort 'Bar < 'Foo . op 'a : nil -> 'Foo [none] . op 'b : nil -> 'Foo [none] . op 'c : nil -> 'Foo [none] . op 'f : 'Foo 'Foo -> 'Foo [assoc comm] . op 'g : 'Foo -> 'Foo [none] . none none rl ['k] : 'f['X:Foo, 'Y:Foo] => 'X:Foo . rl ['k] : 'a.Foo => 'c.Foo . endm, 'f['a.Foo, 'g['a.Foo]], 'k) . red findAllRews(mod 'FOO is protecting 'BOOL . sorts 'Foo ; 'Bar . subsort 'Bar < 'Foo . op 'a : nil -> 'Foo [none] . op 'b : nil -> 'Foo [none] . op 'c : nil -> 'Foo [none] . op 'f : 'Foo 'Foo -> 'Foo [assoc comm] . op 'g : 'Foo -> 'Foo [frozen] . none none rl ['k] : 'f['X:Foo, 'Y:Foo] => 'X:Foo . rl ['k] : 'a.Foo => 'c.Foo . endm, 'f['a.Foo, 'g['a.Foo]], 'k) . fmod TEST is pr META-LEVEL . op m : -> Module . eq m = (mod 'FAIR is protecting 'MACHINE-INT . sorts 'Foo . none op 'i : 'MachineInt -> 'Foo [none] . op 'f : 'Foo 'Foo -> 'Foo [none] . none none rl ['k] : 'i['M:NzMachineInt] => 'i['_-_['M:NzMachineInt, '1.NzMachineInt]] . rl ['k] : 'f['X:Foo, 'i['0.MachineInt]] => 'X:Foo . endm) . op t : -> Term . eq t = 'f['f['i['2.NzMachineInt], 'i['1.NzMachineInt]], 'f['i['3.NzMachineInt], 'i['2.NzMachineInt]]] . endfm red metaFrewrite(m, t, 1, 1) . red metaFrewrite(m, t, 2, 1) . red metaFrewrite(m, t, 3, 1) . red metaFrewrite(m, t, 4, 1) . red metaFrewrite(m, t, 5, 1) . red metaFrewrite(m, t, 6, 1) . red metaFrewrite(m, t, 7, 1) . red metaFrewrite(m, t, 8, 1) . red metaFrewrite(m, t, 9, 1) . red metaFrewrite(m, t, 10, 1) . red metaFrewrite(m, t, 11, 1) . red metaFrewrite(m, t, 0, 1) . set show breakdown off . Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in ~eker/public_html/Maude/Alpha66/ or downloaded from http://www.csl.sri.com/~eker/Maude/Alpha66/ Currently only linux and solaris are supported. Since there are new people on my "Maude Abusers" list I have put the release notes for previous versions in http://www.csl.sri.com/~eker/Maude/ReleaseNotes The changes from Alpha65 are: (1) Break symbol facility - select and deselect break symbols with: break select foo bar baz . break deselect quux . The break facility is switched on and off with set break on/off . When it is on, executing a mb/eq/rl with a break symbol on top will put you in the debugger. (2) match/xmatch commands reimplemented. They may now have a condition introduced by "such that" or equivalently "s.t."; for example match [2] in FOO : X * (Y + Z) <=? (a + b) * (a + d) s.t. A:Nat + B:Nat := X /\ A:Nat = Y . Also you can continue to look for more solutions with cont 4 . for example. Parsing is also a little smart in that the fact that both sides of <=? must be in the same component is taken in to account when resolving ambiguities. (3) search command reimplemented. The new syntax is search [<# solutions>] in : such that . The "[<# solutions>]", "in :" and "such that " parts are optional. "s.t." is an abbreviation for "such that". Possible relations are: => rewrites in exactly 1 step =>* rewrites in 0 or more steps =>+ rewrites in 1 or more steps =>! rewrites to normal form (i.e. a term in which no further rewrites are possible) For example: search [1] a * d + b * d + c * d + a * e + b * e + c * e =>+ X * Y such that W + Z := X . You can look for more solutions with the cont command as above. You may also interrupt a search in progress with ^C. In this case one of two things will happen dependeing on what Maude is doing at the instant you hit ^C. If Maude is not doing a rewrite, the command will exit. If maude is doing a rewrite you will end up in the debugger. In this latter case it is probably best to "abort ." since the debugger has no special support for search at the moment. When a search command terminates; either because there was a finite state graph and hence it can be determined there was no more solutions or because you used the "[<# solutions>]" part to limit the number of solutions found, the state graph is retained in memory until you switch modules or run another command the preforms rewriting. You can interrogate the state graph with the command: show path . which will show the sequence of states and rules going from the start term to the chosen state. Since the search command does a breadfirst search this will be a shortest path. (4) Timing reimplemented. Now if you do set timing off . set loop timing off . no calls to the system calls setitimer() or getitimer() will be made. This should enable the linux version of Maude to run under MS Windows using LINE (http://line.sourceforge.net/). Also the linux version should no longer report negative times. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in ~eker/public_html/Maude/Alpha67/ or downloaded from http://www.csl.sri.com/~eker/Maude/Alpha67/ This release has just 3 minor changes from Alpha66 that have been requested by various `hardcore' Maude users: (1) [requested by Merrill & Kemal] It is now possible to print out the current search graph generated by the search command with the command: show search graph . This command may be used whether or not the search is complete (in the case you have given a bound on the number of solutions); naturally only the portion of the graph actually constructed can be output. The format is a sequence of states, each with 0 or more arcs that look like: state , : arc ===> state () ... () : arc ===> state () ... () State numbers start at 0. Arc numbers for each state start at 0. If it is possible to reach the same next state via multiple rules, this is treated as a single arc with a list of rules. If it is possible to reach the same next state via the same rule with multiple substitutions, this is not explicitly represented (since we are not outputting substitutions). This feature is the main reason for the release. (2) [requested by Carolyn] The trace select facility now also recognizes rule labels rather than just top symbols; so if you keep your rule labels disjoint from your operator names you can selectively trace rules via their label. The recent break select facility now also works in the same way for consistancy. (3) [requested by Jose] If you `in' a file that does not end in a newline, Maude will fake a newline. This allows a command at the end of such a file to be recongnized as such (the `.' at the end of a command must be followed by a newline in order to be recognized as the end of a command rather than as user syntax). Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in ~eker/public_html/Maude/Alpha68/ or downloaded from http://www.csl.sri.com/~eker/Maude/Alpha68/ This release has just one change from Alpha67: the incorporation of an LTL model checker for a finite fragment of rewriting logic. To use the model checker you must load the file model-checker.maude You might also want the file dekker.maude that gives a slightly more realistic example of how to use the model checker. The syntax of LTL formula is given in the LTL module. The available operators are: True true False false ~ f not f /\ g and f \/ g or f -> g implies f <-> g iff @ f next (f holds in the next state) [] f always (f holds now and in all future states) <> f eventually (eventually we will reach a state where f holds) f U g strong until (f holds in all states until the first state where g holds and g will eventually hold) f W g weak until (f holds in all states until the first state where g holds but g need not eventually hold) f R g release (g holds now and in all states upto and including the first state in which f holds but f need not eventually hold) The elementary propositions are just terms (often constants) of sort Prop whose semantics are given by the user. Here's an example: mod TEST is inc MODEL-CHECKER . ops s t : -> State . rl s => t . rl t => s . ops a b : -> Prop . eq s |= a = true . eq t |= b = true . endm Here we have a trivial system with just 2 states, s and t, such that s always goes to t and t always goes to s. There are just two propositions, a and b. a is only true in s and b is only true in t. The semantics of propositions are defined by writing equations of the form eq |= = . where evaluates to true when the proposition matching holds in the state matching . It is only necessary to define the true case, anything else is assumed to be false. Note that since propositions can be arbitrary ground terms we can define parameterized families of propositions with a single equation (see the Dekker algorithm example). To check if a given LTL formula holds in the state transition graph from a given starting state we do a reduction: red |= . For example: red s |= [] <> a . *** a holds infinitely often - true red s |= [] <> b . *** b holds infinitely often - true red s |= [] a . *** a always holds - false red s |= [] (a \/ b) . *** (a or b) always holds - true When the formula is false, a counterexample is produced rather than false. A counterexample is an infinite sequence of states that can be generated in the system and which violates the checked property. A counterexample is presented as a pair of finite lists of states. The second list is a infinite cycle; the first list is a sequence that starts from the start state and reaches the first state of the cycle. Counterexamples are returned as terms using the constructors: op nil : -> StateList [ctor] . op __ : StateList StateList -> StateList [ctor assoc id: nil] . op counterExample : StateList StateList -> Result [ctor] . Here's a slightly more complex example: mod TEST2 is inc MODEL-CHECKER . ops a b : -> Prop . ops s t u v : -> State . rl s => t . rl s => u . rl u => v . rl v => s . rl t => s . rl t => t . eq s |= a = true . eq t |= b = true . endm red s |= <>[] b . *** eventually we reach a state where b *** holds forever - false red s |= []<> a . *** a holds infinitely often - false red s |= <>[] b \/ []<> a . *** one or other of the two previous *** formulae holds - true There are a couple of caveats: (1) The set of reachable states must be finite (otherwise the model check may not halt). (2) LTL formula apply to infinite traces; finite traces (i.e. deadlocks) are a problem. This is dealt with by adding self loops to deadlocked states. There is a module LTL-SIMPLIFIER that can optionally be included along with MODEL-CHECKER; it attempts to rearrange and simplify LTL formulae in order to produce smaller Buchi automata. Known problems: =============== (1) The rewrites used to compute transitions in the state graph are not counted. (2) The model checker responds badly to ^C interrupts. (3) Model checking cannot be traced in a useful way. (4) Counterexamples only list states and not labels, rules, or substitutions; already this looks rather ugly so it's not clear just what is the best format for counter-examples. (5) Buchi automaton generation is highly suboptimal (though better than many existing Buchi automaton-based LTL model checkers). This translates to more space/time usage and longer counter-examples than strictly necessary. (6) No self test for Buchi automaton generation; this is the area where unsoundedness is most likely to arise in a Buchi automaton-based LTL model checker. Design Issues ============= There are a number of UI issues with the model checker and Maude in general on which I would like input from Maude users. (1) To what extent should stuff be put in the prelude (e.g. strings) as opposed to in a library file (e.g. this version of the model checker)? (2) Is it the right thing that model checking is done by special reduce semantics for the _|=_ as opposed to special rewrite semantics for this symbol or a special command (like search)? (3) Should counterexamples be returned as terms (can be processed by user code, but ugly) or arbitrary print out (as a side effect but might be more readable)? (4) Would search be better if it were implemented by a special operator that return it's result as a term rather than as a command which prints it's result on the screen? Or should we have a metaSearch operator which works with meta-terms? (5) What info should go into each step of a counterexample? (6) Would it be useful to have a verbose mode where stuff is printed as the model check proceeds? what stuff would be useful? Some possibilities: (a) # states in very weak alternating automaton. (b) # states & # acceptance sets in generalized Buchi automaton. (c) # states and # accepting states in standard Buchi automaton. (d) # states explore in state transition graph. Could also wrap this stuff into the result term. Steven 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 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 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 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: I have yet to attempt a DTD for maudeml however the current implementation assumes a fragment something like: 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 Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in ~eker/public_html/Maude/Alpha71a/ or downloaded from http://www.csl.sri.com/~eker/Maude/Alpha71a/ Bug fixes: 1 A really nasty bug deep within the AU greedy matcher where a matching function that can return true/false/UNDECIDED was declared as returning bool - with the effect that when it failed as UNDECIDED (no match found, but match might exist) the rest of the AU greedy matcher saw this as a success. This results in unbound variables, missing matching subproblems and general anarchy. It is provoked by a really pathological example from Dilia which contains a pattern simple enough to trick the system into building a AU greedy matching automaton for it but complex enough to be able to fail with UNDECIDED on certain subjects. 2 A wrap around bug where highly ambiguous (billions of parses) terms/statements/commands causes MSCP10 to return a -ve number of parses which was handled ungracefully by the rest of the system - the fix is to treat -ve number of parses as equal to 2. This was provoked by a slight modification to Dilia's example. Incidentally Dilia's example also has 89 user sorts in a single connected component and exposes a performance problem with associative sort checking for which I don't have a fix at the moment - the naive n^3 algorithm is noticeably slow for n=89. 3 A bug in the metalevel parser provoked by the following example of Paco; run right after startup: red in META-LEVEL : metaParse(fmod 'FOO is nil sorts 'Foo . none op 'f : nil -> 'Foo [none] . none none endfm, 'f, 'Foo) . New features: 1 There are several changes to the XML support at Carolyn's request: (a) The XML output stream is flushed after every 2nd level closing tag. (b) XML output is now implemented for the following additiona commands: show search path . search { if } . (c) Each command that produces XML output will also produce an XML echo of that command if set show command on . which is the default. 2 A first version of profiling is implemented. Profiling is turn on and off by set profile on/off . When profiling is switched on, a count is kept of the number of executions of each mb/eq/rl. This can be displayed by show profile { } . The profile information is assciated with each module and is usually cleared at the start of any command that can do rewrites except continue. This behaviour can be changed with set clear profile on/off . For unconditional statements, the profile information is just the number of rewrites using that statement. For conditional statements there is also the number of matches since not every match leads to a rewrite due to condition failure. Also when searching, there can be multiple rewrites for each match since the condition may be solved in multiple ways. Also, there is a table that for each condition fragment gives (a) the number of times the fragment was initially tested (b) the number of times the fragment was test due to backtracking (c) the number of times the fragment succeeded (d) the number of times the fragment failed Normally (a) + (b) = (c) + (d). Special rewrites such as built-in rewrites and memoized rewrites are also tracked, but as these are associated with symbols rather than statements. For conciseness, symbols with no special rewrites, and statements that are not matched are omitted. Like tracing and break symbols/labels, switching profiling on substantially reduces performance. There are some limitations; metalevel rewrites are not displayed due to the ephemeral nature of metamodules. Also condition fragments associated with a match or search command are not tracked (though any rewrites initiated by such a fragment are). If you turn profiling on or off in the debugger you may get inconsistant results. 3 At Carolyn's request the metalevel now has "ascent" functions for uping stuff from the module database: op upMbs : Qid Bool ~> MembAxSet . op upEqs : Qid Bool ~> EquationSet . op upRls : Qid Bool ~> RuleSet . The first argument is the name of a module in the database. The second argument is true if imported statements are to be including. A module may examine itself: mod INTROSPECTION is inc META-LEVEL . op rules : -> RuleSet . rl rules => upRls('INTROSPECTION, false) . endm rew rules . mod SELF-REFLECTION is inc INTROSPECTION . op allRules : -> RuleSet . rl allRules => upRls('SELF-REFLECTION, true) . op myRules : -> RuleSet . rl myRules => upRls('SELF-REFLECTION, false) . endm rew myRules . rew allRules . 4 Loop mode now recognizes several special Qids in addition to '\t and '\n : '\s (forced) space '\r red '\g green '\y yellow '\b blue '\m magenta '\c cyan '\u underline '\! bold '\o revert to original color and style 5 The format attribute is now supported at the metalevel: op format : QidList -> Attr [ctor] . metaPrettyPrint() uses the above special Qids to approximate how the object level pretty-printer handles formatting instructions. Also I have changed the way Maude searches for files slightly: For prelude.maude it now checks: (a) the directories in the MAUDE_LIB environment variable (b) the directory containing the executable (c) the current directory For files specified by a bare file name, it checks (with .maude, .fm, .obj extensions if the filename does have one of these extensions): (a) the current directory (b) the directories in the MAUDE_LIB environment variable (c) the directory containing the executable In both cases (c) is an addition to the previous behaviour. Since some users just put library files such as model-checker.maude (there will be others in the near future) in the same directory as the executable rather than setting MAUDE_LIB this should enable Maude to find such files, e.g. with load model-checker Of course sticking configuration & library files in a bin directory is frowned upon. Also this might help with finding the prelude under windoze where the executable finding code breaks. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in ~eker/public_html/Maude/Alpha73/ or downloaded from http://www.csl.sri.com/~eker/Maude/Alpha73/ Running this new version is complicated by the fact it uses dynamic libraries, (gmp 4.1 and its C++ bindings) that will not be installed on most machines. Thus you may need to install them by one of these methods: (1) Obtain the source code from http://www.swox.com/gmp/ Configure with --enable-cxx for C++ support. Compile it with g++ 2.95.3 (because the C++ ABI changes with every compiler release you need the same g++ as I used to compile Maude). Install the two shared objects produced some place where your dynamic linker can find them. If you cannot write to system library directories and your sysadmins won't install them for you, you can always place them in ~/lib and point the LD_LIBRARY_PATH environment variable at this directory. (2) If this fails, you can get the shared objects I use from http://www.csl.sri.com/~eker/Maude/Lib/Linux/ or http://www.csl.sri.com/~eker/Maude/Lib/Solaris/ as appropriate and put them in ~/lib Then make the symbolic links and set LD_LIBRARY_PATH ln -s ~/lib/libgmp.so.3.3.0 ~/lib/libgmp.so.3 ln -s ~/lib/libgmpxx.so.3.0.2 ~/lib/libgmpxx.so.3 setenv LD_LIBRARY_PATH ~/lib Note also the the linux version is now dynamically linked whereas previous versions were statically linked and in particular you will need the libstdc++.so.3 that comes with g++ 2.95.3. If you run into linking problems you can use the ldd command to see what shared objects are needed. BTW I will be offline from Sat June 22 thru Sun July 7 so if you are going to try this new version I suggest install it before noon PST friday in case you need email support. Bug fixes: 1 A bug in sortLeq which caused unpredictable behavior when the two sorts were in different kinds - reported by Carolyn. 2 A bug which caused a incomplete module terminated by ctrl-D to not be discarded, causing unpredictable behavior - reported by Carolyn. 3 A bug where memoized rewrites were not counted - reported by Carolyn. Minor changes: 1 show all . and show ops . now display format attributes; further more generated gather info is only displayed if the op has arguments. 2 show all . now puts multiple subsorts in a single subsort declaration where possible. There are a number of major changes in this version, the last two of which will break most existing Maude code, however the existing model-checker.maude can be used unmodified. The iter theory =============== Unary operators may be declared to belong to the iter (short for iterated function symbol) theory. op f : Foo -> Foo [iter] . The sole purpose of this theory is to permit the efficient i/o and manipulation of very large stacks of functions symbols. The term f(f(f(X:Foo))) can be input as f^3(X:Foo) and will be output in that form. A term such as f^1234567890123456789(X:Foo) is too large to be input, output or manipulated is regular notation but can be input and output in this compact notation and certain (built in) manipulations may be efficient. The precise form the of compact iter theory notation is the prefix name of the operator followed by: ^[1-9][0-9]* (in lex regular expression notation) without no intervening white space. Note that f^0123(X:Foo) is not acceptable. Of course regular notation (and mixfix notation if appropriate) can still be used. Sort computations using subsort polymorphism are efficient: subsorts Odd Even < Foo . op f : Odd -> Even [ditto] . op f : Even -> Odd [ditto] . red f^1234567890123456789(X:Odd) . Membership axioms headed by iter operators are neither efficient nor correct (the same is true of assoc operators since we started allowing declarations at the kind level). Correctness may eventually be fixable, efficiency will not be. The situation with matching and rewriting is analogeous to the assoc theory - proper subterms of s^3(X:Foo), such as s^2(X:Foo) and s(X:Foo) can be matched and rewritten by means of extension. However for the pupose of calculating term depth, if the top level is 0, X:Foo is at level 1, not level 3. Fair rewriting treats a whole stack of iter operartors as a single position for the purposes of position fairness (again this is analogeous to the assoc case). The iter attribute is reflected by op iter : -> Attr [ctor] . A term such as f^1234567890123456789(X:Odd) is metarepresented as 'f^1234567890123456789['X:odd] metaParse() understands the compact iter theory notation and metaPrettyPrint() uses it. A version of the notation is also supported by the -xml-log command line flag, using the number attribute: The built in NATs ================= This is the primary application of the iter theory - an algebraic specification of the natural numbers that supports efficient builtin representation and operations. The natural numbers are constructed as follows: sorts Zero NzNat Nat . subsort Zero NzNat < Nat . op 0 : -> Zero [ctor] . op s_ : Nat -> NzNat [ctor iter special (...)] . Natural numbers can be input, and by default will be output in normal decimal notation; however 42 is just an alternative concrete syntax for s_^42(0). The command set print number on/off . controls whether decimal notation is used by the pretty printer. Note that redundant notation such as 00042 is not acceptable. metaParse() and metaPrettyPrint() support decimal notation however there is no other reflection of it - the metarepresentation of 42 is 's_^42['0.Zero] not '42.NzNat Nor is there XML support for it. Most of the usual arithmetic and bitwise operators are provided. They are not defined algebraically but could be given an algebraic definition by the user if desired. The operation semantics for most of the builtin operators is that you only get builtin behaviour when all the arguments are actually natural numbers. The exception is AC builtin operators which will compute as much as possible on natural number arguments and leave other arguments unchanged; so for example: red in NAT : gcd(gcd(12, X:Nat), 15) . results in: result Nat: gcd(X:Nat, 3) If the builtin operator does not disappear due to builtin semantics then user equations are tried. You can define functions on the Nats by matching into the sucessor notation; for example: fmod FACT is inc NAT . op _! : Nat -> NzNat . var N : Nat . eq 0 ! = 1 . eq (s N) ! = (s N) * N ! . endfm red 100 ! . red 1000 ! . It is even possible to get a specification of Z_{3} by fmod MOD3 is inc NAT . eq 3 = 0 . endfm However. apart from it's poor efficiency, this "writes up" from NzNat to Nat. Note that to avoid producing negative numbers, negation, subtraction and bitwise not are not provided. There is however symmetric difference: op sd : Nat Nat -> Nat [comm special (...)] . There is a limit on exponentiation in that builtin behavior will not occur if the first agumnent is > 1 and the second argument is too large. Similarly left shift does not work if the first argument is >= 1 and the second argument is too large. Currently "too large" means greater than 1000000 but this may change. Warning: it is easy to fill your machine's memory by generating huge natural numbers. Modular exponentiation op modExp : Nat Nat NzNat ~> Nat [special (...)] . has no such limits and may be useful for cryptographic algorithms. The built in INTs ================= The integers are constructed on top of the natural numbers as follows: sorts NzInt Int . subsort NzNat < NzInt Nat < Int . op -_ : NzNat -> NzInt [ctor special (...)] . Integers can be input, and by default are output in normal decimal notation; however -42 is just an alternative concrete syntax for - 42 which itself is just an alternative concrete syntax for - s_^42(0). As with NATs this notation is supported by metaParse() and metaPrettyPrint() but not by the metaterm representation or XML. Many of the operations in NAT extend to the integers, and a few new ones are provided. Bitwise operations on negative integers use the 2's complement representation. The built in RATs ================= The rationals are constructed on top of the integers and natural numbers as follows: sorts NzRat Rat . subsorts NzInt < NzRat Int < Rat . op _/_ : NzInt NzNat -> NzRat [ctor prec 31 gather (E e) special (...)] . Rationals can be input, and by default are output in normal decimal notation; however -5/42 is equivalent to -5 / 42 which is equivalent to - 5 / 42 which really denotes - s_^5(0) / s_^42(0). As with NATs and INTs this notation is supported by metaParse() and metaPrettyPrint() but not by the metaterm representation or XML. The numerator and denominator of a rational may contain common factors but these are removed by a single builtin rewrite whenever the rational is reduced (_/_ is not a free constructor). Some of the operations in INT are extended to rationals and a few new ones are provided. However unlike operations on the NATs and INTs these are defined in Maude by equations and may do some rewriting even when their arguments are not properly constructed rationals. Note that the choice of equations for defining operations on the rationals is motivated by performance - simpler equations are possible in many cases but they turn out to have a big performance penalty. op trunc : Rat -> Int . rounds its argument towards 0. op frac : Rat -> Rat . gives the fraction part of its argument and this always has the same sign as its argument. MachineInts replaced by number hierarchy ======================================== This is the most far reaching change since most of the builtin operations (except the model checker and sat solver) are affected to some extent and have their semantics subtly or not so subtly altered. fmod FLOAT is unaffected except some special hooks are renamed for consistancy. fmod STRING now protects NAT rather than MACHINE-INT. Nats are used in place of MachineInts which means that operations can no longer take nehative arguments. The String <-> MachineInt conversion functions are deleted. fmod FLOAT-CONVERSION is deleted. fmod NUMBER-CONVERSION is added to consolidate all the conversion functions between the 3 major builtin data types (Nats/Ints/Rats, Floats and Strings). op float : Rat -> Float . Computes the nearest Float to a given Rat. If the absolute value of the Rat falls outside the range representable by IEEE-754 double precision finite floating point numbers, Infinity or -Infinity is returned as appropriate. This seems consistant since Infinity & -Infinity are used to handle out-of-range situations in the Float world. op rat : FiniteFloat -> Rat . Converts finite Floats to Rats exactly (since every IEEE-754 finite floating point number is a rational number). Of course if the result happens to be a Nat or an Int that is what you get. rat(Infinity) and rat(-Infinity) do not reduce since they have no reasonable representation in the Rat would. It is intended that float(rat(F:FiniteFloat)) = F:FiniteFloat though I am relying on a 3rd party library (GNU gmp) for the yucky bit twiddling and I have not checked it's correctness. Also note that counterintuitive results are possible when converting from the approximate world of Floats to the exact world of Rats: red rat(1.1) . gives result NzRat: 2476979795053773/2251799813685248 This is because 1.1 cannot be represented exactly as a Float and the nearest Float is 1.100000000000000088817841970012523233890533447265625 which is the above rational. op string : Rat NzNat ~> String Converts a Rat to a String using a given base which must lie in the range 2,...,36. Of course Rats that are really Nats or Ints are converted to string representations of Nats or Ints so red string(-1, 10) . gives result String: "-1" op rat : String NzNat ~> Rat Converts a String to a Rat using a given base which must lie in the range 2,...,36. Of course if the result happens to be a Nat or an Int that is what you get. Currently the function is very strict about what strings are converted: the string must be something that the Maude parse would recognize as a Nat, Int or Rat. This could be changed to a more generous interpretation in the future. op string : Float -> String . op float : String ~> Float . These work as they did in FLOAT-CONVERSION. In particular float(string(F:Float)) == F:Float . op <_,_,_> : Int String Int -> DecFloat [ctor] . op decFloat : Float Nat -> DecFloat . DecFloats provide the means for arbirary formating of Floats as they did in FLOAT-CONVERSION. A DecFloat consists of a sign (1, 0 or -1), a String of digits and a decimal point position (0 is just in front of first digit, -ve is to the left, +ve is to the right). Thus < -1, "123", 11 > represents -1.23e10 . decFloat(F, N) converts F to a decFloat, rounding to N significant digits using the IEEE-754 "round to nearest" rule with trailing zeros if need. If N is 0, an _exact_ DecFloat representation of F is produced - this may require hundreds of digits. For any well formed Nat N: decFloat(Infinity, N) = < 1,"Infinity",0 > and decFloat(-Infinity, N) = < -1,"Infinity",0 > In fmod QID, the only operations that depended on MACHINE-INT were the deprecated backward compatibility operations so these are deleted. In fmod META-TERM some function definitions are rewritten to avoid the need for maxMachineInt. In fmod META-MODULE, Nats replace MachineInts and NatLists replace MachineIntLists: sort NatList . subsort Nat < NatList . op __ : NatList NatList -> NatList [ctor assoc] . op strat : NatList -> Attr [ctor] . op prec : Nat -> Attr [ctor] . In fmod META-LEVEL we need a notion of unbounded that was previously supplied by maxMachineInt. We use: sort Bound . subsort Nat < Bound . op unbounded : -> Bound . Also Nat replaces MachineInt in: op noParse : Nat -> ResultPair? [ctor] . The descent functions with modified semantics are: op metaRewrite : Module Term Bound ~> ResultPair . op metaFrewrite : Module Term Bound Nat ~> ResultPair . Rewrite limit is a Bound; it must be >= 1 and may be unbounded. Gas is now a Nat and must be >= 1. op metaApply : Module Term Qid Substitution Nat ~> ResultTriple? . op metaXapply : Module Term Qid Substitution Nat Bound Nat ~> Result4Tuple? . op metaMatch : Module Term Term Condition Nat ~> Substitution? . op metaXmatch : Module Term Term Condition Nat Bound Nat ~> MatchPair? . op metaSearch : Module Term Term Condition Qid Bound Nat ~> ResultTriple? . Last argument is always the solution number which is now a Nat. For metaXapply() and metaXmatch() the minimum depth is now a Nat. For metaXapply(), metaXmatch() and metaSearch() the maximum depth is now a Bound and can take the value unbounded. Statement Attributes ==================== Statements can now take attributes; currently only two statement attributes are available - more are planned. They are label, which is followed by an identifier and metadata which is followed by string. For example: eq foo = bar [label e1 metadata "lemma 1"] . cmb a : b if c [label m1] . rl quux => baz [metadata "\cite{Bloggs:2001}"] . Note that membership axioms and equations can now take labels rather than just rules. One use for such labels is in conjunction with the tracer/debugger. For example set trace on . set trace select on . trace select e1 . would cause selective tracing of rewrites that have e1 as top symbol _or_ involve a statement labeled e1 such as the equation above. In a similar vein it is possible to break into the debugger when a given labeled statement is about to execute: set break on . break select e1 . There will be other applications for labeled equations in the future. The old style rule labels are now supported as syntactic sugar, even for membership axioms and equations: eq [e1]: foo = bar [metadata "lemma 1"] . cmb [m1]: a : b if c . The metadata attribute is intended to hold data about the statement in whatever syntax the user cares to create/parse. It is like a comment that is carried around with the statement. Usual string escape conventions apply. Statement attributes and the new syntax for labels is reflected by the following changes to the metasignature: op label : Qid -> Attr [ctor] . op metadata : String -> Attr [ctor] . op mb_:_[_]. : Term Sort AttrSet -> MembAx [ctor] . op cmb_:_if_[_]. : Term Sort EqCondition AttrSet -> MembAx [ctor] . op eq_=_[_]. : Term Term AttrSet -> Equation [ctor] . op ceq_=_if_[_]. : Term Term EqCondition AttrSet -> Equation [ctor] . op rl_=>_[_]. : Term Term AttrSet -> Rule [ctor] . op crl_=>_if_[_]. : Term Term Condition AttrSet -> Rule [ctor] . There is no distinction at the sort level between statement and operator attributes but of course you should only pass operator attributes to operators and statement attributes to statements. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in ~eker/public_html/Maude/Alpha75a/ or downloaded from http://www.csl.sri.com/~eker/Maude/Alpha75a/ This version needs the same dynamic libraries as Alpha73. Bug fixes: 1 Bug in the tracing of polymorphic ops: set trace on . set trace select on . red in BOOL : true == false . Reported by Paco. 2 Bug in the metalevel uping of constants and variables at the kind level cause (illegal) Qids like 'a.'[Foo`] rather than 'a.`[Foo`] - reported by Paco. Other changes: 1 Free theory uses new style order-sorted discrimination nets for equational rewriting. This allows subsumed equations to be discarded. 2 Interpretation of discrimination nets optimized. 3 Special handling for free theory ternary symbols. 4 Substitution coloring; this helps with a performance bug noted in earlier release notes where there is a equation with a huge ground rhs. This would previously force all substitutions to have a slot for every subterm in such a rhs. Substitution coloring allows slots to be reused. 5 Two of the four pretty pinters rewritten to handle more disambiguation corner cases. There are 11 classes of operator that have special i/o representation and disambiguation needs: Polymorphs sort tests itor symbols variables flattened assoc symbols nats ints rats floats strings qids The last 3 have always been handled. The first 3 are still not handled. The middle 5 are now handled correctly by the object level. The two remaining pretty printers (metaPrettyPrint and term graph pretty printer) still need to be rewritten. The following ambiguous examples shows some of the corner cases now handled. fmod OVERLOAD is pr NUMBER-CONVERSION . sorts Foo Bar . ops 1 -42 1/2 N:Nat : -> Foo . op a : -> Foo . op a : -> Bar . op f : Foo Foo -> Foo [assoc] . op f : Bar Bar Bar -> Bar . endfm red 1 . red -42 . red 1/2 . red N:Nat . red f(a, a, a) . There are some new error messages for cases where a signature is created such that no disambiguation is possible. 6 Ctor declarations are now stored and printed out correctly with show all . whereas previously they were just comments. Ditto attribute does not copy ctor attribute but allows a ctor attribute to be included - this is because subsort polymorphic overloaded operators may reasonably have differing ctor status. 7 Term coloring partly implemented. This feature was called ctor debugging in previous discussions. The command is set print color on . Symbols within terms that are being executed (i.e. in trace or the final result of a reduce) are colored as follows: reduced, ctor not colored reduced, non-ctor, strangeness below blue reduced, non-ctor, no strangeness below red unreduced, no reduced above green unreduced, reduced directly above magenta unreduced, reduced not directly above cyan Strangeness is a colored operator. The idea is that red and magenta indicate initial locus of a bug while blue and cyan indicate secondary damage. Green denotes reduction pended and cannot appear in final result. It is instructive to run a trace of a reduction involving lazy operators: fmod SIEVE is pr NAT . sort List . subsort Nat < List . op nil : -> List [ctor]. op _,_ : Nat List -> List [ctor prec 31 gather (e E) strat (1 2 0)] . op l : Nat List -> List [ctor strat (0)] . op force : List Nat -> List . op ints-from : Nat -> List [ctor] . op sieve : List -> List . op filter : List Nat -> List . var N M : Nat . var L : List . eq ints-from(N) = l(N, ints-from(s(N))) . *** infinite list of Nats eq sieve(l(N, L)) = l(N, sieve(filter(L, N))) . *** the actual sieve eq filter(l(N, L), M) = if M divides N then filter(L, M) else l(N, filter(L, M)) fi . eq force(L, 0) = nil . eq force(l(N, L), s(M)) = N, force(L, M) . *** force lazy list endfm set trace on . set trace whole on . set print color on . red force(sieve(ints-from(2)), 10) . There is also Jose's missing case example: fmod NAT-MSET-MIN is sorts Nat NatMSet . subsort Nat < NatMSet . op 0 : -> Nat [ctor] . op s : Nat -> Nat [ctor] . op _ _ : NatMSet NatMSet -> NatMSet [assoc comm ctor] . op _<_ : Nat Nat -> Bool . op min : NatMSet -> Nat . vars N M : Nat . var S : NatMSet . eq 0 < s(N) = true . eq s(N) < 0 = false . eq s(N) < s(M) = N < M . eq min(N N S) = min(N S) . ceq min(N M S) = min(N S) if N < M . ceq min(N M) = N if N < M . eq min(N) = N . endfm set print color on . red min(s(0) s(s(0))) . red min(s(s(0)) min(s(0) s(0))) . Color & style due to format attributes are implicitly turned off to avoid confusion when "print color" is on. Operators that have assoc or iter attributes need to have all of their declarations have ctor or be without ctor. For other operators, if they have both with and without ctor declarations, ctorness is computed from arguments sorts. Finally there is a command introduced in Alpha73 that I forgot to document: set print rat off . switches off the special printing for _/_ in fmod RAT. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha76/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha76/ My Maude alpha release site now requires authentication: User Name: maudeabuser Password: bughunter The linux version is statically linked, while the solaris version only depends are standard solaris dynamic libraries - you should not have to install any shared objects to run these versions. This and future alpha releases include the source tree (alpha76.src.tar.gz). This is done for several reasons: (1) To allow static binaries while preserving your right to link against newer versions of GNU LGPL'd libraries it uses. (2) My hard drive died during the level 0 backup while I was at WRLA 2002 and this has left me paranoid about having the only Maude source tree on my local disk. (3) To allow white box testing. (4) Several people have expressed an interest in porting it to their favorite platform - although this may be premature as the source tree is rather messy and I'm planning a big reorganization before the end of the year. Note that the source code is not yet under the GNU GPL, and like the binaries should not be redistributed. Currently it only compiles with g++ 2.95.3. I will be moving it to a newer C++ compiler/stdc++ library in the near future. Other requirements are recent versions of bison and flex and the following 3rd party libraries: Doug Lea's malloc (ftp://g.oswego.edu/pub/misc/malloc.c) BuDDy (http://www.itu.dk/research/buddy/) Tecla (http://www.astro.caltech.edu/~mcs/tecla/) GNU GMP (http://www.swox.com/gmp/) I have mirrored them in: http://www.csl.sri.com/~eker/Maude/Lib/Src Bug fixes: (1) We used to allow iter operators with more or less than one argument which could provoke internal errors: fmod SUCC-BUG is sort Foo . op crash : -> Foo [iter] . endfm (2) The following example used to take O(n^3) time to abort due to a cascade of eager big num computations that are redone and thrown away during the stack unwinding (n = # of stack frames). fmod FACT is pr NAT . op _! : Nat -> NzNat . vars N M : Nat . eq 0 ! = s 0 . eq (s N) ! = s N * N ! . endfm red 10000 ! . ^C abort . The bug is now partly fixed by an extra test for abort in ACU_NumberOpSymbol; however the cascade of AC normalization is still O(n^2) (but far less noticable). A better ACU representation will eventually get this down to O(n log n) which will be unnoticable to the interactive user. (3) The performance bug noted in the Alpha71a release notes wrt associativity checking for kinds with many user sorts (Dilia's example) is mostly resolved by replacing the O(n^3) algorithm with a O(k.n^2) algorithm where k is the width of the sort diagram generated for the associative operator. k is bounded by the number of user sorts, n, and when n is large, k is typically much smaller. (4) We now check that terms kinds agree in eq/ceq/rl/crl meta-statements and =/:=/=> meta-condition fragments and metaMatch/metaXmatch/metaSearch descent functions. We also that term and sort kinds agree in mb/cmb meta-statements and : meta-condition fragments. The first of this large family of related bugs was reported by Peter. (5) The check for collapsing to a larger or incomparable sort via idempotence was the wrong way around. (6) Some missing operator sort declarations added to the prelude. Other changes: (1) Command line editing is supported using Tecla. There are a large number of commands and options - see http://www.astro.caltech.edu/~mcs/tecla/ for details. Basics: left/right arrow keys to move within line, up/down arrow keys for history and tab for file name completion. Also you get a continuation prompt rather than a blank line when Maude is expecting more input. (2) The line wrapper now notices changes in the terminal width (courtesy of Tecla). (3) The line wrapper uses a new algorithm that avoids inserting a newline when the next token (say a Nat or a String) is so long that it will hardwrap anyhow. (4) You can now use \ in String constants (just like in C++): red in STRING : "'The time has come,' the Walrus said, \ 'To talk of many things: \ Of shoes and ships and sealing wax, \ Of cabbages and kings; \ Of why the sea is boiling hot, \ And whether pigs have wings.'" . (5) The frozen attribute takes a list of numbers to freeze individual arguments; e.g.: op i : Foo Foo Foo -> Foo [frozen (1 3)] . Frozen on it's own freezes all arguments as before. The metalevel now only supports the list of numbers version: op frozen : NatList -> Attr [ctor] . though there is a nasty but temporary hack to allow the current version of Full Maude to run. This change necessitated replacing the frewrite algorithm - this is a good place to look for bugs. (6) There is a new attribute owise (or otherwise) that is only permitted for equations. An owise equation will only be applied at a redex if no regular equations apply at that redex. This feature should be used with care as it can make your specifications harder to analyze. In some ways it a bit like cut in Prolog or goto in C++. The reflection is op owise : -> Attr [ctor] . (7) The remaining ANSI escape sequences are now available in the format attribute as follows: p black (for pitch black... b is already used.) w white P Background black R Background red G Background green Y Background yellow B Background blue M Background magenta C Background cyan W Background white ? Dim f Blink (for flash... b is already used.) x Reverse video h Hidden I've included a modified version of interfere.maude from the WRLA 2002 demo to show what tricks are possible. (8) Warnings and advisories now have a more standardized form. Quoting of user identifiers used be very inconsistent, as well as confusing since ' and " can legally appear in identifiers. Instead color is used: Warning: red Advisory: green User identifiers: magenta However quoting of whole statments on lines of their own are not colored. (9) Compilation of operator declarations is now done lazily just as compilation of eqs/rls/mbs has been done for some time. This now means that some warnings and advisories will only show up when you actually do a reduction in a module. The benefit is a saving of cpu cycles and memory for loading large programs (such as Full Maude) where execution occurs in the last module. (10) There are a slew of under-the-hood changes such as an optimization in the main AC/ACU matcher, a new memory allocation mechanism for dag nodes and linking against newer 3rd party libraries. Hopefully these shouldn't have introduced any new bugs... Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha76a/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha76a/ This is an urgent bug fix release that just includes binaries and the changed source files. See Alpha76 for everything else. Bug fixes: (1) metaXmatch() complains about kind clashes between the pattern and subject terms; but this is perfectly legal for metaXmatch(). I overdid the checking introduced for bug fix (4) from Alpha76. Thanks to Carolyn for spotting this. (2) Tecla does not play well with Emacs (or vice versa depending on your point of view). There are two new command line flags: -tecla Use Tecla -no-tecla Don't use Tecla The default is to use Tecla unless: (a) standard input is not a tty; or (b) TERM environment variable is set to emacs or dumb. Thanks to Joe Hendrix for spotting this bug. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha77/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha77/ Alpha release site authentication: User Name: maudeabuser Password: bughunter Bug fixes: (1) A bug when reading files that don't end in with a newline. Maude usually fakes a newline in this case, but if the is an in/load near the end of the offending file, the flag to fake a newline will be set before the included file is read and then overwritten by the handling of the included file before the newline is faked. This is now fixed by stacking the flag. This bug was found by Peter. (2) There was a portability bug in the memory management that meant Maude would not work unless compiled with g++ 2.95.3. This is partly fixed by a rewrite of the memory manager. Although it's still not 100% ANSI compliant it should port to most platforms now. There are no new features but there are a lot of changes under the hood: (1) It's now compiled with g++ 3.2 and the ANSI compliant libstdc++ version 3. This may give a performance gain for some examples. I will probably remove support for the non-ANSI compliant libstdc++ version 2 in the near future. (2) In full AC/ACU matching, element variables are now pushed in to the bipartite graph problem rather than the Diophantine system problem in order to reduce the search space. This should help with Merrill's "killer rules" during search/model checking. (3) Iterators used for A/AU/AC/ACU arguments lists; this may improve performance. SPEED_HACKs removed from A/AU/AC/ACU code. (4) More special casing for full AC/ACU matching. (5) AC/ACU subpatterns of the form f(X, t) where t is ground and X is not yet bound now get to use greedy matching even if X occurs elsewhere in pattern or condition - since subpatterns with this form can match in at most one way. (6) A number of low level changes to the AC/ACU code to avoid unnecessary copying and unpredicatable branches. (7) Matching a variable with extension (i.e. at the top) against an AC/ACU subject is now a little smarter. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha78/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha78/ Alpha release site authentication: User Name: maudeabuser Password: bughunter Bug fixes: (1) A warning is now generated for single argument empty syntax operators; these have never been allowed in eithe OBJ3 or Maude. Bug reported by Feng Chen. The main change in this version is a new term representation along with new matching and renormalization algorithms for the AC and ACU theories. For some simple patterns, this enables rewrites that would have taken time linear in the size of the subject (using the old greedy matching) to execute in log time (using the new greedy matching). This can be a big win if the subject has thousands of alien subterms under an AC/ACU operator. In particular it is now feasible to implement maps using AC or ACU rewriting - see mapExample.maude So far the new method is only implemented for a small subset of patterns and in particular it does not work at all for conditional equations. Nor does it work for rules in model checking or search where all matches are needed. In these cases the subject must be converted to the old representation in order to use the old algorithms, and thus things can get slower. I expect to increase the subset of patterns handled and make the heuristics for switching between representations smarter in future versions. However since this is such a radical change to the guts of the rewrite engine I am putting this version out so people can check if anything is broken. Two changes that you may notice: (1) The term ordering for terms headed by AC/ACU operators has changed slightly. (2) The matches chosen and hence the sequence of rewrites may differ. Neither of these should be a problem if your specification is confluent. There are some minor changes agreed at various Maude teleconferences: (1) =>1 replaces => for one step search in search command. This is to avoid confustion with => in conditions which means search for 0 or more step proofs (=>* in search command). This also affect the XML output. (2) fmod NUMBER-CONVERSION renamed to CONVERSION since Carolyn pointed out that it also involves strings. Unfortunately this breaks Full Maude. (3) _|=_ which use to do double duty in the model checker is now just used for satisfaction and lives in fmod SATISFACTION. The operator to actually start the model checker is now: op modelCheck : State Formula ~> ModelCheckResult . This enables checking satisfaction without invoking the model checker. (4) If you get an internal error, bug report address is now: maude-bugs@maude.cs.uiuc.edu Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha79/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha79/ Alpha release site authentication: User Name: maudeabuser Password: bughunter Bug fixes: (1) Bug where pointer was printed in a "can't continue." message if cont . was typed after start up. (2) iter matching against a bare variable with extension now works so for example you can do: mod ITER-SEARCH is inc NAT . op f : Nat -> Nat . var X : Nat . rl X => f(X) . endm search 6 =>1 X . Not so much a bug as an unimplemented corner case. (3) A nasty bug in the ACU/AC sort calculation where I assumed that assignments to variables couldn't be in the error sort; this assumption no longer holds since we have variables at the kind level. This bug is exposed by the following code. fmod ACU-SORT-BUG is sort Foo . ops a b c d e : -> Foo . op k : -> [Foo] . op f : Foo Foo -> Foo [assoc comm] . var K : [Foo] . eq f(a, K) = K . endfm red f(a, b, c, k) . *** result should be at kind level (4) Similar bug in the AU/A sort calculation. (5) Bug in ACU Red-Black matcher code that could miss matches against subjects of the form f(a, X), a ground, if the subject had a strange sort structure. (6) Similar bug in specialized matcher for f(X, Y) case. (7) Stale pointer bug in the code that echos match/search commands in the case that the pattern flattened or collapsed during normalization (reported by Christiano Braga). (8) A nasty bug in the original greedy matcher, where it fails to find a match, but decides there is no match rather than running the full matcher. fmod GREEDY-BUG is sorts E1 E2 P T . subsort E2 < E1 P < T . op f : P P -> P [assoc comm] . op f : T T -> T [assoc comm] . op i : T -> T . op a : -> E2 . op b : -> E1 . ops c d : -> P . op ok : -> T . eq i(f(X:E1, X:E1, Y:P, Z:P)) = ok . endfm red i(f(a, a, b, b, c, d)) . match i(f(X:E1, X:E1, Y:P, Z:P)) <=? i(f(a, a, b, b, c, d)) . The main change in this version is that I have implemented the new AC/ACU representation and matching for a wider class of patterns. I've also revamped the old AC/ACU matcher and made a few optimizations in other places. To see how the recent changes have affected AC/ACU rewriting I have run the last 3 alphas on the mapExample.maude that I distributed with Alpha78 and 4 other AC/ACU benchmarks that I've put in: http://www.csl.sri.com/~eker/Maude/Benchmarks/ Here are the results I got on a 2.8GHz Xeon. Some of the benchmarks are very stack intensive so remember to "unlimit stacksize" to avoid a stack overflow segmentation fault. Also you need lots of RAM. 8 cpu minutes is where my patience gives out :) Alpha79 -------- setHierarchy.maude rewrites: 6667125 in 6550ms cpu (6560ms real) (1017881 rewrites/second) simpleSet.maude rewrites: 766675 in 2480ms cpu (2480ms real) (309143 rewrites/second) rewrites: 833341 in 2670ms cpu (2670ms real) (312112 rewrites/second) tautology.maude rewrites: 554823 in 990ms cpu (990ms real) (560427 rewrites/second) threeElt.maude rewrites: 2192505 in 44780ms cpu (44770ms real) (48961 rewrites/second) mapExample.maude rewrites: 599 in 0ms cpu (0ms real) (~ rewrites/second) rewrites: 5999 in 20ms cpu (10ms real) (299950 rewrites/second) rewrites: 59999 in 210ms cpu (210ms real) (285709 rewrites/second) rewrites: 599999 in 2820ms cpu (2830ms real) (212765 rewrites/second) Alpha78 -------- setHierarchy.maude rewrites: 6667125 in 109820ms cpu (109830ms real) (60709 rewrites/second) simpleSet.maude > 8 cpu minutes > 8 cpu minutes tautology.maude rewrites: 554823 in 1550ms cpu (1550ms real) (357950 rewrites/second) threeElt.maude rewrites: 2192505 in 60800ms cpu (60790ms real) (36060 rewrites/second) mapExample.maude rewrites: 599 in 0ms cpu (10ms real) (~ rewrites/second) rewrites: 5999 in 10ms cpu (10ms real) (599900 rewrites/second) rewrites: 59999 in 220ms cpu (210ms real) (272722 rewrites/second) rewrites: 599999 in 2820ms cpu (2820ms real) (212765 rewrites/second) Alpha77 -------- setHierarchy.maude rewrites: 6667218 in 48610ms cpu (48610ms real) (137157 rewrites/second) simpleSet.maude > 8 cpu minutes > 8 cpu minutes tautology.maude rewrites: 554819 in 1560ms cpu (1560ms real) (355653 rewrites/second) threeElt.maude rewrites: 2193693 in 50690ms cpu (50700ms real) (43276 rewrites/second) mapExample.maude rewrites: 599 in 0ms cpu (0ms real) (~ rewrites/second) rewrites: 5999 in 150ms cpu (140ms real) (39993 rewrites/second) rewrites: 59999 in 55000ms cpu (55000ms real) (1090 rewrites/second) > 8 cpu minutes There are also some changes to the source code that should make porting easier; in particular the #pragmas that caused linking problems with certain versions of g++ are gone. I used g++ 3.2. I notice that some people have been discouraged from using Alpha78 because it breaks FullMaude. A work around for Alpha79 is to run it with the prelude.maude from Alpha77. Then fm75-5.maude should work as it did in Alpha77. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha80/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha80/ Alpha release site authentication: User Name: maudeabuser Password: bughunter Bug fixes: (1) A bug in the AU greedy matcher provoked by: fmod AU_GREEDY_BUG is op l : List List -> List [assoc id: nil] . op nil : -> List . sort List Elt . subsort Elt < List . ops a b : -> Elt . var E : Elt . var M N : List . op f : List -> List . eq f(l(E, M, N)) = M . endfm red f(l(a, b)) . (2) A really subtle bug in the AU Boyer-Moore based matcher provoked by: mod AU_META is sort S . op l : S S -> S [assoc] . ops a b c d e : -> S . op g : S -> S . rl [1]: l(g(a), g(X:S)) => e . endm red in META-LEVEL : metaXapply( ['AU_META], 'l['b.S, 'g['a.S], 'g['b.S], 'c.S, 'd.S], '1, none, 0, 0, 0) . red in META-LEVEL : metaXapply( ['AU_META], 'l['b.S, 'g['a.S], 'g['b.S], 'c.S, 'd.S], '1, 'X:S <- 'b.S, 0, 0, 0) . The problem is that since g(X:S) subsumes g(a) so when g(X:S) fails to match something we get a shift of 2. However in the second example g(X:S) fails to match g(a) because X:S is bound, and we cannot assume that the subpattern g(a) will fail on subject g(a) (i.e. a shift of 1). Shifting by 2 causes us to miss the match. The problem is that subsumption doesn't take account of variables being bound by some external agency (the META-LEVEL). The Boyer-Moore based AU matcher is probably overkill... does anyone have real examples with an A/AU pattern where shifting the pattern versus the subject benefits from the Boyer-Moore shift table? Changes ======== (1) The big change is a new term representation along with new matching and renormalization algorithms for the A and AU theories. For some simple patterns, this enables rewrites that would have taken time linear in the size of the subject (using the old greedy matching) to execute in constant time (using the new greedy matching). This can be a big win if the subject has thousands of alien subterms under an A/AU operator. In particular you can now reverse an associative list in linear time using any of the 3 obvious algorithms - see revExample.maude - and remember to "unlimit stacksize". The new representation is only supported for A/AU symbols that: (a) don't have a 1-sided identity; and (b) don't have equations that rewrite at the top. (2) Some optimizations to reduce the number and size of stack frames needed for deep recursions. (3) For my convenience: set print color on . now colors terms appearing in modules by operator theory according to the following scheme (previously only rewritten terms were colored according their reduction status): AC red ACU magenta A green AU, AUl, AUr cyan C, CU, CI CUI blue U, Ur, Ul, I, UI, UrI, UlI yellow iter, free black This color scheme may need to change if more theories are added. (4) At Jose's request: eq f => g = [] (f -> g) . eq f <=> g = [] (f <-> g) . added to model-checker.maude (5) fmod EXT-BOOL added to prelude.maude Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha80a/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha80a/ Alpha release site authentication: User Name: maudeabuser Password: bughunter Bug fixes: =========== (1) A bug where metadata was not copied on importation: fmod METADATA is sort Foo . ops a b : -> Foo . eq a = b [metadata "bar"] . endfm fmod IMPORTER is inc METADATA . endfm show all . red in META-LEVEL : upEqs('IMPORTER, true ) . Changes ======== (1) The AC/ACU theory now uses a simpler, faster version of red-black trees where the size of subtrees are no longer stored in each node. I've eliminated much special case code that no longer gives a performance win. One user visible change is that AC/ACU contexts at the metalevel are no longer flattened. For example: reduce in META-LEVEL : metaXmatch(fmod 'FOO is protecting 'BOOL . sorts 'Foo ; 'Bar . subsort 'Bar < 'Foo . ((op 'f : 'Foo 'Foo -> 'Foo [assoc comm] . op 'c : nil -> 'Foo [none] .) op 'b : nil -> 'Foo [none] .) op 'a : nil -> 'Foo [none] . none none endfm, 'f['X:Foo,'Y:Foo], 'f['a.Foo,'b.Foo,'c.Foo,'c.Foo], nil, 0, s_^100(0), s_^30(0)) . used to produce: rewrites: 1 in 0ms cpu (2ms real) (~ rewrites/second) result MatchPair: { 'X:Foo <- 'b.Foo ; 'Y:Foo <- 'a.Foo,'f['c.Foo,'c.Foo,[]]} but will now produce: rewrites: 1 in 0ms cpu (3ms real) (~ rewrites/second) result MatchPair: { 'X:Foo <- 'b.Foo ; 'Y:Foo <- 'a.Foo,'f['f['c.Foo,'c.Foo],[]]} (2) There is a first implementation of object-message rewriting. The special behaviour is associated with configuration constructors which must be AC and may optionally have an identity. op c : Foo Foo -> Foo [ctor config assoc comm] . Configuration only have their special behavior wrt arguments that have object and message constructors on top. Object and message constructors must have at least one argument: op ob : Bar -> Foo [ctor object]. op m : Bar -> Foo [ctor msg]. An operator can have at most one of the 3 new attributes: config, object and msg. For object constructors, the first argument is considered to be the objects name. For message constructors, the first argument is considered to be the messages target. There may be multiple configuration, object and message constructors. A rule is consider to be an object-message rule if all the following hold: (a) Its lhs has a configuration constructor on top with two arguments A and B (b) A and B are stable (cannot change their top symbol under a substitution). (c) A has a message constructor on top. (d) B has an object constructor on top. (e) The first arguments of A and B are identical. The new behavior appears with the command frewrite and the descent function metaFrewrite(). When the fair traversal attempts to perform a single rewrite on a term headed by a configuration constructor, the following happens: (a) Arguments headed by object constructors are collected. It is a runtime error for more than one object to have the same name. (b) For each object, messages with its name as first argument are collected and placed in a queue. (c) Any remaining argments are placed on a remainder list. (d) For each object, and for each message in its queue, an attempt is made to deliver the message by performing a rewrite with an object-message rule. If all applicable rules fail, the message is placed on the remainder list. If a rule succeeds, the rhs is constructed, reduced, and the result is searched for the object. Any other arguments in the result configuration go onto the remainder list. If the object cannot be found, any messages left in its queue go onto the remainder list. Once its message queue is exhausted, the object itself is placed on the remainder list. (e) A new term is constructed using the configuration constructor on top of the arguments in the remainder list. This is reduced, and a single rewrite using the non-message-object rules is attempted. There is no restriction on object names, other than uniqueness. An object may change its object constructor during the course of a rewrite and delivery of any remaining message will still be attempted. If the configuration constructor changes during the course of a rewrite, the resulting term is considered alien, and does not participate any further in the object-message rewriting for the original term. The order in which objects are considered and messages delivered is system dependent, but note that newly created message are not delivered until some future visit to the configuration (though all arguments including new messages and alien configurations could potentially participate in the single non-message-object rewrite attempt. Message delivery is "just" rather than "fair" - in order for message delivery to be guarenteed, an object must always be willing to accept the message. If multiple object-message rules contain the same message constructor they are tried in a round robin fashion. Non-message-object rules are also tried in a round robin fashion for the single non-message-object rewrite attempt. The counting of object-message rewrites is strange: For the purposes of the rewrite argument given to frewrite, a visit to a configuration that results in one or more rewrites counts as a single rewrite; though for other accounting purposes all rewrites are counted. Finally, for tracing, profiling and breakpoints only, there is a fake rewrite at the top of the configuration in the case that object-message rewriting takes place but the single non-message-object rewrite attempt fails. It is not included in the reported rewrite total, but is inserted to keep tracing consistent. Object-message rewriting is reflected by op config : -> Attr [ctor] . op object : -> Attr [ctor] . op msg : -> Attr [ctor] . in fmod META-MODULE. (3) The nonexec statement attribute is supported. Inadmissable rules, equations and memberships are required to use it. When a statement has the nonexec attribute, it is not used for rewriting. Nonexec rules can be used by metaApply()/metaXapply() and nonexec statements can be upped with the ascent functions. As a temporary backward compatibility hack for FullMaude users, inadmissable rules that don't use nonexec get a warning, but then the nonexec attributed is then added rather than ignoring the rule. The nonexec statement attribute is reflected by op nonexec : -> Attr [ctor] . in fmod META-MODULE. Paco has released Full Maude 80-1 which is compatible with Alpha80/80a and I have put this in the release directory. You should not use an older prelude.maude with Alpha80a since the metalevel hooks have changed. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha80b/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha80b/ Alpha release site authentication: User Name: maudeabuser Password: bughunter This version claims to be Maude 2.0 at startup - this is because unless any show stoppers are reported before I leave for Spain it is what we will release at RTA 2003. Bug fixes: =========== (1) A bug where the bug reporting address was not always printed when Maude crashed. This was caused by the line wrapper being in a bad state - it is now bypassed with a system call. Bug reported by Ambarish. (2) The special hook mechanism no longer crashes if there is a missing sort; but bad hooks is still a good way to corrupt memory. Bug reported by Christiano Braga. Changes: ========= The most important change is that this version is released under the GNU GPL - see the source tree for details - so you may redistribute it. The other major change is that the persistent AC/ACU rewriting now supports conditional rewriting for certain patterns - though this is more of a proof of concept than comprehensive implementation. There are several minor changes: op extending_. : ModuleExpression -> Import [ctor] . is added to fmod META-MODULE. For associative and iterated operators (assoc & iter attributes) the operational semantics of mbs/cmbs is tidied up. It is now an error to have both non-kind declaractions and mbs/cmbs for the same associative or iterated operator but non-kind declaractions can be converted to mbs as long as there is a kind declaractions. So instead of fmod ASSOC-MB1 is sort Foo . op f : Foo Foo -> Foo [assoc comm] . op e : -> [Foo] . ops a b c d : -> Foo . mb f(a, e) : Foo . endfm red f(a, b, e) . red f(a, b, e, a) . red f(e, b, e, a) . red f(a, b, e, e, a) . red f(a, a, b, e, e, a) . write fmod ASSOC-MB2 is sort Foo . op f : [Foo] [Foo] -> [Foo] [assoc comm] . op e : -> [Foo] . ops a b c d : -> Foo . mb f(X:Foo, Y:Foo) : Foo . mb f(a, e) : Foo . endfm red f(a, b, e) . red f(a, b, e, a) . red f(e, b, e, a) . red f(a, b, e, e, a) . red f(a, a, b, e, e, a) . and instead of fmod ITER-MB1 is sort Foo . op f : Foo -> Foo [iter] . op e : -> [Foo] . mb f(e) : Foo . endfm red f(e) . red f(f(e)) . red f(f(f(e))) . write fmod ITER-MB2 is sort Foo . op f : [Foo] -> [Foo] [iter] . op e : -> [Foo] . mb f(X:Foo) : Foo . mb f(e) : Foo . endfm red f(e) . red f(f(e)) . red f(f(f(e))) . For this build I have removed the integrated compiler and MOS oracles - though the code is still in the source tree. These features are not officially part of the release and will not be documented in the manual. I have also removed the Full Maude hack from prelude.maude - the 2.0 release of Full Maude should not need it. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha81/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha81/ Alpha release site authentication: User Name: maudeabuser Password: bughunter This version reports itself as Maude 2.0.1 and will be released as such if no show stoppers are found. Bug fixes: (1) A critical bug in the AC/ACU matcher (reported by Paco) triggered by the following example: fmod AC-BUG is inc NAT . sorts NatSet State . subsort Nat < NatSet . op i : Nat -> Nat . op g : NatSet NatSet -> NatSet [assoc comm] . op f : NatSet NatSet -> State . var X : Nat . vars S T : NatSet . endfm match f(g(X, S), g(i(X), T)) <=? f(g(0, 1), g(g(i(1), i(2), i(3), i(4), i(5), i(6), i(7), i(8)), i(9)) ) . (2) A bug where Maude would go into infinite recursion when a unary operator had empty syntax (reported by "Sylvan S. Pinsky" ): fmod BUG is sorts T A . subsorts T < A . op __ : A A -> A . ops pl(_) +(_) : T -> A . vars g h : A . endfm red h g . Other Changes ============== The big change is that the builld system now uses autoconf/automake for easier porting. There are also many portability fixes. There are ready made binaries for: maude.darwin Darwin (Mac OSX), dynamically linked maude.freeBSD i86 Free BSD, dynamically linked maude.linux i86 Linux, statically linked maude.macLinux Mac Linux, statically linked maude.alpha DEC Alpha OSF, statically linked maude.solaris Sparc Solaris, dynamically linked So far I've failed to make it build on AIX (insufficient memory to link), HPUX (math library issues) and SGI/IRIX (g++/libstdc++ issues). There are now --help and --version command line flags. The internal ordering on Qids is now alphabetical at Manuels request. Previously it was based on the order the underlying identifiers had been seen which caused reproducibility problems for proof scripts. I will be out of town and off line for the next 2 weeks, though I may be able to read email sent to steveneker@att.net (no large files!). Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha82/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha82/ 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 Solaris - I will make a MacOSX binary in the near future. Bug fixes ========== (1) Infinity and -Infinity now work on MacOSX (and FreeBSD) - previously Infinity was converted to 0. Reported by Carolyn. (2) Various bugs in show module (and show all) commands fixed. Reported by Narciso. (3) Break points no longer cause an internal error when executing builtin function symbols. Reported by Christiano Braga. (4) metaPrettyPrint() now handles variables at the kind level correctly. Reported by Joe Hendrix. (5) Printing a sort redeclaration warning from the metalevel no longer causes an internal error. Reported by Peter Olveczky. (6) Various files (ChangeLogs and compiler code) that were accidently left out of the last source tree are included - automake files are fixed. Other changes ============== (1) The semantics over owise equations wrt operator level strategies has changed. Now owise equations can only be used in evaluating the final 0 of a strategy. This change was suggested by Joe Hendrix. (2) The Int operators quo, rem, gcd, lcm, divides now work on Rats. quo gives the number of whole times a rational can be divided by another, rem gives the rational remainder. divides returns true if a rational divides a rational a whole number of times. gcd returns the largest rational that divides into each of its arguments a whole number of times while lcm returns the smallest rational that is an integer multiple of its arguments. (3) Ctor coloring is now supported for iter symbols: set print color on . fmod ITER-COLOR is sorts Nat0 Nat1 Nat2 Nat . subsort Nat0 Nat1 Nat2 < Nat . op s_ : Nat0 -> Nat1 [iter ctor] . op s_ : Nat1 -> Nat2 [iter ctor] . op s_ : Nat2 -> Nat0 [iter] . op 0 : -> Nat0 [ctor] . endfm red s 0 . red s s 0 . red s s s 0 . red s s s s 0 . (4) META-LEVEL has two new polymorpic functions: op upTerm : Universal -> Term [special (...)] . op downTerm : Term Universal -> Universal [special (...)] . upTerm() converts a term into it's meta-representation, while downTerm() converts a meta-term into a regular term. They can handle regular terms at the kind level. The 2nd argument to downTerm is a term belonging to the appropriate component that is returned should the meta-term not represent a valid term in that component. fmod UP-DOWN-TEST is inc META-LEVEL . sort Foo . ops a b c d e : -> Foo . op f : Foo Foo -> Foo . eq c = d . endfm red upTerm(upTerm(f(a, f(b, c)))) . red downTerm(downTerm(upTerm(upTerm(f(a, f(b, c)))), X:Term), a) . (5) The configuration now supports building without Tecla (--with-tecla=no). Requested by Ambarish. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha83/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha83/ 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, Solaris and Darwin. Bug fixes ========== (1) A bug in the meta-context code where iter operators were not properly handled. Reported by Alberto Verdejo, and provoked by the following example: red in META-LEVEL : metaXmatch(mod 'SORTING is protecting 'BOOL . protecting 'STRING . protecting 'NAT . sorts 'Pair ; 'PairSet . subsort 'Pair < 'PairSet . op '<_;_> : 'Nat 'String -> 'Pair [none] . op '__ : 'PairSet 'PairSet -> 'PairSet [assoc comm id('empty.PairSet)] . op 'empty : nil -> 'PairSet [none] . none none rl '__['<_;_>['J:Nat,'X:String],'<_;_>['I:Nat,'Y:String]]=> '__['<_;_>[ 'J:Nat,'Y:String],'<_;_>['I:Nat,'X:String]] [label('switch)] . endm, '__['<_;_>['B:Nat,'C:String],'<_;_>['A:Nat,'D:String]], '__['<_;_>['s_['0.Zero],'"d".Char],'__['<_;_>['s_^2['0.Zero], '"b".Char],'__['<_;_>['s_^3['0.Zero],'"a".Char],'<_;_>['s_^4['0.Zero], '"c".Char]]]], '_and_['_<_['B:Nat,'A:Nat],'_>_['C:String,'D:String]] = 'true.Bool, 0, unbounded, 0) . (2) A bug in the handling of bubbles at the object level where adding an "Exclude" id-hook caused the bubble property to be ignored. Provoked by the following example: fmod BUBBLE-TEST is inc QID-LIST . sort Text . op text : QidList -> Text [special ( id-hook Bubble (1 -1 ( )) id-hook Exclude ( x y z ) op-hook qidSymbol ( : ~> Qid) op-hook qidListSymbol (__ : QidList QidList ~> QidList))] . op f : Text -> Bool . endfm red f( a c b ) . Other changes ============== (1) Polymorphic operators are now declared explicitly by the polymorphic (abbreviates to poly) attribute. This take a set of integers enclosed in parentheses that indicates which arguments are polymorphic; 0 indicates the range. For polymorphic operators that are not constants, at least one argument should be polymorphic to avoid ambiguities. Since there are no polymorphic equations, polymorphic operators are limited to constructors and builtins. Polymorphs are always instantiated with the polymorphic arguments going to the kind level which further limits their generality. The sort name in a polymorphic position is purely a place holder - any legal type name could be used but it seems a useful convention to use "Universal". One reasonable use for polymorphic operators beyond the existing builtins is to define hetrogeneous lists: fmod HET-LIST is inc CONVERSION . sort List . op nil : -> List . op __ : Universal List -> List [ctor poly (1)] . endfm red 4 "foo" 4.5 1/2 nil . The polymorphic attribute is reflected by: op poly : NatList -> Attr [ctor] . (2) The show all and show mod commands now print out the special attribute and its hooks. (3) The set of ascent functions is completed with: op upModule : Qid Bool ~> Module . op upImports : Qid ~> ImportList . op upSorts : Qid Bool ~> SortSet . op upSubsortDecls : Qid Bool ~> SubsortDeclSet . op upOpDecls : Qid Bool ~> OpDeclSet . These work in an analogous fashion to the existing ascent functions. Note that upImports() does not take a Bool since it is not useful to query the imports of a flattened module. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha83a/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha83a/ 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, Solaris and Darwin. Since this version contains a lot of new code and will likely be used as the basis for a 2.1 release at WRLA 2004 I would appreciate people trying to break it. Also the linux version was built on my Mandrake 9.2 home box rather than on my Red Hat 7.3 desktop so I'm hoping it will resolve the tecla/library issue people have been complaining about under newer linux distros. Bug fixes ========== (1) An internal error that occurred when bubbles were imported: fmod FOO is inc QID . sorts Token Foo . op token : Qid -> Token [special(id-hook Bubble (1 1) op-hook qidSymbol ( : ~> Qid))] . op [_] : Token -> Foo . endfm fmod BAR is inc FOO . endfm (2) An nasty memory corruption bug when copying persistent representations of dag nodes. Copying of dags only occurs for non-eager strategies and conditional membership axioms (because cmbs can potentially be applied in lazy subdags) to avoid side effects in shared subdags. Thus this problem only shows up in rare examples such as one by Jose, and the effect of the memory corruption may not be immediately visible even then. (3) An internal error that occurred when a meta-module is incompletely pulled down, and one of the modules it depended on is overwritten: red in META-LEVEL : metaReduce( fmod 'FOO is including 'NAT . sorts 'Foo . none none none X:EquationSet endfm, '0.Nat) . fmod NAT is endfm Other changes ============== The main change is a major overhaul of the module system which now supports simple module expressions formed by summation and renaming. Module expressions can only be used in importation statements. The they have the syntax: ::= | "(" ")" | "+" | "*" := "(" { "," }* ")" := "sort" "to" | "label" "to" | "op" | "op" ":" * "->" := "to" [ "[" + "]" ] + is associative; * binds tighter than + and groups to the left. The only attributes currently allowed are prec, gather and format - the idea is that when you rename an operator, the old syntactic properties may no longer be legal and are reset to defaults unless you explicitly set them with these attributes. Modules are constructed for each subexpression of a module expression and so each signature must be legal. Modules and module expressions are cached both to save time and so that the same module corresponding to a module expression will not be imported twice via a diamond import. Mutually or self recursive imports occurring through module expressions are detected and disallowed. Cached modules generated by module expressions that no longer have any users (if the module(s) containing the module expression have been replaced) are deleted. When a named module A, used in a module expression is replaced, any modules generated for module expressions that (possibly indirectly) depend on A are deleted and any named modules that (possibly indirectly) depend on A are reevaluated if you attempt to use them. Here the notion of "depends on" is transitive through arbitrary nesting of importation and module expressions. Summations are flattened before being evaluated so A + (B + C) creates a single new module A + B + C, which is considered to be an otherwise empty module that includes A, B and C. A summation is an fmod if all the summands are fmods and a mod otherwise. Renaming a module that has imports is a subtle issue. To avoid duplicating imported modules unnecessarily and ending up with a lot of duplicated contents (say many identical copies of BOOL), the module importation structure is maintained throughout the renaming. A module expression A * R evaluates to A if A contains no contents that are affected by R. Otherwise A * R evaluates to a new module A * R' where R' is obtained by deleting those renaming items that don't affect A, and canonizing the types in operator renamings wrt A (see later). If A imports modules B and C, A * R' will import modules found by evaluating B * R' and C * R'. Operators with the poly attribute are only affected by operator renamings that don't specify types. Renaming a module does not change its module type. There are some subtle cases to handle. Consider: fmod A is sort Foo . op a : -> Foo . op f : Foo -> Foo . endfm fmod B is including A . sort Bar . subsort Foo < Bar . op f : Bar -> Bar . endfm fmod C is inc B * (op f : Bar -> Bar to g) . endfm Here the f in A looks as though is isn't affected by the renaming, but because of the subsort declaration in B, it should be renamed for consistency. This is handled is by canonizing the type Bar occurring in the renaming (op f : Bar -> Bar to g) to the kind expression [Foo,Bar] which includes _all_ of the sorts in the kind [Bar] occurring in B. Thus B * (op f : Bar -> Bar to g) evaluates to a new module B * (op f : [Foo,Bar] -> [Foo,Bar] to g) which includes the module expression A * (op f : [Foo,Bar] -> [Foo,Bar] to g) which evaluates to a new module A * (op f : [Foo] -> [Foo] to g) in which f has been renamed. Consider also: fmod A is sorts Foo Bar . endfm fmod B is inc A . op f : Foo -> Foo . endfm fmod C is inc A . subsort Foo < Bar . op f : Bar -> Bar . endfm It is _not_ the case that (B + C) * (op f : Bar -> Bar to g) and (B * (op f : Bar -> Bar to g)) + (C * (op f : Bar -> Bar to g)) evaluate to the same module because in the latter, the f occurring in B will not be renamed. Hence in general * does not distribute over +. Note that this behavior differs from Full Maude where both module expressions evaluate to the same module - which module depends on the order that Full Maude sees the module expressions. Module expressions are reflected in the metalevel through the new META-MODULE declarations: sorts Renaming RenamingSet . subsort Renaming < RenamingSet . op sort_to_ : Qid Qid -> Renaming [ctor] . op op_to_[_] : Qid Qid AttrSet -> Renaming [ctor format (d d d d s d d d)] . op op_:_->_to_[_] : Qid TypeList Type Qid AttrSet -> Renaming [ctor format (d d d d d d d d s d d d)] . op label_to_ : Qid Qid -> Renaming [ctor] . op _,_ : RenamingSet RenamingSet -> RenamingSet [ctor assoc comm prec 43 format (d d ni d)] . op _+_ : ModuleExpression ModuleExpression -> ModuleExpression [ctor assoc comm] . op _*(_) : ModuleExpression RenamingSet -> ModuleExpression [ctor prec 39 format (d d s n++i n--i d)] . in the obvious way. Bashing together of previously unrelated sorts operators and used to be regarded as illegal; however it is now legal and the previous warnings have been downgraded to advisories: fmod FOO is sort Foo . op a : -> Foo . endfm fmod BAR is sort Foo . op a : -> Foo . endfm fmod BAZ is inc FOO + BAR . endfm Note that you get two sets of advisories - one for (FOO + BAR) and one for BAZ. There is a new command show modules . which shows the named and created modules currently in the system. The latter are ephemeral and the garbage collection policy for created modules may change. Operators with the poly attribute may now be ad hoc overloaded (but not subsort polymorphic overloaded). This is not recommended since it can lead to ambiguities for parsing and pretty-printing. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha84/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha84/ Alpha release site authentication: User Name: maudeabuser Password: bughunter This version reports itself as Maude 2.1 and will be released as such if no show stoppers are found between now and next Thursday. This version has binaries for Mac/Linux, HP-Alpha/OSF and x86/Free BSD in addition to the usual platforms. Bug fix ======== A bug in the post syntax error clean up code which freed module expression structures that it should not, resulting in memory corruption, random warnings, and an internal error following a syntax error. Reported by Azadeh Farzan and Carolyn. For example: fmod FOO is protecting NAT . op f : -> Nat Nat . endfm fmod FOO is endfm Other changes ============== This version uses recently released Tecla 1.5.0 which resolves various issues on newer linux versions. Unfortunately I haven't been able to get this Tecla version to build under Panther so the Darwin binary still uses Tecla 1.4.1. The is also to possibility that the Darwin binary may not run under earlier MacOS X versions. There is now a rudimentary test suite in the source tree; use make check to run it after building from source. In order to support automated testing the is a new command line flag -no-banner which suppresses the banner (which will differ between versions making output comparison harder). Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha84b.1/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha84b.1/ Alpha release site authentication: User Name: maudeabuser Password: bughunter This version is a slightly patched version of Alpha84b to fix a critical bug in the AU sort calculation code reported by Jon Haugsand. A simplified version of his example that exposes the problem is fmod SORT-INT is pr INT . sorts Seq Pseq Tree . subsorts Int < Pseq < Seq . op ntree : -> Tree [ctor] . op tree : Tree Int Tree -> Tree [ctor] . op nil : -> Seq . op __ : Seq Seq -> Seq [assoc id: nil ctor] . op __ : Pseq Pseq -> Pseq [assoc id: nil ctor] . vars M N : Int . vars S : Seq . vars F G : Tree . op downto : Nat Nat -> Seq . eq downto(M, N) = if M <= N then downto(M + 1,N) M else nil fi . op itree : Tree Int -> Tree . eq itree(ntree,N) = tree(ntree,N,ntree) . eq itree(tree(F,M,G),N) = if M >= N then tree(itree(F,N),M,G) else tree(F,M,itree(G,N)) fi . op seqtotree : Seq -> Tree . eq seqtotree(N) = tree(ntree,N,ntree) . eq seqtotree(N S) = itree(seqtotree(S),N) . endfm red seqtotree(downto(1,6)) . So far I have had no reports at all about Alpha84b. I would like to know if it breaks Full Maude in anyway. This new version also reports itself as 2.1.1 and I would like to release it as such in the next week or so unless anyone finds a show stopper. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha84b.2/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha84b.2/ Alpha release site authentication: User Name: maudeabuser Password: bughunter This release is a slightly patched version of Alpha84b.1 to fix a critical bug in the operator renaming reported by Paco: fmod FOO is sorts Bar Foo . subsorts Bar < Foo . op foo : Foo -> Foo . op foo : -> Foo . endfm fmod BAZ is inc FOO * (op foo : Bar -> Bar to bar). endfm show all . show modules . This new version also reports itself as 2.1.1 and I would like to release it as such in the next week or so unless anyone finds a show stopper. I will release a snapshot of my development tree (alpha84c) with experimental features in the near future. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha84b/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha84b/ Alpha release site authentication: User Name: maudeabuser Password: bughunter This version reports itself as Maude 2.1.1 and will be released as such if no show stoppers are found in the next week or so. It is intended as bug fix release. Currently there are no Darwin or FreeBSD binaries because of configuration issues on our Darwin and FreeBSD servers - hopefully this will be fixed by next week. Bug fixes ========== (1) A bug where upModule() generated the wrong meta-hooks for special operators of classes ACU_NumberOpSymbol and CUI_NumberOpSymbol. This also shows up with the "show all" command. Reported by Nathalie Sznajder and Paco. (2) A bug whether certain legal label names such as sort could not be parsed in label renamings. (3) The situation where two ad hoc overloaded operators have the same domain kinds but different ranges now causes a warning to be emitted as does the case where the arities differ but might look the same because of associativity: fmod FOO is sorts Foo Bar . op f : Foo -> Foo . op f : Foo -> Bar . endfm fmod BAR is sorts Foo Bar . op f : Foo Foo -> Foo [assoc] . op f : Foo Foo Foo -> Bar . endfm These cases are illegal but are handled correctly at the object level. They always break the metalevel because of ambiguity and this needs to be made clear in the manual. This inconsistancy was reported by Nathalie Sznajder and Olaf Owe. (4) There is now rudimentary checking of the consistancy for bubble hooks since users are expected write these themselves; Thanks to Fabricio Chalub for pointing out that the previous version crashes on (bad) examples from the manual. (5) A bug where an module with a missing identity could be imported, causing an internal error: fmod M is sort S . op __ : S S -> S [assoc id: ] . endfm fmod N is pr M . endfm Reported by Kazuhiro Ogata. Other changes ============== (1) Symmetric with set include FOO on/off . we now have set protect FOO on/off . and set extend FOO on/off . A module may only be auto-imported in one mode. Furthermore the prelude is changed so that BOOL is now auto-protected rather than auto-included. (2) Syntax for theories is supported. Currently this is mostly syntactic sugar except that the rules for importation that we agreed upon in Barcelona are now enforced by warnings and the module type of a summation is correctly calculated. Basically we have a lattice: th / \ fth mod \ / fmod where summation corresponds to join and a module may only import a module of less or equal type. Furthermore theories may only be imported via the including importation mode. Theories are reflected by constructors: fth_is_sorts_.____endfth and th_is_sorts_._____endth The are now extra subsorts: SModule FTheory STheory. Module is now used as the top sort rather than to represent system modules. This choice was made to avoid breaking stuff that expects Module to be the most general sort. The subsort relations are: subsorts FModule < SModule < Module . subsorts FTheory < STheory < Module . op [_] : Qid -> Module . is redefined so that it works with all kinds of modules without producing warnings. (3) The surface parser now supports overparsing - i.e. it deliberately parses more than the legal syntax in order to recover gracefully from common errors. Currently it recognizes rls/crls in fmods/fths, theories and modules terminated with the wrong keyword and the missing space before the period ending a statement. In order to make this possible there are minor restrictions on the legal syntax which should only affect pathological examples: < -> ~> are prohibited as sort names. Tokens ending in a period in the rhs of a eq/rl/mb or the condition of a ceq/crl/cmb cannot be followed by a keyword unless they are inside of parentheses; eg the following is not allowed: eq c = d. eq . It must be rewritten as eq c = (d. eq) . Steven 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= where 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 Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha85/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha85/ 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. Bug Fixes ========== (1) A bug where the up of a kind variable was incorrect; illustrated by the following code: fmod FOO is sort Foo . op a : -> [Foo] . op foo : [Foo] -> [Foo] . var X : [Foo] . eq foo(X) = a . endfm red in META-LEVEL : upEqs('FOO, false) . Bug reported by Manuel. (2) Operators notFound in fmod STRING and unbounded in fmod META-MODULE were not declared as constructors. Found by Joe Hendrix with his sufficient completeness checker. (3) A bug where FloatOpSymbol hooks were converted to NumberOpSymbol hooks by the ascent functions; for example: red in META-LEVEL : upOpDecls('FLOAT, false) . Bug reported by Joe Hendrix. (4) A bug where 0.0 ^ -1.0 evaluated to Infinity rather than being returned unevaluated as a [Float]. (5) A bug where module selectors such as getEqs() were not defined for theories. Bug reported by Carolyn. New features ============= (1) There are now builtin min() and max() functions in NAT, INT and RAT. Note that these operators are AC and so can be used with any number of arguments. In order to make the sort structure of max() associative it turned out to be necessary to a new sort PosRat to RAT. Otherwise consider the following triple of sorts Rat Rat NzNat Since the max of a Rat and a NzNat is necessarily a NzRat, grouping ((Rat Rat) NzNat) yields a NzRat while grouping (Rat (Rat NzNat)) yeilds only a Rat. Adding the sort PosRat fixes this, though all of the other declarations in RAT need to take PosRat into account. This feature was requested by Manuel. (2) The operator glbSorts() which computes the greatest lower bounds of a pair of sorts in a metamodule now works on types rather than sorts and is declared: op glbSorts : Module Type Type ~> TypeSet [special (...)] . TypeSets are added and become subsort polymorphic with SortSets and KindSets; this means that KindSets are now formed by the _;_ operator rather than the _&_ operator. Also the prec of _;_ is changed from the default (41) to 43 to allow TypeListSets (see below) to parse naturally. The empty constant is moved to the new sort EmptyTypeSet to avoid preregularity issues. The reason the return sort is a TypeSet is that the result will either be a Kind or a SortSet asn thus a supersort is needed. This extension was requested by Jose. (3) A new metalevel operator: op maximalAritySet : Module Qid TypeList Sort ~> TypeListSet [special (...)] . is added. For an operation in metamodule M specified by name F and domain D, maximalAritySet(M, F, D, S) computes the set of maximal arities (lists of types) that F could take and have a sort S' <= S. This might be the empty set if S is small or F is only defined at the kind level. The sort TypeListSet is added, which is a super sort of both TypeList (for single sets) and TypeSet (for arities of a unary operator). This feature was requested Jose. (4) A new metalevel operator: op metaSearchPath : Module Term Term Condition Qid Bound Nat ~> Trace? [special (...)] . where trace is a list of triples constructed by subsort TraceStep < Trace . op {_,_,_} : Term Type Rule -> TraceStep [ctor] . op nil : -> Trace [ctor] . op __ : Trace Trace -> Trace [ctor assoc id: nil format (d n d)] . metaSearchPath() is complementary to metaSeach() and carries out the same search, but instead of returning the final state and matching substitution returns the sequence of states and rules on a path starting with the reduced initial state and leading to (but not including) the final state. metaSearchPath() shares caching with metaSearch() so calling one after the other on the same arguments only performs a single search. This feature was requested by Carolyn. (5) There is a new command show path labels . that is like the show path command but only show labels rather than the full path. This feature was requested Merrill. (6) The show profile command now shows percentages as well as absolute rewrite counts. This extension was requested by Manuel. (7) There is a new command set clear rules on/off . Normally each rewrite or frewrite command and each loop mode invocation resets the rule state for each symbol. For most symbols the rule state consists of the next rule to be executed in a round robin scheme but for counter symbols the rule state consists of the next number to rewrite to. Setting "clear rules" to "off" means the rule state will not be reset between commands. This feature (in the special case of counters) was requested by Jose and Koushik Sen. Also there a number of changes under the hood: non-ANSI C++ code has cleaned up, allowing Maude to be compiled with the g++ 3.4.* series of compilers and the latest versions of Tecla, GMP and BuDDy have been used. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha85a/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha85a/ 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. Bug Fixes ========== (1) Operators op __ : TypeList TypeList -> TypeList [ditto] . op nil : -> EqCondition . op none : -> AttributeSet . were not declared as constructors. Found by Joe Hendrix with his sufficient completeness checker. (2) The declaration op _&_ : Nat Int -> Nat [...] . was missing from fmod INT causing certain integer expressions to have a larger sort than necessary. New features ============= (1) Operator declarations may now take the metadata attribute that was previously reserved for mbs/eqs/rls. Note that like ctor, metadata is attached to the declaration and not the operator. Thus two subsorted overloaded declarations may have different metadata attributes, a metadata attribute is not copied by the ditto attribute and a declaration may have a metadata attribute as well as a ditto attribute: fmod FOO is sorts Foo Bar . subsort Foo < Bar . op f : Foo -> Foo [memo metadata "f on Foos"] . op f : Bar -> Bar [ditto metadata "f on Bars"] . endfm The metadata attribute is copied unchanged by importation and renaming; it may not be explicity mentioned in a renaming. It has no effect on semantics except that it is visible in meta operator declarations (using the existing metadata operator) generated by ascent functions. This feature was requested by Carolyn. (2) The is now alpha quality support for rewriting with external objects and an implementation of sockets as the first such external objects. Configurations that want to communicate with external objects must contain at least one 'portal' where op <> : -> Portal [ctor] . now appears in mod CONFIGURATION . Rewriting with external objects is started by the command erewrite (or erew) which is like frew except is allows messages to be exchanged with external objects that do not reside in the configuration. Currently erewrite has some serious limitations: (a) Limit / gas parameters, and continuation do not work (b) Rewrites that involve messages entering or leaving the configuration do not show up in tracing, profiling or rewrite counts. (c) Bad interactions with break points and debugger. (d) Potential race condition with ^C. Note that erewrite may not terminate just because there are no more rewrite possible - if there are requests made to external objects that have not yet been fulfilled because of waiting for external events from the operating system, the Maude interpreter will suspend until at least one of those events occurs at which time rewriting will resume. While the interpreter is suspended, the erewrite may be aborted with ^C. External objects created by an erewrite do not survive to the next erewrite. If a message to an external object is malformed or inappropriate or the external object is not ready for it, it just stays in the configuration for future acceptance or for debugging purposes. The first example of external objects is sockets, which are accessed using the messages declared in socket.maude : mod SOCKET is pr STRING . inc CONFIGURATION . op socket : Nat -> Oid [ctor] . op createClientTcpSocket : Oid Oid String Nat -> Msg [ctor msg format (b o)] . op createServerTcpSocket : Oid Oid Nat Nat -> Msg [ctor msg format (b o)] . op createdSocket : Oid Oid Oid -> Msg [ctor msg format (m o)] . op acceptClient : Oid Oid -> Msg [ctor msg format (b o)] . op acceptedClient : Oid Oid String Oid -> Msg [ctor msg format (m o)] . op send : Oid Oid String -> Msg [ctor msg format (b o)] . op sent : Oid Oid -> Msg [ctor msg format (m o)] . op receive : Oid Oid -> Msg [ctor msg format (b o)] . op received : Oid Oid String -> Msg [ctor msg format (m o)] . op closeSocket : Oid Oid -> Msg [ctor msg format (b o)] . op closedSocket : Oid Oid String -> Msg [ctor msg format (m o)] . op socketError : Oid Oid String -> Msg [ctor msg format (r o)] . op socketManager : -> Oid [special (...)] . endm Currently only IPv4 TCP sockets are supported - other protocol families and socket types may be added in the future. The external object named by socketManager is a factory for socket objects. To create a client socket, you send socketManager a createClientTcpSocket(socketManager, ME, ADDRESS, PORT) where ME is the name of the object the reply should be sent to, ADDRESS is the name of the server you want to connect to; say "www.google.com", and PORT is the port you want to connect to; say 80 for HTTP connections. You may also specify the name of the server as an IPv4 dotted address or as "localhost" for same machine as Maude is running on. The reply will either be: createdSocket(ME, socketManager, NEW-SOCKET-NAME) or socketError(ME, socketManager, REASON) where NEW-SOCKET-NAME is the name of the newly created socket and REASON is the operating system's terse explanation of what went wrong. You can then send data to the server with: send(NEW-SOCKET-NAME, ME, DATA) which elicits either: sent(ME, socketManager) or closedSocket(ME, socketManager, REASON) Notice that all errors on a client socket are handled by closing the socket. Similarly you can receive data from the server with: receive(NEW-SOCKET-NAME, ME) which elicits either: received(ME, socketManager. DATA) or closedSocket(ME, socketManager, REASON) When you are done with the socket you can close it with closeSocket(NEW-SOCKET-NAME, ME) closedSocket(ME, socketManager, "") Once a socket has be closed, it name may be reused so sending messages to a closed socket can cause confusion and should be avoided. Note that TCP does not preserve message boundries, so sending "ONE" and "TWO" might be received as "ON" and "ETWO". Delimiting message boundries is the responsibility of the next higher level protocol, such as HTTP. The file webClient.maude contains an updated version of the 5 rule HTTP/1.0 client from the "Towards Maude 2.0" paper that is now executable. To have communication between 2 Maude interpreter instances, one of them must take the server role and offer a service on a given port. Generally ports below 1024 are protected. You cannot in general assume that a given port is available for use. To create a server socket, you send socketManager a createServerTcpSocket(socketManager, ME, PORT, BACKLOG) where PORT is the PORT number and BACKLOG is the number of queue requests for connection that you will allow (5 seems to be a good choice). The response is createdSocket(ME, socketManager, SERVER-SOCKET-NAME) or socketError(ME, socketManager, REASON) Here SERVER-SOCKET-NAME refers to a server socket. The only thing you can do with a server socket (other than close it) is accept clients: acceptClient(SERVER-SOCKET-NAME, ME) which elicits acceptedClient(ME, SERVER-SOCKET-NAME, ADDRESS, NEW-SOCKET-NAME) or socketError(ME, socketManager, REASON) Here ADDRESS is the originating address of the client and NEW-SOCKET-NAME is the name of the socket you use to communicate with that client. This new socket behaves just like a client socket for sending and receiving. Note the an error in accepting a client does not close the server socket. You can always reuse the server socket to accept new clients until you explicitly close it. The files factorialServer.maude and factorialClient.maude illustrate a very naive 2 way communication between to Maude interpreter instances. The issues of port availability and message boundries are deliberately ignored (and thus if you are unluck this example could fail) for the sake of illustration. Almost everything in the socket implementation is done in a non-blocking way; so for example if you try to open a connection to some webserver and that webserver takes 5 minutes to respond, other rewriting and transactions happen in the meanwhile as part of the same erewrite. The one exception is DNS resolution which is done as part of the createClientTcpSocket() message handling and which cannot be nonblocking without special tricks. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha85/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha85/ 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. Bug Fixes ========== (1) A bug where the up of a kind variable was incorrect; illustrated by the following code: fmod FOO is sort Foo . op a : -> [Foo] . op foo : [Foo] -> [Foo] . var X : [Foo] . eq foo(X) = a . endfm red in META-LEVEL : upEqs('FOO, false) . Bug reported by Manuel. (2) Operators notFound in fmod STRING and unbounded in fmod META-MODULE were not declared as constructors. Found by Joe Hendrix with his sufficient completeness checker. (3) A bug where FloatOpSymbol hooks were converted to NumberOpSymbol hooks by the ascent functions; for example: red in META-LEVEL : upOpDecls('FLOAT, false) . Bug reported by Joe Hendrix. (4) A bug where 0.0 ^ -1.0 evaluated to Infinity rather than being returned unevaluated as a [Float]. (5) A bug where module selectors such as getEqs() were not defined for theories. Bug reported by Carolyn. New features ============= (1) There are now builtin min() and max() functions in NAT, INT and RAT. Note that these operators are AC and so can be used with any number of arguments. In order to make the sort structure of max() associative it turned out to be necessary to a new sort PosRat to RAT. Otherwise consider the following triple of sorts Rat Rat NzNat Since the max of a Rat and a NzNat is necessarily a NzRat, grouping ((Rat Rat) NzNat) yields a NzRat while grouping (Rat (Rat NzNat)) yeilds only a Rat. Adding the sort PosRat fixes this, though all of the other declarations in RAT need to take PosRat into account. This feature was requested by Manuel. (2) The operator glbSorts() which computes the greatest lower bounds of a pair of sorts in a metamodule now works on types rather than sorts and is declared: op glbSorts : Module Type Type ~> TypeSet [special (...)] . TypeSets are added and become subsort polymorphic with SortSets and KindSets; this means that KindSets are now formed by the _;_ operator rather than the _&_ operator. Also the prec of _;_ is changed from the default (41) to 43 to allow TypeListSets (see below) to parse naturally. The empty constant is moved to the new sort EmptyTypeSet to avoid preregularity issues. The reason the return sort is a TypeSet is that the result will either be a Kind or a SortSet asn thus a supersort is needed. This extension was requested by Jose. (3) A new metalevel operator: op maximalAritySet : Module Qid TypeList Sort ~> TypeListSet [special (...)] . is added. For an operation in metamodule M specified by name F and domain D, maximalAritySet(M, F, D, S) computes the set of maximal arities (lists of types) that F could take and have a sort S' <= S. This might be the empty set if S is small or F is only defined at the kind level. The sort TypeListSet is added, which is a super sort of both TypeList (for single sets) and TypeSet (for arities of a unary operator). This feature was requested Jose. (4) A new metalevel operator: op metaSearchPath : Module Term Term Condition Qid Bound Nat ~> Trace? [special (...)] . where trace is a list of triples constructed by subsort TraceStep < Trace . op {_,_,_} : Term Type Rule -> TraceStep [ctor] . op nil : -> Trace [ctor] . op __ : Trace Trace -> Trace [ctor assoc id: nil format (d n d)] . metaSearchPath() is complementary to metaSeach() and carries out the same search, but instead of returning the final state and matching substitution returns the sequence of states and rules on a path starting with the reduced initial state and leading to (but not including) the final state. metaSearchPath() shares caching with metaSearch() so calling one after the other on the same arguments only performs a single search. This feature was requested by Carolyn. (5) There is a new command show path labels . that is like the show path command but only show labels rather than the full path. This feature was requested Merrill. (6) The show profile command now shows percentages as well as absolute rewrite counts. This extension was requested by Manuel. (7) There is a new command set clear rules on/off . Normally each rewrite or frewrite command and each loop mode invocation resets the rule state for each symbol. For most symbols the rule state consists of the next rule to be executed in a round robin scheme but for counter symbols the rule state consists of the next number to rewrite to. Setting "clear rules" to "off" means the rule state will not be reset between commands. This feature (in the special case of counters) was requested by Jose and Koushik Sen. Also there a number of changes under the hood: non-ANSI C++ code has cleaned up, allowing Maude to be compiled with the g++ 3.4.* series of compilers and the latest versions of Tecla, GMP and BuDDy have been used. Steven Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha85a/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha85a/ 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. Bug Fixes ========== (1) Operators op __ : TypeList TypeList -> TypeList [ditto] . op nil : -> EqCondition . op none : -> AttributeSet . were not declared as constructors. Found by Joe Hendrix with his sufficient completeness checker. (2) The declaration op _&_ : Nat Int -> Nat [...] . was missing from fmod INT causing certain integer expressions to have a larger sort than necessary. New features ============= (1) Operator declarations may now take the metadata attribute that was previously reserved for mbs/eqs/rls. Note that like ctor, metadata is attached to the declaration and not the operator. Thus two subsorted overloaded declarations may have different metadata attributes, a metadata attribute is not copied by the ditto attribute and a declaration may have a metadata attribute as well as a ditto attribute: fmod FOO is sorts Foo Bar . subsort Foo < Bar . op f : Foo -> Foo [memo metadata "f on Foos"] . op f : Bar -> Bar [ditto metadata "f on Bars"] . endfm The metadata attribute is copied unchanged by importation and renaming; it may not be explicity mentioned in a renaming. It has no effect on semantics except that it is visible in meta operator declarations (using the existing metadata operator) generated by ascent functions. This feature was requested by Carolyn. (2) The is now alpha quality support for rewriting with external objects and an implementation of sockets as the first such external objects. Configurations that want to communicate with external objects must contain at least one 'portal' where op <> : -> Portal [ctor] . now appears in mod CONFIGURATION . Rewriting with external objects is started by the command erewrite (or erew) which is like frew except is allows messages to be exchanged with external objects that do not reside in the configuration. Currently erewrite has some serious limitations: (a) Limit / gas parameters, and continuation do not work (b) Rewrites that involve messages entering or leaving the configuration do not show up in tracing, profiling or rewrite counts. (c) Bad interactions with break points and debugger. (d) Potential race condition with ^C. Note that erewrite may not terminate just because there are no more rewrite possible - if there are requests made to external objects that have not yet been fulfilled because of waiting for external events from the operating system, the Maude interpreter will suspend until at least one of those events occurs at which time rewriting will resume. While the interpreter is suspended, the erewrite may be aborted with ^C. External objects created by an erewrite do not survive to the next erewrite. If a message to an external object is malformed or inappropriate or the external object is not ready for it, it just stays in the configuration for future acceptance or for debugging purposes. The first example of external objects is sockets, which are accessed using the messages declared in socket.maude : mod SOCKET is pr STRING . inc CONFIGURATION . op socket : Nat -> Oid [ctor] . op createClientTcpSocket : Oid Oid String Nat -> Msg [ctor msg format (b o)] . op createServerTcpSocket : Oid Oid Nat Nat -> Msg [ctor msg format (b o)] . op createdSocket : Oid Oid Oid -> Msg [ctor msg format (m o)] . op acceptClient : Oid Oid -> Msg [ctor msg format (b o)] . op acceptedClient : Oid Oid String Oid -> Msg [ctor msg format (m o)] . op send : Oid Oid String -> Msg [ctor msg format (b o)] . op sent : Oid Oid -> Msg [ctor msg format (m o)] . op receive : Oid Oid -> Msg [ctor msg format (b o)] . op received : Oid Oid String -> Msg [ctor msg format (m o)] . op closeSocket : Oid Oid -> Msg [ctor msg format (b o)] . op closedSocket : Oid Oid String -> Msg [ctor msg format (m o)] . op socketError : Oid Oid String -> Msg [ctor msg format (r o)] . op socketManager : -> Oid [special (...)] . endm Currently only IPv4 TCP sockets are supported - other protocol families and socket types may be added in the future. The external object named by socketManager is a factory for socket objects. To create a client socket, you send socketManager a createClientTcpSocket(socketManager, ME, ADDRESS, PORT) where ME is the name of the object the reply should be sent to, ADDRESS is the name of the server you want to connect to; say "www.google.com", and PORT is the port you want to connect to; say 80 for HTTP connections. You may also specify the name of the server as an IPv4 dotted address or as "localhost" for same machine as Maude is running on. The reply will either be: createdSocket(ME, socketManager, NEW-SOCKET-NAME) or socketError(ME, socketManager, REASON) where NEW-SOCKET-NAME is the name of the newly created socket and REASON is the operating system's terse explanation of what went wrong. You can then send data to the server with: send(NEW-SOCKET-NAME, ME, DATA) which elicits either: sent(ME, socketManager) or closedSocket(ME, socketManager, REASON) Notice that all errors on a client socket are handled by closing the socket. Similarly you can receive data from the server with: receive(NEW-SOCKET-NAME, ME) which elicits either: received(ME, socketManager. DATA) or closedSocket(ME, socketManager, REASON) When you are done with the socket you can close it with closeSocket(NEW-SOCKET-NAME, ME) closedSocket(ME, socketManager, "") Once a socket has be closed, it name may be reused so sending messages to a closed socket can cause confusion and should be avoided. Note that TCP does not preserve message boundries, so sending "ONE" and "TWO" might be received as "ON" and "ETWO". Delimiting message boundries is the responsibility of the next higher level protocol, such as HTTP. The file webClient.maude contains an updated version of the 5 rule HTTP/1.0 client from the "Towards Maude 2.0" paper that is now executable. To have communication between 2 Maude interpreter instances, one of them must take the server role and offer a service on a given port. Generally ports below 1024 are protected. You cannot in general assume that a given port is available for use. To create a server socket, you send socketManager a createServerTcpSocket(socketManager, ME, PORT, BACKLOG) where PORT is the PORT number and BACKLOG is the number of queue requests for connection that you will allow (5 seems to be a good choice). The response is createdSocket(ME, socketManager, SERVER-SOCKET-NAME) or socketError(ME, socketManager, REASON) Here SERVER-SOCKET-NAME refers to a server socket. The only thing you can do with a server socket (other than close it) is accept clients: acceptClient(SERVER-SOCKET-NAME, ME) which elicits acceptedClient(ME, SERVER-SOCKET-NAME, ADDRESS, NEW-SOCKET-NAME) or socketError(ME, socketManager, REASON) Here ADDRESS is the originating address of the client and NEW-SOCKET-NAME is the name of the socket you use to communicate with that client. This new socket behaves just like a client socket for sending and receiving. Note the an error in accepting a client does not close the server socket. You can always reuse the server socket to accept new clients until you explicitly close it. The files factorialServer.maude and factorialClient.maude illustrate a very naive 2 way communication between to Maude interpreter instances. The issues of port availability and message boundries are deliberately ignored (and thus if you are unluck this example could fail) for the sake of illustration. Almost everything in the socket implementation is done in a non-blocking way; so for example if you try to open a connection to some webserver and that webserver takes 5 minutes to respond, other rewriting and transactions happen in the meanwhile as part of the same erewrite. The one exception is DNS resolution which is done as part of the createClientTcpSocket() message handling and which cannot be nonblocking without special tricks. Steven