Maude-help mailing list

[Santiago Escobar <sescobar AT dsic.upv.es>]

Dear Bartosz Zieliński, it is a bug for the case when you specify both a 
depth bound and a bound on the number of solutions. I will fix this bug and 
submit a new version to GitHub.
—Santiago

> On 11 Jul 2017, at 18:12, 
> bzielinski AT uni.lodz.pl
>  wrote:
> 
> 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
>