The tracing facilities allow us to follow the execution of our specifications, that is, the sequence of rewrites or equational simplification reductions that take place. Tracing is turned on with the command
set trace on .
A log of the trace can be captured 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. We refer to Section 16.5 for a complete list of tracing commands and options.
One of the most useful options is selective tracing:
set trace select on . trace select foo bar ([_,_]) .
This will cause only rewrites where the statement (equation, membership or rule)
is labeled with a selected name or the redex is headed by operators with a selected
name to be traced. In the above example, suppose foo and bar are
rule labels, [_,_] is an operator name, and foo is also an operator
name. Then, rewrites using the rules labeled by foo or bar will be
reported, as will also rewrites with redex whose top-level operator is either
foo or [_,_]. Note that these labels or operators need not be in
existence at the time the trace select command is executed; thus it is
possible to select statements and operators that will only be created at runtime
via the metalevel.
A useful option for metaprogramming is
trace exclude FOO BAR .
This will exclude the named modules from being traced and thus allows one to selectively avoid tracing the chosen object and/or metalevel modules. This is particularly useful when using Full Maude to localize the tracing to the ``object modules'' being executed and not to the FULL-MAUDE module itself (see Chapter 14). After loading Full Maude, its specification is excluded from the tracing, which allows us to trace Full Maude specifications as Core Maude specifications.
As we have mentioned, there are different commands that may help us in the control of the trace of the execution at hand. If the number of rewrites is small, we may use the whole trace to check the behavior of our specification. However, the number of rewrites is usually big, and considering the whole trace is completely impossible. The different options may help us, for example, to focus on a particular rule or set of rules, exclude certain modules from the trace, or not tracing the rewrites happening in the conditions.
Let us illustrate some of these commands to trace the bank accounts example presented in Section 8.1. To see the trace we just need to set the trace on. After it, the trace of any rewrite command will be given, according to the active options. By default, the application of every equation, membership axiom, and rule will be printed, showing the corresponding substitution, the current whole term, and the subterm on which the axiom is being applied before and after its application. To get a flavor of the information we get, let us rewrite the bankConf term with a bound of 1.
Maude> set trace on .
Maude> rew [1] bankConf .
rewrite [1] in BANK-ACCOUNT-TEST : bankConf .
*********** 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 >
*********** 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
*********** equation
(built-in equation for symbol _>=_)
300 >= 150
--->
true
*********** success for condition fragment
N:Nat >= M:Nat = true
A:Oid --> A-001
M:Nat --> 150
N:Nat --> 300
*********** success #1
*********** 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] .
A:Oid --> A-001
M:Nat --> 150
N:Nat --> 300
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
--->
(debit(A-001, 200) debit(A-002, 400) < A-002 : Account | bal : 250 >
< A-003 : Account | bal : 1250 > from A-003 to A-002 transfer
300) < A-001 : Account | bal : (300 - 150) >
*********** equation
(built-in equation for symbol _-_)
300 - 150
--->
150
rewrites: 4 in 1ms cpu (1ms real) (4000 rewrites/second)
result Configuration: 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
Notice that, even though the bound for the rewrite command is one, there are four rewrites. Recall that the bound only concerns rule application. In this trace we see how three equations--two of them built-in--are also applied. In addition to the statement used in each rewriting step, the trace shows the matching substitution and the whole term, before and after the application of the statement. Notice also the information concerning the evaluation of conditions. We can see that, although there is a match with the debit rule, this rule is not applied until the success of its condition has been checked.
Suppose we are mainly concerned with the application of rules. In this case
we may think that there is too much ``noise'' due to the application of
equations. We may request hiding the information about the application
of equations with the command set trace eq off. Then the trace
for rewriting the same bankConf term with the same
bound of 1 is as follows:
Maude> set trace eq off .
Maude> rew [1] bankConf .
rewrite [1] in BANK-ACCOUNT-TEST : bankConf .
*********** 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
*********** success for condition fragment
N:Nat >= M:Nat = true
A:Oid --> A-001
M:Nat --> 150
N:Nat --> 300
*********** success #1
*********** 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] .
A:Oid --> A-001
M:Nat --> 150
N:Nat --> 300
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
--->
(debit(A-001, 200) debit(A-002, 400) < A-002 : Account | bal : 250 >
< A-003 : Account | bal : 1250 > from A-003 to A-002 transfer
300) < A-001 : Account | bal : (300 - 150) >
rewrites: 4 in 1ms cpu (0ms real) (4000 rewrites/second)
result Configuration: 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
The selection of the concrete operator or statement label to trace may
also be a good alternative when looking for something specific. Suppose
that we are suspicious of a particular rule,
say transfer. We may get the applications of such a rule for
the unbounded rewrite of the bankConf term by using the
trace select command as follows.
Maude> set trace select on .
Maude> trace select transfer .
Maude> rew bankConf .
rewrite in BANK-ACCOUNT-TEST : bankConf .
*********** trial #1
crl < A:Oid : Account | bal : N:Nat > < B:Oid : Account | bal :
N':Nat > fromA: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] .
A:Oid --> A-003
N:Nat --> 1250
B:Oid --> A-002
N':Nat --> 250
M:Nat --> 300
*********** solving condition fragment
N:Nat >= M:Nat = true
*********** success for condition fragment
N:Nat >= M:Nat = true
A:Oid --> A-003
N:Nat --> 1250
B:Oid --> A-002
N':Nat --> 250
M:Nat --> 300
*********** success #1
*********** 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] .
A:Oid --> A-003
N:Nat --> 1250
B:Oid --> A-002
N':Nat --> 250
M:Nat --> 300
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
--->
(debit(A-001, 200) debit(A-002, 400) < A-001 : Account | bal : 150 >)
< A-003 : Account | bal : (1250 - 300) > < A-002 : Account |
bal : (300 + 250) >
rewrites: 13 in 1ms cpu (1ms real) (13000 rewrites/second)
result Configuration: debit(A-001, 200) < A-001 : Account |
bal : 150 > < A-002 : Account | bal : 150 > < A-003 : Account |
bal : 950 >
We may also hide some of the information being shown. For example, we may
get the same trace without the substitutions being shown with the
set trace substitution off command.
Maude> set trace substitution off .
Maude> rew bankConf .
rewrite in BANK-ACCOUNT-TEST : bankConf .
*********** trial #1
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] .
*********** solving condition fragment
N:Nat >= M:Nat = true
*********** success for condition fragment
N:Nat >= M:Nat = true
*********** success #1
*********** 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] .
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
--->
(debit(A-001, 200) debit(A-002, 400) < A-001 : Account | bal : 150 >)
< A-003 : Account | bal : (1250 - 300) > < A-002 : Account |
bal : (300 + 250) >
rewrites: 13 in 0ms cpu (0ms real) (~ rewrites/second)
result Configuration: debit(A-001, 200) < A-001 : Account |
bal : 150 > < A-002 : Account | bal : 150 > < A-003 : Account |
bal : 950 >
Let us consider now a different example, namely, the PATH module presented in Sections 3.5 and 4.3. We use it here to illustrate the trace given for membership axioms and for conditional axioms with multiple fragments. We recall first the conditional membership axiom defining multi-edge paths and the conditional equation defining the associativity of path concatenation.
var E : Edge .
vars P Q R S : Path .
cmb E ; P : Path if target(E) = source(P) .
ceq (P ; Q) ; R = P ; (Q ; R)
if target(P) = source(Q) /\ target(Q) = source(R) .
Now we request the trace for the reduction of the term
length((b ; c) ; d).
The information shown is particularly illustrative for understanding
the way in which the membership axioms are used and the way conditions
are evaluated. Note that the equation expressing the associativity of
path concatenation has two fragments, one of which is evaluated after the
other. In case the condition of a matching equation fails another equation
is attempted; furthermore, equations with matching conditions
have unbounded variables initially.
Since the full trace is more than six pages long, we use the set trace condition off command, so that the evaluation of the conditions is omitted.
Maude> set trace on .
Maude> set trace condition off .
Maude> red length((b ; c) ; d) .
reduce in PATH : length((b ; c) ; d) .
*********** trial #1
cmb E ; P : Path if target(E) = source(P) .
E --> b
P --> c
*********** solving condition fragment
target(E) = source(P)
*********** success for condition fragment
target(E) = source(P)
E --> b
P --> c
*********** success #1
*********** membership axiom
cmb E ; P : Path if target(E) = source(P) .
E --> b
P --> c
[Path]: b ; c becomes Path
*********** trial #2
ceq (P ; Q) ; R = P ; (Q ; R)
if target(P) = source(Q) /\ target(Q) = source(R) .
P --> b
Q --> c
R --> d
*********** solving condition fragment
target(P) = source(Q)
*********** success for condition fragment
target(P) = source(Q)
P --> b
Q --> c
R --> d
*********** solving condition fragment
target(Q) = source(R)
*********** success for condition fragment
target(Q) = source(R)
P --> b
Q --> c
R --> d
*********** success #2
*********** equation
ceq (P ; Q) ; R = P ; (Q ; R)
if target(P) = source(Q) /\ target(Q) = source(R) .
P --> b
Q --> c
R --> d
(b ; c) ; d
--->
b ; (c ; d)
*********** trial #3
cmb E ; P : Path if target(E) = source(P) .
E --> c
P --> d
*********** solving condition fragment
target(E) = source(P)
*********** success for condition fragment
target(E) = source(P)
E --> c
P --> d
*********** success #3
*********** membership axiom
cmb E ; P : Path if target(E) = source(P) .
E --> c
P --> d
[Path]: c ; d becomes Path
*********** trial #4
cmb E ; P : Path if target(E) = source(P) .
E --> b
P --> c ; d
*********** solving condition fragment
target(E) = source(P)
*********** success for condition fragment
target(E) = source(P)
E --> b
P --> c ; d
*********** success #4
*********** membership axiom
cmb E ; P : Path if target(E) = source(P) .
E --> b
P --> c ; d
[Path]: b ; (c ; d) becomes Path
*********** trial #5
ceq length(E ; P) = 1 + length(P) if E ; P : Path .
E --> b
P --> c ; d
*********** solving condition fragment
E ; P : Path
*********** success for condition fragment
E ; P : Path
E --> b
P --> c ; d
*********** success #5
*********** equation
ceq length(E ; P) = 1 + length(P) if E ; P : Path .
E --> b
P --> c ; d
length(b ; (c ; d))
--->
1 + length(c ; d)
*********** trial #6
ceq length(E ; P) = 1 + length(P) if E ; P : Path .
E --> c
P --> d
*********** solving condition fragment
E ; P : Path
*********** success for condition fragment
E ; P : Path
E --> c
P --> d
*********** success #6
*********** equation
ceq length(E ; P) = 1 + length(P) if E ; P : Path .
E --> c
P --> d
length(c ; d)
--->
1 + length(d)
*********** equation
eq length(E) = 1 .
E --> d
length(d)
--->
1
*********** equation
(built-in equation for symbol _+_)
1 + 1
--->
2
*********** equation
(built-in equation for symbol _+_)
1 + 2
--->
3
rewrites: 20 in 2ms cpu (1ms real) (10000 rewrites/second)
result NzNat: 3
But the trace is too long to observe what we were interested in. Suppose we just wanted to check a possible mistake in the specification of the length function. We may select it for filtering the equations defining it.
Maude> set trace select on . Maude> trace select length . Maude> red length((b ; c) ; d) . reduce in PATH : length((b ; c) ; d) . *********** trial #1 ceq length(E ; P) = 1 + length(P) if E ; P : Path . E --> b P --> c ; d *********** solving condition fragment E ; P : Path *********** success for condition fragment E ; P : Path E --> b P --> c ; d *********** success #1 *********** equation ceq length(E ; P) = 1 + length(P) if E ; P : Path . E --> b P --> c ; d length(b ; (c ; d)) ---> 1 + length(c ; d) *********** trial #2 ceq length(E ; P) = 1 + length(P) if E ; P : Path . E --> c P --> d *********** solving condition fragment E ; P : Path *********** success for condition fragment E ; P : Path E --> c P --> d *********** success #2 *********** equation ceq length(E ; P) = 1 + length(P) if E ; P : Path . E --> c P --> d length(c ; d) ---> 1 + length(d) *********** equation eq length(E) = 1 . E --> d length(d) ---> 1 rewrites: 20 in 0ms cpu (1ms real) (~ rewrites/second) result NzNat: 3