Maude-help mailing list

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

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