Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

On Friday 21 November 2008 07:25, Marc Boyer wrote:
> I try to use the tracing control commands, but I do not achieve
> to make it works.
>
> Here is a minimal example: I want to trace the reduction of f,
> but not the one on NAT.
>
> fmod MY-MOD is
>   protecting NAT .
>   sort S .
>   op _ + _ : S S -> S .
>   op f _ : Nat -> S .
>   vars n n' : Nat .
>   eq [lab] : f n + f n' = f ( n + n') .
> endfm
>
> I have tried to select f:
>       set trace on .
>       set trace select on .
>       trace select f .
>       red f 3 + f 4 .
> But it does not print anything (except the result of course).

Thats because _+_, not f is the top symbol in the lhs of your equation and 
you 
haven't selected _+_.

> I have tried to exclude NAT:
>       set trace on .
>         trace exclude NAT .
>       red f 3 + f 4 .
> But it prints the reduction 3+4 -> 7

The trace exclude feature excludes rewrites happening in the NAT module, but 
you are rewriting in MY-MOD. The intended use for trace exclude is when you 
have rewrites happening in multiple modules due to reflection. The classic 
case is when you run a reduced in Full Maude, you want to see the rewrites 
happening in your module and not thoses of Full Maude.

> The only thing that worf is to select le label lab, but in my
> real problem, I have a lot of rules to traces, and I would be able
> to select operators or to exlude modules.

The trace control granularity is fairly coarse - I can't think of a good way 
to selection between operators with the same name.

Steven