Maude-help mailing list

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

On Wednesday 24 May 2006 01:43, Mirko Viroli wrote:
> Hi all,
>
> I have some troubles understanding the combination of rewrites and the
> library counter..
>
> Since Maude accepts this command "rew [1] counter ." replying an
> increasing natural number each time, I would be tempted to use as a
> condition to a rule the following "counter => N:Nat".
> Unfortunatelly, this does not seem to work.
>
> In particular, given the following definition:
>
> vars N N' : Nat .
>
> op {_}: Nat -> Nat [frozen] .
> crl {N} => {N'} if counter => N' .
>
>
> I would expect the command "rew [1] {100}" to yield each time a
> different {N}, instead I have:
>
> Maude> rew [1] {10} .
> rewrite [1] in TRY : {10} .
> rewrites: 0 in 0ms cpu (0ms real) (~ rewrites/second)
> result Nat: {10}
>
>
> That is, no match!!!
> Any clue on that?

Counters only work for normal rewriting; not search or model checking because 
otherwise they cause an infinite search space. => condition fragments are 
evaluated using search.

Steven