Maude-help mailing list

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

Without the full example, (including modules ELECTRICAL-COMPONENT and SATISFACTION) I can't reproduce your problem to look into it.

Steven

On 6/26/12 7:34 PM, Mark Yu wrote:

Dear Sir :
          I am a postgraduate from Taibei University. I am facing some problems about MAUDE now .
 
The example on Book is
*************************************************
mod RELAY is
   pr ELECTRICAL-COMPONENT .
   pr SATISFACTION .
 
   sort Relay .
   subsort Relay < ElectricalComponent .
  
   op Relay : -> Relay [ctor] .
   op drawn :_ : Bool -> Attribute [ctor gather (&)] .
   var B : Bool .
   var R : Qid .
   var VRelay : Relay .
   var ATTS : AttributeSet .
   var CONF : Configuration .
 
   ops canDraw canDrop : Qid Configuration -> Bool [memo] .
   eq canDraw(R, CONF) = false [owise] .
   eq canDrop(R, CONF) = false [owise] .
 
   op idle : Qid Configuration -> Bool .
 
   ceq idle(< R : VRelay | drawn : false, ATTS > CONF) = false  if canDraw(R, (< R : VRelay | drawn : false, ATTS > CONF)) .
   ceq idle(< R : VRelay | drawn : true, ATTS > CONF) = false   if canDrop(R, (< R : VRelay | drawn : true, ATTS > CONF)) .

endm  
**************************************************  
The red Words has reported the error . I think it's a defining problem .
I have quoted the MAUDE built-in module . For example," op <_:_|_> : Oid Cid AttributeSet -> Object [ctor] ." in module CONFIGURATION .
I don't know about How to define the red sentence.
 
 I think I can't solve the problem , please give me some tips. 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