Maude-help mailing list

[Francisco Durán <duran AT lcc.uma.es>]

Hi Roberto,

First of all, the fact that the tool gives you some (conditional) critical 
pairs doesn't mean your specification is not confluent. It is just that the 
tool cannot discard them. Camilo Rocha and Jose Meseguer are currently 
working on methods to discard these critical pairs, and we'd like to have 
them available in the CRC soon. With these methods one could prove your spec 
ground confluence. Notice that since you cannot assume confluence you have to 
prove that for any possible instantiation of your critical pair it always 
joins. 

With the current tool your only chance is to modify your spec by replacing 
equations or by adding new ones that allow joining the critical pairs. I 
cannot say more without your current spec, but from your message I deduce you 
already know the procedure. 

Cheers,

Francisco


El 12/08/2010, a las 22:09, Roberto Bruttomesso escribió:

> Hello,
> 
> I'm trying to use the nice CRC tool of maude to check one
> specification of mine. The problem is that I need to express
> conditional statements, like
> 
> rd( wr( x, i, e ), j ) = rd( x, j )             if i > j .
> 
> however I cannot define i, j to be Nat and use the predefined _>_
> operator. So I tried to define it myself using a successor function
> and so on. However
> I cannot specify that the relation is transitive, and I get a critical pair
> 
> The following critical pairs cannot be joined:
>  ccp for 8 and 6a
>    rd(wr(wr(#1:ARRAY,I:INDEX,E:ELEM),#2:INDEX,#3:ELEM),J:INDEX)
>    = rd(wr(#1:ARRAY,#2:INDEX,#3:ELEM),J:INDEX)
>    if I:INDEX > J:INDEX = true /\ #2:INDEX > I:INDEX = true .
> 
> which could actually be joined since I > J and #2 > I implies #2 > J,
> and a rule more would be triggered.
> 
> Defining something like
> 
> ceq N > M if N > L and L > M .
> 
> does not seem to help.
> 
> Is there a way around ?
> 
> Thanks in advance !
> 
> Roberto
> 
> -- 
> Roberto Bruttomesso, PhD - http://tinyurl.com/r0b3r70
> _______________________________________________
> Maude-help mailing list
> Maude-help AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help