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