Maude-help mailing list

[Vladimir Klebanov <klebanov AT kit.edu>]

Many thanks to all of you for the very helpful and educational
replies. To close the loop, I would like to add the following.

Googling with the right keywords delivered a complete metalevel solution:
http://einarj.at.ifi.uio.no/inf5130/exercises4/exercisesL4.maude
(Hello Einar!)

Of course, it is much more comfortable to use the Anima tool, which is
fantastic and, I think, should be advertised more prominently on the
Maude page.

For your entertainment: one source of inadequacy in my rules was as
follows. I was trying to compute a closure of a set of strings wrt
concatenation, but the rule

    rl[concatenate] : (k1,k2,know) => (k1 + k2,k1,k2,know) .

was not sufficient for this, as k1 and k2 cannot be instantiated with
the same element.

Thanks again,

Vladimir




-- 
Vladimir Klebanov
Postdoctoral Researcher, Application-oriented Formal Verification
Karlsruhe Institute of Technology
http://formal.iti.kit.edu/~klebanov