Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

Also there are a number of syntax errors in the 2nd module so whatever you have is not running code.

Steven

On 5/29/12 11:40 AM, Francisco Durán wrote: Hi Mark,

COMMON is not a Maude built-in module. You should contact one of the authors of the paper/specification to get it. 

Best,

Francisco

On 29/05/2012, at 09:17, Mark Yu wrote:

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  

_______________________________________________
Maude-help mailing list
Maude-help AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/maude-help

_______________________________________________
Maude-help mailing list
Maude-help AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/maude-help