Maude-help mailing list

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

James,

The CRC cannot handle built-ins. It's based on a critical pair analysis. 

Best,

Francisco


> On 25 May 2017, at 22:50, James M Decker 
> <decker31 AT purdue.edu>
>  wrote:
> 
> Hi Francisco,
> 
> I've downloaded maude++ and the MFE. SCC appears to be working now (though 
> the Church-Rosser tool says it's unable to work with built-ins...I'm sure I 
> just messed something up, so I'll keep looking it over).
> 
> Thanks!
> 
> James
> From: Francisco Durán 
> <duran AT lcc.uma.es>
> Sent: Thursday, May 25, 2017 11:26:28 AM
> To: James M Decker
> Cc: 
> maude-help AT cs.uiuc.edu
> Subject: Re: [[Maude-help] ] Using SCC
>  
> James,
> 
> I suppose you have downloaded SCC from its web site 
> (http://maude.cs.uiuc.edu/tools/scc/). There it says that you need either 
> the ITP or an extended version of Maude (Maude 2.3). 
> 
> The tool was updated to Maude 2.7 and 2.7.1 as part of the Maude Formal 
> Environment (MFE) (https://github.com/maude-team/MFE/wiki), but, again, an 
> extended version of Maude is required. 
> 
> Binaries of extended versions of Maude are available in both cases in their 
> respective sites. 
> 
> Best,
> 
> Francisco
> 
> 
>> On 25 may 2017, at 16:18, James M Decker 
>> <decker31 AT purdue.edu>
>>  wrote:
>> 
>> Hi Francisco,
>> 
>> Great, thank you! Yes, I'm running Maude 2.7 and SCC 2.3. The Maude manual 
>> (2.7) says the following:
>> 
>> "Maude’s Sufficient Completeness Checker (SCC) can be used to ensure that 
>> constructor declarations are really correct, so that all functions are 
>> fully defined relative to those constructors. We can take the NUMBERS 
>> module, incrementally introduced in Chapter 3 and the previous sections of 
>> this chapter, to illustrate how the SCC can be used to help the specifier 
>> in this regard."
>> 
>> The following (buggy) code is then provided:
>> 
>>   fmod NUMBERS is
>>     protecting BOOL .
>> 
>>     sort Zero .
>>     sorts Nat NzNat .
>>     subsort Zero NzNat < Nat .
>>     op zero : -> Zero [ctor] .
>>     op s_ : Nat -> NzNat [ctor] .
>>     op sd : Nat Nat -> Nat .
>>     ops _+_ _*_ : Nat Nat -> Nat [assoc comm] .
>>     op _+_ : NzNat Nat -> NzNat [ditto] .
>>     op _*_ : NzNat NzNat -> NzNat [ditto] .
>>     op p : NzNat -> Nat .
>> 
>>     vars I N M : Nat .
>>     eq N + zero = N .
>>     eq N + s M = s (N + M) .
>>     eq sd(N, N) = zero .
>>     eq sd(N, zero) = N .
>>     eq sd(zero, N) = N .
>>     eq sd(s N, s M) = sd(N, M) .
>>     eq N * zero = zero .
>>     eq N * s M = (N * M) + N .
>>     eq p(s N) = N [label partial-predecessor] .
>> 
>>     eq (N + M) * I = (N * I) + (M * I)
>>       [nonexec metadata "distributive law"] .
>> 
>>     sort Nat3 .
>>     ops 0 1 2 : -> Nat3 [ctor] .
>>     op _+_ : Nat3 Nat3 -> Nat3 [comm] .
>>     vars N3 : Nat3 .
>>     eq N3 + 0 = N3  .
>>     eq 1 + 1 = 2 .
>>     eq 1 + 2 = 0 .
>>     eq 2 + 2 = 1 .
>> 
>>     sort NatSeq .
>>     subsort Nat < NatSeq .
>>     op nil : -> NatSeq .
>>     op __ : NatSeq NatSeq -> NatSeq [assoc id: nil] .
>> 
>>     sort NatSet .
>>     subsort Nat < NatSet .
>>     op empty : -> NatSet .
>>     op _;_ : NatSet NatSet -> NatSet [assoc comm id: empty] .
>>     eq N ; N = N [label natset-idem] .
>> 
>>     op _in_ : Nat NatSet -> Bool .
>>     var NS : NatSet .
>>     eq N in N ; NS = true .
>>     eq N in NS = false [owise] .
>>   endfm
>> 
>> This is followed by the following commands:
>> 
>> Maude> (scc NUMBERS .)
>> Checking sufficient completeness of NUMBERS ...
>> Warning: This module has equations that are not left-linear which
>> will be ignored when checking.
>> Failure: The term 0 was found to be a counterexample. Since the
>> analysis is incomplete, it may not be a real counterexample.
>> 
>> However, when I run this command, I get the following:
>> 
>> Maude> (scc NUMBERS .)
>> Checking sufficient completeness of NUMBERS ...
>> Warning: This module has equations that are not left-linear which will be 
>> ignored when checking.
>> 
>> As such, the failure notification is missing. Based on your email, I would 
>> guess this is simply a problem of SCC not working with Maude 2.7? It's 
>> weird that it would still be mentioned in the manual (and with a message 
>> that I'm unable to replicate)...
>> 
>> Please let me know if you need more details! Thank you for your help.
>> 
>> James
>> From: Francisco Durán 
>> <duran AT lcc.uma.es>
>> Sent: Thursday, May 25, 2017 5:35:50 AM
>> To: James M Decker
>> Cc: 
>> maude-help AT cs.uiuc.edu
>> Subject: Re: [[Maude-help] ] Using SCC
>>  
>> Hi James, 
>> 
>> I’m going to need details to help you. SCC cannot be run on the “official” 
>> version of Maude, it requires the extended version with the SCC hooks. You 
>> say that you have managed to execute it, so I suppose you already know 
>> this. The SCC was initially developed for Maude 2.3, so if you are using 
>> 2.7 I guess you are using it inside the MFE, in which case the interaction 
>> should be slightly different... as I said, without details...
>> 
>> Best, 
>> 
>> Francisco
>> 
>>  
>>> On 24 may 2017, at 18:42, James M Decker 
>>> <decker31 AT purdue.edu>
>>>  wrote:
>>> 
>>> Hey there,
>>> 
>>> I'm following the Maude Manual (for Maude 2.7), but having some trouble 
>>> in Section 4.4 regarding use of the SCC. Specifically, it doesn't seem 
>>> that SCC is built into Maude 2.7 by default? I went and downloaded SCC 
>>> separately and was able to get it loaded in and running, but the output 
>>> doesn't match what's shown in the manual. Do you have any suggestions?
>>> 
>>> James Decker