Maude-help mailing list

[Mark Yu <fangwenmahu AT hotmail.com>]

Dear Sir :
          I am a postgraduate from Taibei University.  Our lab is doing some research about Maude recently. After reading the paper "Verification of Safety Properties for Relay Interlocking Systems",we  run this case and meet some problems.

 For example: Two files of  the source write here. That’s about the track of ELECTRICAL-COMPONENT and CIRCUIT. But I can’t understand the bad token B or R in the mod CIRCUIT , for I have defined it.

 

The source file is:

 

mod ELECTRICAL-COMPONENT is
  
protecting COMMON .  
protecting QID-SET . 
including CONFIGURATION .
 
sort ElectricalComponent .  
subsort ElectricalComponent < Cid .
 
var C : Qid .  
var CS : QidSet .  
var Conf : Configuration .
  
op conducting : Qid Configuration -> Bool .  
eq conducting(C, Conf) = false [owise] .
op anyConducting : QidSet Configuration -> Bool .
eq anyConducting((C, CS), Conf) = conducting(C, Conf) or-else anyConducting(CS, Conf) . 
eq anyConducting(empty, Conf) = false .
endm
 
 
mod CIRCUIT is
  
including CONFIGURATION .
including QID .
  
op {_} : Configuration -> Configuration .
  
var B : Qid . 
var R : Qid .  
var V@Relay : Relay . 
var ATTS : AttributeSet .  
var CONF : Configuration .
op idle : Configuration -> Bool   
op valid : Configuration -> Bool . 
eq valid(CONF) = true [owise] . 

********************************  
***Button behaviour 
********************************* 
crl [pushButton] :    
{ < B : Button | pushed : false > CONF} => { < B : Button | pushed : true > CONF}
if idle(< B : Button | pushed : false > CONF) 
and-then    
valid(< B : Button | pushed : false > CONF) . 
crl [releaseButton] :    
{ < B : Button | pushed : true > CONF } =>
 { < B : Button | pushed : false > CONF }   
if
 idle(< B : Button | pushed : true > CONF)  
and-then     
valid(< B : Button | pushed : true > CONF) . 
************************************ 
*** Relay behaviour  
************************************!  
crl [drawRelay]      
{ < R : V@Relay | drawn : false, ATTS > CONF } =>
 { < R : V@Relay | drawn : true, ATTS > CONF }     
if       
valid(< R : V@Relay | drawn : false, ATTS > CONF)    
and-then       
canDraw(R, (< R : V@Relay | drawn : false,  ATTS > CONF)) . 
crl [dropRelay] :     
{ < R : V@Relay | drawn : true, ATTS > CONF }  =>
 { < R : V@Relay | drawn : false, A! TTS > CONF }    
if        
valid(< R : V@Relay | drawn : true, ATTS > CONF)   
and-then   
canDrop(R, (< R : V@Relay | drawn : true,  ATTS > CONF)) .
endm

 

Here the question is when we run this example, there are many warnings,such as:


Maude> in /usr/maude/ve/ELECTICAL-COMPONENT.maude
==========================================
mod ELECTRICAL-COMPONENT
Warning: "ELECTICAL-COMPONENT.maude", line 2 (mod ELECTRICAL-COMPONENT): module
    COMMON does not exist.
Warning: "ELECTICAL-COMPONENT.maude", line 6 (mod ELECTRICAL-COMPONENT):
    undeclared sort Cid.
Warning: "ELECTICAL-COMPONENT.maude", line 10 (mod ELECTRICAL-COMPONENT):
    undeclared sort Configuration.

==========================================
mod CIRCUIT
Warning: "te.maude", line 266 (mod CIRCUIT): didn't expect token B:
crl [ pushButton ] : { < B <---*HERE*
Warning: "te.maude", line 265 (mod! CIRCUIT): no parse for statement
crl [pushButton] : {< B : Button | pushed : false > CONF} => {< B : Button | pushed : true > CONF} if idle (< B : Button | pushed : false > CONF) and-then
    valid (< B : Button | pushed : false > CONF) .
Warning: "te.maude", line 275 (mod CIRCUIT): didn't expect token B:
crl [ releaseButton ] : { < B <---*HERE*
Warning: "te.maude", line 274 (mod CIRCUIT): no parse for statement
crl [releaseButton] : {< B : Button | pushed : true > CONF} => {< B : Button | pushed : false > CONF} if idle (< B : Button | pushed : true > CONF) and-then
    valid (< B : Button | pushed : true > CONF) .
Warning: "te.maude", line 288 (mod CIRCUIT): didn't expect token R:
crl [ drawRelay ] : { < R <---*HERE*
Warning: "te.maude", line 287 (mod CIRCUIT): no parse for statement
crl [drawRelay] : {< R : V@Relay | drawn : false, ATTS >! CONF} => {< R : V@Relay | drawn : true, ATTS > CONF} if vali d (< R : V@Relay | drawn : false, ATTS
    > CONF) and-then canDraw (R, (< R : V@Relay | drawn : false, ATTS > CONF)) .
Warning: "te.maude", line 297 (mod CIRCUIT): didn't expect token R:
crl [ dropRelay ] : { < R <---*HERE*
Warning: "te.maude", line 296 (mod CIRCUIT): no parse for statement
crl [dropRelay] : {< R : V@Relay | drawn : true, ATTS > CONF} => {< R : V@Relay | drawn : false, ATTS > CONF} if valid (< R : V@Relay | drawn : true, ATTS >
    CONF) and-then canDrop (R, (< R : V@Relay | drawn : true, ATTS > CONF)) .




We think these warnings are caused by the loss of "COMMON". But we couldn't find this model, we want to know whether the "COMMON" is a
built-in model of Maude.If it is,can you give us some details.Can you do some guiding to  help us successfully run this model? We are looking forward to your response.
 Sincerely,
    !   Mark Yu