Maude-help mailing list

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

Narsis,

I cannot reproduce your problem. Can you please tell which version of Maude are you using and on which machine.

Francisco

    \||||||||||||||||||/

  --- Welcome to Maude ---

    /||||||||||||||||||\

   Maude 2.4 built: Nov  6 2008 16:49:57

   Copyright 1997-2008 SRI International

  Thu Jul 30 17:32:00 2009

Maude> fmod VENDING-MACHINE-SIGNATURE is

>     sorts Coin Item Marking .

>     subsorts Coin Item < Marking .

>     op __ : Marking Marking -> Marking [assoc comm id: null] .

>     op null : -> Marking .

>     op $ : -> Coin [format (r! o)] .

>     op q : -> Coin [format (r! o)] .

>     op a : -> Item [format (b! o)] .

>     op c : -> Item [format (b! o)] .

>   endfm

Maude> reduce in META-LEVEL : 

>            upModule('VENDING-MACHINE-SIGNATURE, false) .

reduce in META-LEVEL : upModule('VENDING-MACHINE-SIGNATURE, false) .

rewrites: 1 in 0ms cpu (0ms real) (1706 rewrites/second)

result FModule: fmod 'VENDING-MACHINE-SIGNATURE is

  including 'BOOL .

  sorts 'Coin ; 'Item ; 'Marking .

  subsort 'Coin < 'Marking .

  subsort 'Item < 'Marking .

  op '$ : nil -> 'Coin [format('r! 'o)] .

  op '__ : 'Marking 'Marking -> 'Marking [assoc comm id('null.Marking)] .

  op 'a : nil -> 'Item [format('b! 'o)] .

  op 'c : nil -> 'Item [format('b! 'o)] .

  op 'null : nil -> 'Marking [none] .

  op 'q : nil -> 'Coin [format('r! 'o)] .

  none

  none

endfm

El 30/07/2009, a las 14:22, Narsis Amini escribió:

Thanks,

It does not work too.

Even I can not load the following example

from the book all about Maude :

 

  fmod VENDING-MACHINE-SIGNATURE is
    sorts Coin Item Marking .
    subsorts Coin Item < Marking .
    op __ : Marking Marking -> Marking [assoc comm id: null] .
    op null : -> Marking .
    op $ : -> Coin [format (r! o)] .
    op q : -> Coin [format (r! o)] .
    op a : -> Item [format (b! o)] .
    op c : -> Item [format (b! o)] .
  endfm

reduce in META-LEVEL :
           upModule('VENDING-MACHINE-SIGNATURE, false) .

--- On Thu, 7/30/09, Francisco Durán <duran AT lcc.uma.es> wrote:

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

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