Maude-help mailing list

[Mirko Viroli <mirko.viroli AT unibo.it>]

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?

Thank you for any suggestion on this topic.
--Mirko

--
Dott. Ing. Mirko Viroli
Research Associate
DEIS, Alma Mater Studiorum - Università di Bologna, Cesena
via Venezia 52, 47023 Cesena, Italy
Tel.: +39 0547 339216,  Fax: +39 0547 339208
mailto:mirko.viroli AT unibo.it
http://www.ingce.unibo.it/~mviroli/