The debugger

There are three ways to get into the Maude debugger:

• a control-C interrupt during rewriting,
• prefixing a command with the keyword debug, and
• hitting a break point.

Break points are set with the command

  break select foo bar ([_,_]) .

where the names refer to operators or statement (equation, membership or rule) labels in a way that is completely analogous to the trace select command described in Section 13.1.1. Break points are enabled with the command

  set break on .

On entering the debugger, the prompt changes to $\texttt{Debug(}n\texttt{)>}$ where $n$ is the debug level, that is, 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.

We illustrate these commands using the bank accounts example presented in Section 8.1 (assuming it is in the file bank-account-test.maude).

We first use the debug command to activate the debugger from the begining of a rewrite. Note the use of the where, step, and resume commands.

  Maude> load bank-account-test.maude
  Maude> debug rew bankConf .
  rewrite in BANK-ACCOUNT-TEST : bankConf .
  Debug(1)> where .
  Current term is:
  bankConf
  which arose while executing a top level command.
  Debug(1)> step .
  *********** equation
  eq bankConf = (((((< A-003 : Account | bal : 1250 > from A-003 to
      A-002 transfer 300) debit(A-002, 400)) < A-002 : Account | bal :
      250 >) debit(A-001, 150)) debit(A-001, 200)) < A-001 : Account |
      bal : 300 > .
  empty substitution
  bankConf
  --->
  (((((< A-003 : Account | bal : 1250 > from A-003 to A-002 transfer
      300) debit(A-002, 400)) < A-002 : Account | bal : 250 >) debit(
      A-001, 150)) debit(A-001, 200)) < A-001 : Account | bal : 300 >
  Debug(1)> where .
  Current term is:
  debit(A-001, 150) debit(A-001, 200) debit(A-002, 400) < A-001 :
      Account | bal : 300 > < A-002 : Account | bal : 250 > < A-003 :
      Account | bal : 1250 > from A-003 to A-002 transfer 300
  which arose while executing a top level command.
  Debug(1)> resume .
  rewrites: 13 in 2ms cpu (85160ms real) (6500 rewrites/second)
  result Configuration: debit(A-001, 200) < A-001 : Account | bal :
      150 > < A-002 : Account | bal : 150 > < A-003 : Account | bal :
      950 >

As said above, we can also enter into the debugger by reaching a break point or typing control-c. In the following example we set a break point on the debit rule, take a step, and then abort the rewrite process.

  Maude> set break on .
  Maude> break select debit .
  Maude> rew bankConf .
  rewrite in BANK-ACCOUNT-TEST : bankConf .
  break on labeled rule:
  crl debit(A:Oid, M:Nat) < A:Oid : Account | bal : N:Nat > => < A:Oid
      : Account | bal : (N:Nat - M:Nat) > if N:Nat >= M:Nat = true [
      label debit] .
  Debug(1)> where .
  Current term is:
  debit(A-001, 150) debit(A-001, 200) debit(A-002, 400) < A-001 :
      Account | bal : 300 > < A-002 : Account | bal : 250 > < A-003 :
      Account | bal : 1250 > from A-003 to A-002 transfer 300
  which arose while executing a top level command.
  Debug(1)> step .
  *********** trial #1
  crl debit(A:Oid, M:Nat) < A:Oid : Account | bal : N:Nat > => <
      A:Oid : Account | bal : (N:Nat - M:Nat) > if N:Nat >= M:Nat =
      true [label debit] .
  A:Oid --> A-001
  M:Nat --> 150
  N:Nat --> 300
  *********** solving condition fragment
  N:Nat >= M:Nat = true
  Debug(1)> where .
  Current term is:
  300 >= 150
  which arose while checking a condition during the evaluation of:
  debit(A-001, 150) debit(A-001, 200) debit(A-002, 400) < A-001 :
    Account | bal : 300 > < A-002 : Account | bal : 250 > < A-003 :
    Account | bal : 1250 > from A-003 to A-002 transfer 300
  which arose while executing a top level command.
  Debug(1)> abort .
  Maude>

Our last example illustrates the re-entering nature of the debugger. As said above, any command can be used during the debugging process, allowing, for example, starting an execution while debugging another one. We execute a debug rew command, entering the debugger, where we set a break point on the transfer rule. Notice the Debug(2)> prompt. Notice also how after getting out of the inner debugger the break point is still active.

  Maude> debug rew bankConf .
  rewrite in BANK-ACCOUNT-TEST : bankConf .
  Debug(1)> step .
  *********** equation
  eq bankConf = (((((< A-003 : Account | bal : 1250 > from A-003 to
      A-002 transfer 300) debit(A-002, 400)) < A-002 : Account | bal
      : 250 >) debit(A-001, 150)) debit(A-001, 200)) < A-001 : Account
      | bal : 300 > .
  empty substitution
  bankConf
  --->
  (((((< A-003 : Account | bal : 1250 > from A-003 to A-002 transfer
      300) debit(A-002, 400)) < A-002 : Account | bal : 250 >) debit(
      A-001, 150)) debit(A-001, 200)) < A-001 : Account | bal : 300 >
  Debug(1)> set break on .
  Debug(1)> break select transfer .
  Debug(1)> rew bankConf .
  rewrite in BANK-ACCOUNT-TEST : bankConf .
  break on labeled rule:
  crl < A:Oid : Account | bal : N:Nat > < B:Oid : Account | bal :
      N':Nat > from A:Oid to B:Oid transfer M:Nat => < A:Oid : Account
      | bal : (N:Nat - M:Nat) > < B:Oid : Account | bal : (M:Nat +
      N':Nat) > if N:Nat >= M:Nat = true [label transfer] .
  Debug(2)> where .
  Current term is:
  debit(A-001, 200) debit(A-002, 400) < A-001 : Account | bal : 150 >
      < A-002 : Account | bal : 250 > < A-003 : Account | bal : 1250 >
      from A-003 to A-002 transfer 300
  which arose while executing a top level command.
  Debug(2)> resume .
  break on labeled rule:
  crl < A:Oid : Account | bal : N:Nat > < B:Oid : Account | bal :
    N':Nat > from A:Oid to B:Oid transfer M:Nat => < A:Oid : Account |
    bal : (N:Nat - M:Nat) > < B:Oid : Account | bal : (M:Nat + N':Nat)
    > if N:Nat >= M:Nat = true [label transfer] .
  Debug(2)> abort .
  Debug(1)> resume .
  break on labeled rule:
  crl < A:Oid : Account | bal : N:Nat > < B:Oid : Account | bal :
      N':Nat > from A:Oid to B:Oid transfer M:Nat => < A:Oid : Account
      | bal : (N:Nat - M:Nat) > < B:Oid : Account | bal : (M:Nat +
      N':Nat) > if N:Nat >= M:Nat = true [label transfer] .
  Debug(1)> set break off .
  Debug(1)> resume .
  rewrites: 13 in 4ms cpu (63920ms real) (2600 rewrites/second)
  result Configuration: debit(A-001, 200) < A-001 : Account | bal :
      150 > < A-002 : Account | bal : 150 > < A-003 : Account | bal :
      950 >