Maude-help mailing list

[bzielinski AT uni.lodz.pl]

Dear Sir or Madame

When using Maude's narrowing search command in Full Maude I have observed
that for some modules the search command uses strangely the required
solution limit. For example, with the following module:
mod TEST is
        sorts Conf State Oid .
        op nil : -> Conf .
        op __ : Conf Conf -> Conf [assoc comm] .
        op <_> : Conf -> State .
        ops O a : Oid -> Conf .
        vars X : Oid .  var C : Conf .
        rl [create] : < C > => < C O(X) a(X) > [nonexec] .
endm

the command
 (search [1, 5] in TEST : < nil > ~>* < C:Conf a(R1:Oid) a(R2:Oid)
a(R3:Oid) > .)
returns 6 solutions (all permutations of assignement of "#"-variables to
R1 , R2, R3.
Similarly anomalous behaviour occurs when using narrowing search at
metalevel.
Solutions, by the way, are correct.
I had also examples with executable rewrite rules which exhibit similar
behaviour. Is this a bug or a feature? Or, if it is a feature can you
point me to some resource which would help me to understand it?

Best regards

Bartosz Zieliński