Maude-help mailing list

["Hui Ding" <huiding AT uiuc.edu>]

I got really frustrated by the following phenomenon. First, I defined four modules in four separate files.

<1> a file named "oidlist.maude", declaring a new sort OidList

(omod OID-LIST is
  including INT .
  including CONFIGURATION .
 
  sort OidList .
  subsort Oid < OidList .
  ... ... 

endom)

 

<2> a file named "general.maude"

(omod GENERAL-RULES is
  including OID-LIST .
  
  sort ThreadState .
  ops start shutdown active passive : -> ThreadState .

  ... ...

endom)

 

<3> a file named "control.maude"

(omod CAR-CONTROL is
  including GENERAL-RULES .
  ... ... 
endom)

 

<4> a file named "deadlock.maude"

(omod DEADLOCK is
  including CONFIGURATION .
  including OID-LIST .
  including CAR-CONTROL .
 
  var O O2 : Oid .
  var C : Cid .
  var OIDLIST : OidList .
  var CF : Configuration .
  var ATTRSET : AttributeSet .

  ... ...

  --- some rewriting rules involving OIDLIST

endom)

 

Now I do as follows

in full-maude -> in oidlist -> in general -> in control, all modules have been correctly introduced until now.

But ...

when I run command "in deadlock", I was told the following message tens of times and this command just does not return :

       Advisory: could not find sort OidList in meta-module DEADLOCK.
       Advisory: bad operator declaration op 'OIDLIST : nil -> 'OidList [none] . in meta-module DEADLOCK.

 

When I delete those rewriting rules involving OIDLIST but keep the variable OIDLIST declarations there,  the same phenomenon happens.

When I delete all the operation, equation and rewriting rules in module  DEADLOCK  and only keep those statements as shown above, the warning messages disappear, but the command just does not return.

 

What happens here? How to make it work? Thanks for the help.