Maude Manual -- 2.9.2 Debugging Core Maude Specifications

Go backward to 2.9.1 Command Line Options
Go up to 2.9 System Issues and Debugging
Go forward to 2.9.3 User Facilities Not Yet Implemented

2.9.2 Debugging Core Maude Specifications

There are two approaches to debugging Core Maude specifications. The most general technique is to turn tracing on with the command

  set trace on .

and capture a log of the trace using script or xterm logging. This can then be studied using a text editor. Since the trace is usually voluminous, there are a number of trace options to control just what is traced. One of the more useful is selective tracing:

  set trace select on .
  trace select foo bar ([_,_]) .

This will cause only rewrites where the redex is headed by operators with the selected names to be traced. Note that these operators need not be in existence at the time the trace select command is executed; thus it is possible to select operators that will only be created at runtime via the metalevel.

The other approach is to use the Core Maude debugger. When reductions are happening and a control-C interrupt is received, the debugger is automatically entered. The prompt changes to Debug(n)> where n is the debug level; or the number of times the debugger has been re-entered (it is fully re-entrant). All top level commands can be executed from the debugger, along with four commands that are special to the debugger:

where .: Prints out the stack of pending rewrites, explaining how each one arose.
step .: Executes the next rewrite with tracing turned on.
resume .: Exits the debugger and continues with the current rewriting task.
abort .: Exits the debugger and abandons the current rewriting task.

Since it is sometimes useful to enter the debugger just before the first rewrite takes place, the reduce, rewrite and continue commands can be prefixed by the debug keyword to accomplish this. For example:

  debug rewrite [8] in MY-SPEC : init-symbol .