Maude-help mailing list

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

In (Core) Maude the upModule takes a Qid as first argument. Perhaps it is just that you are missing the quote.

Paco

El 30/07/2009, a las 12:06, Narsis Amini escribió:

Thanks for your reply,
here is a simple example:

fmod MYCONF is
  pr BOOL .
  pr INT .
  pr FLOAT ..
  protecting STRING . 

****************************
*** Attribute Definition ***
****************************
  sorts Attribute AttributeSet AttributeList .
  subsort Attribute < AttributeSet .
  op asnone : -> AttributeSet .
  op _;_ : AttributeSet AttributeSet -> AttributeSet
      [ctor assoc comm id: asnone format (d d n d)] .
  subsort Attribute < AttributeList .
  op alnone : -> AttributeList .
  op _;|_ : AttributeList AttributeList -> AttributeList
      [ctor assoc id: alnone format (d d n d)] .

  sorts AType AVal .
  op _~_ : AType AVal -> Attribute [format (sssg o d d)].
  op AVnone : -> AVal .

  vars AS atts : AttributeSet .
  var A : Attribute .
  var AT : AType .
  var AV : AVal .

************************************
*** Message Structure Definition ***
************************************

    sort MVal MValName MsgName .
    sorts Query Reply PType .

    sort Msg MsgQ .
    subsort Msg < MsgQ .
    op none : -> MsgQ .
    op _,_ : MsgQ MsgQ -> MsgQ [ctor assoc id: none] . 
  *** add to q on left; remove from right
  *** MsgQ is not comm to preserve q order
  
    op _(_) : MsgName AttributeSet -> Msg [format (r o g o o)].
    ops lin lout : MsgQ -> Attribute .
    
      op _(_) : MValName Msg -> MVal [format (r o r o o)].
***      op _(_,_) : MValName Msg Reply -> MVal [format (r o r o r o o)].
      
    op _<-_@_ : Oid Msg Oid -> Msg [format (nsb o r o b o)]..
    
  
  *********************************
  *** State & Object Definition ***
  *********************************
  sort SState .      
  op ssnone : -> SState .
  op __ : SState SState -> SState [ctor assoc comm id: ssnone] .
  
  sort Oid Cid Object .  *** object id, class id, object
  subsorts Object < SState .

  op [_:_|_|_|_] : Oid Cid AttributeSet SState AttributeSet -> 
                            Object [format (ns b o nssss d d d d d d d d)] .

    *****sort converstions ******
    op vi : AVal -> Int .
    op nv : Int -> AVal .
    op vb : AVal -> Bool .
    op bv : Bool -> AVal  .


endfm

mod ACTORS is 
    inc MYCONF .

    sort intensity invac status . 
    op light : -> Cid .
    ops light1 light2 : -> Oid .

    ops intensity lstatus : -> AType .
    op intensity : -> Nat .
    ops off on : -> status .
    ops switch-on switch-off inc-intensity dec-intensity : -> MsgName .


    op sv : status -> AVal .
    op iv : intensity -> AVal .

    vars intensity? intensity1? intensity2? ointensity  ?vint : intensity .
    var confrm-vac? invac? : Attribute .
    var lstatus? : status .
    var light? : Oid .
    vars O Oto Ofrom : Oid .
    vars inQ outQ : MsgQ .
    var c : SState .
    op getTotalIntensity : SState -> Int .

    eq getTotalIntensity ([ light? : light | (lstatus ~ sv(lstatus? ) ) ; (intensity ~ iv(intensity?)) 
      | ssnone | lin(inQ ) ; lout(outQ) ] c ) =  vi (iv (intensity?)) + getTotalIntensity(c) .
    
    eq getTotalIntensity ([ light? : light | (lstatus ~ sv(lstatus? )) ; (intensity ~ iv(intensity?)) 
          | ssnone | lin(inQ ) ; lout(outQ) ] ) =  vi( iv (intensity?)) .

endm


mod INTERFACES is 
    protecting ACTORS .
    protecting META-LEVEL .

    sort interface .
    subsort interface < Cid .

    var M : Module .
    var Q : Qid .
    var at : AType .
    var av : AVal .

    ops light1 light2 :-> Oid .
    ops test : -> Oid .
    op myState :-> SState .
    op term : -> ResultPair .
***    eq myState =  [ light1 : light | (lstatus ~ sv(on)) ; (intensity ~ nv( 1 )) 
***      | ssnone | lin(inQ) ; lout(outQ) ]  [ light2 : light | (lstatus ~ sv(on)) ***; (intensity ~ nv( 2 )) | ssnone | lin(inQ) ; lout(outQ) ] . 

 eq term = metaReduce ( upModule( ACTORS , true ), upTerm( getTotalIntensity( [ light1 : light | (lstatus ~ sv(on)) ; (intensity ~ nv( 1 )) 
      | ssnone | lin(inQ) ; lout(outQ) ] ) ) ) .

endm

---

From: Francisco Durán <duran AT lcc.uma.es>
To: Narsis Amini <narsisa90 AT yahoo.com>
Cc: maude-help AT maude.cs.uiuc.edu
Sent: Thursday, July 30, 2009 8:30:46 PM
Subject: Re: [Maude-help] upModule problem

Could you please send us an example? It is probably just a syntactic error.

Best,

Francisco 

El 30/07/2009, a las 10:51, Narsis Amini escribió:

Dear all,
I want to use reflection capabilities.
I import Meta-level module, but something is wrong here and 
when I use upModule, "bad token" message is raised. 
I have no problem with operations like metaApply etc.
I use Maude in windows OS.
I would be pleased if you help me.
Thanks
  

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