Maude-help mailing list

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

For small values of n you could label the rules and use the built-in fragment of the Maude strategy language:

mod TEST is
  pr NAT .
  ops f g : Nat -> Nat .
  op h : Nat Nat -> Nat .

var N : Nat .
  crl f(N) => g(N + 1) if N < 20 [label s] .
  crl g(N) => f(N + 1) if N rem 5 =/= 0 [label s] .

  rl f(N) => h(N, g(N)) [label m] .
endm

srew f(0) using s ; s ; s ; s ; m ; s ! .

This returns terms that result from 4 applications of an s rule, one application of an m rule, and then applications of s rules until no more s rules apply.

Steven

On 5/22/13 4:46 AM, Morandi Benjamin wrote:

Dear All,

 

I would like to achieve the following:

 

-          Rewrite a starting term ‘t’ ‘n’-times using ‘rew[n]’ and a set of rules ‘s’. The resulting term is ‘tt’. -          Change ‘tt’ by manually applying a rule that is not in ‘s’. The resulting term is ‘ttt’. -          Continue rewriting ‘ttt’ using ‘cont .’ and  the rules in ‘s’.

 

More generally, I’d like to influence which rule the rewrite command picks at a breakpoint of my choosing. Does anyone have an idea on how to do that?

 

Best regards

 

Benjamin Morandi

_______________________________________________
Maude-help mailing list
Maude-help AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/maude-help