Maude-help mailing list

[Patrick Browne <patrick.browne AT dit.ie>]

Esther
I think that by using a lazy strategy for the location operation you
should get the same results as BOBJ.

op location : Monk Time-Of-Day -> Location-On-Path [strat(0)] .

Regards,
Pat


th MONK-ON-MOVE is
protecting BOOL .
sorts Monk Time-Of-Day Location-On-Path .
op location : Monk Time-Of-Day -> Location-On-Path [strat(0)] .
op meets : Monk Monk Time-Of-Day Time-Of-Day Location-On-Path
Location-On-Path -> Bool .
vars M1 M2 : Monk .
vars T1 T2 : Time-Of-Day .
vars L1 L2 : Location-On-Path .
eq meets(M1,M2,T1,T2,L1,L2) = if M1 =/= M2 and (T1 == T2) and (L1 == L2)
then true else false fi .
endth


On 15/12/2010 11:41, esther loeliger wrote:
> Paco,
> 
> Thank you very much for the link!
> 
> Is there any way of changing the order in which rewriting rules are applied?
> 
>>>>
> th A
> 
> th B
> 
> th C including (A + B)
> <<<
> 
> If only rewriting rules of A and B are applied before the ones of C,
> there won't be any problems. BOBJ seems to rewrite in that order.
> 
> -Esther
> 
> 
> On 14 December 2010 17:14, Francisco Durán 
> <duran AT lcc.uma.es
> <mailto:duran AT lcc.uma.es>>
>  wrote:
> 
>     Esther,
> 
>     I don't know much about BOBJ, but I would say that everything in
>     OBJ3, unless perhaps some syntactic issue, should have the same
>     operational behavior in Maude. 
> 
>     You could perhaps take a look to the paper by Meseguer "From OBJ to
>     Maude and Beyond"
>     (http://www.springerlink.com/content/g52731263044818g/). I don't
>     know whether this is the kind of document you are looking for. 
> 
>     Paco
> 
> 
>     El 14/12/2010, a las 17:50, esther loeliger escribió:
> 
>>
>>
>>     ---------- Forwarded message ----------
>>     From: *esther loeliger* 
>> <estherloeliger AT gmail.com
>>     
>> <mailto:estherloeliger AT gmail.com>>
>>     Date: 14 December 2010 16:00
>>     Subject: Re: [Maude-help] MAUDE vs. BOBJ: same code evaluates
>>     differently ('false' vs. 'true')
>>     To: Michael Katelman 
>> <katelman AT uiuc.edu
>>  
>> <mailto:katelman AT uiuc.edu>>
>>
>>
>>     Michael,
>>
>>     BOBJ, in this case, seems to first rewrite
>>     location(monkd,timed2) to locationd2 and 
>>     location(monku,timeu2) to locationu2.
>>     No backtracking.
>>
>>     Might it be possible to use variables instead when trying to make
>>     stuff equal? Something along the lines of:
>>
>>     ceq location(X1,Y2) = location(X2,Y2) if X1 == X2 and Y1 == Y2 .
>>
>>     When trying to port some of Goguen's OBJ3 examples to MAUDE I ran
>>     into problems as well (include issues).
>>
>>     Is there a document that describes the differences of the OBJ
>>     languages?
>>
>>     -Esther
>>
>>
>>     On 14 December 2010 15:49, Michael Katelman 
>> <katelman AT uiuc.edu
>>     
>> <mailto:katelman AT uiuc.edu>>
>>  wrote:
>>
>>         Esther,
>>
>>         I am not exactly sure (because I don't know much about BOBJ),
>>         but it
>>         could be because of speed. Does BOBJ do backtracking when
>>         trying to
>>         establish equalities? Maude will not do this, instead relying on
>>         confluence (and termination), which the user must ensure.
>>
>>         -Michael
>>
>>         On Tue, Dec 14, 2010 at 9:37 AM, esther loeliger
>>         
>> <estherloeliger AT gmail.com
>>  
>> <mailto:estherloeliger AT gmail.com>>
>>         wrote:
>>         > Michael,
>>         > Thanks a lot for getting back quickly!
>>         > When I switch on the trace, I can in fact see what you wrote:
>>         > MAUDE:
>>         >>>>
>>         > reduce in MONK-MEETS-HIMSELF : location(monku, timeu2) ==
>>         location(monkd,
>>         >     timed2) .
>>         > *********** equation
>>         > eq location(monku, timeu2) = locationu2 .
>>         > empty substitution
>>         > location(monku, timeu2)
>>         > --->
>>         > locationu2
>>         > *********** equation
>>         > eq timed2 = timeu2 .
>>         > empty substitution
>>         > timed2
>>         > --->
>>         > timeu2
>>         > *********** equation
>>         > (built-in equation for symbol _==_)
>>         > locationu2 == location(monkd, timeu2)
>>         > --->
>>         > false
>>         > rewrites: 3 in 0ms cpu (0ms real) (~ rewrites/second)
>>         > result Bool: false
>>         > <<<
>>         > BOBJ:
>>         >>>>
>>         > ***>  red location(monku,timeu2) == location(monkd,timed2) .
>>         should be true
>>         > ==========================================
>>         > reduce in MONK-MEETS-HIMSELF : location(monku, timeu2) ==
>>         location(monkd,
>>         >     timed2)
>>         > rewrite target: location(monku, timeu2)
>>         > use: location(monku, timeu2) = locationu2
>>         > result: locationu2
>>         > ................................
>>         > rewrite target: location(monku, timeu2)
>>         > rewrite point: location(monku, timeu2)
>>         > result: locationu2
>>         > ................................
>>         > rewrite target: location(monkd, timed2)
>>         > use: location(monkd, timed2) = locationd2
>>         > result: locationd2
>>         > ................................
>>         > rewrite target: locationd2
>>         > use: locationd2 = locationu2
>>         > result: locationu2
>>         > ................................
>>         > rewrite target: locationd2
>>         > rewrite point: locationd2
>>         > result: locationu2
>>         > ................................
>>         > rewrite target: location(monkd, timed2)
>>         > rewrite point: location(monkd, timed2)
>>         > result: locationu2
>>         > ................................
>>         > rewrite target: location(monku, timeu2) == location(monkd,
>>         timed2)
>>         > rewrite point: location(monku, timeu2) == location(monkd,
>>         timed2)
>>         > result: true
>>         > ................................
>>         > result Bool: true
>>         > rewrite time: 2ms       parse time: 2ms
>>         > <<<
>>         > I'm wondering about the different ways/orders of evaluation
>>         in MAUDE and
>>         > BOBJ. Why does MAUDE evaluate the way it does? Is it to make
>>         it faster?
>>         > -Esther
>>         > On 14 December 2010 15:15, Michael Katelman
>>         
>> <katelman AT uiuc.edu
>>  
>> <mailto:katelman AT uiuc.edu>>
>>  wrote:
>>         >>
>>         >> Esther,
>>         >>
>>         >> At least regarding the evaluation of
>>         >>
>>         >> location(monku, timeu2) == location(monkd, timed2)
>>         >>
>>         >> to false, what's happening is that on the right-hand side
>>         of the ==,
>>         >> Maude is first applying "eq timed2 = timeu2", yielding
>>         >> "location(monkd, timeu2)", which is no longer reducible. This
>>         >> essentially means that the code is not confluent, an
>>         assumption needed
>>         >> for Maude to work correctly (perhaps OBJ doesn't require
>>         this?).
>>         >>
>>         >> If you're not already familiar with it, note that Maude has
>>         a tracing
>>         >> command so that you can see exactly what it's doing
>>         step-by-step. You
>>         >> just type "set trace on ." before issuing commands to the Maude
>>         >> interpreter.
>>         >>
>>         >> -Michael
>>         >>
>>         >> On Tue, Dec 14, 2010 at 6:36 AM, esther loeliger
>>         >> 
>> <estherloeliger AT gmail.com
>>         
>> <mailto:estherloeliger AT gmail.com>>
>>  wrote:
>>         >> > Hi,
>>         >> > I'm fairly new to MAUDE. My first Maude program
>>         unfortunately yielded
>>         >> > results that seemed a bit odd -- I was expecting 'true'
>>         and got 'false'.
>>         >> > It's a very simple implementation of the Monk who meets
>>         himself
>>         >> > (http://markturner.org/blending.html). When I installed
>>         BOBJ and ran the
>>         >> > same code, I only had to adjust one keyword, cq (BOBJ)
>>         instead of ceq
>>         >> > (MAUDE).
>>         >> > Here is the MAUDE code:
>>         >> > maudevsbobj.maude:
>>         >> >
>>         >> >
>>         
>> -----------------------------------------------------------------------------------
>>         >> > th MONK-ON-MOVE is
>>         >> > protecting BOOL .
>>         >> > sorts Monk Time-Of-Day Location-On-Path .
>>         >> > op location : Monk Time-Of-Day -> Location-On-Path .
>>         >> > op meets : Monk Monk Time-Of-Day Time-Of-Day Location-On-Path
>>         >> > Location-On-Path -> Bool .
>>         >> > vars M1 M2 : Monk .
>>         >> > vars T1 T2 : Time-Of-Day .
>>         >> > vars L1 L2 : Location-On-Path .
>>         >> > ceq meets(M1,M2,T1,T2,L1,L2) = true if M1 =/= M2 and T1
>>         == T2 and L1 ==
>>         >> > L2 .
>>         >> > endth
>>         >> >
>>         >> > th MONK-ON-MOVE-UP is
>>         >> > including MONK-ON-MOVE .
>>         >> > op monku : -> Monk .
>>         >> > ops timeu1 timeu2 timeu3 : -> Time-Of-Day .
>>         >> > ops locationu1 locationu2 locationu3 : -> Location-On-Path .
>>         >> > eq location(monku,timeu1) = locationu1 .
>>         >> > eq location(monku,timeu2) = locationu2 .
>>         >> > eq location(monku,timeu3) = locationu3 .
>>         >> > endth
>>         >> >
>>         >> > th MONK-ON-MOVE-DOWN is
>>         >> > including MONK-ON-MOVE .
>>         >> > op monkd : -> Monk .
>>         >> > ops timed1 timed2 timed3 : -> Time-Of-Day .
>>         >> > ops locationd1 locationd2 locationd3 : -> Location-On-Path .
>>         >> > eq location(monkd,timed1) = locationd3 .
>>         >> > eq location(monkd,timed2) = locationd2 .
>>         >> > eq location(monkd,timed3) = locationd1 .
>>         >> > endth
>>         >> >
>>         >> >
>>         >> > th MONK-MEETS-HIMSELF is
>>         >> > protecting BOOL .
>>         >> > including ( MONK-ON-MOVE-UP + MONK-ON-MOVE-DOWN ) .
>>         >> > eq locationd1 = locationu3 .
>>         >> > eq locationd2 = locationu2 .
>>         >> > eq locationd3 = locationu1 .
>>         >> > eq timed1 = timeu1 .
>>         >> > eq timed2 = timeu2 .
>>         >> > eq timed3 = timeu3 .
>>         >> > endth
>>         >> >
>>         >> > ***> red in MONK-MEETS-HIMSELF :
>>         >> > meets(monku,monkd,timeu2,timed2,locationu2,locationd2) .
>>         should be true
>>         >> > red in MONK-MEETS-HIMSELF :
>>         >> > meets(monku,monkd,timeu2,timed2,locationu2,locationd2) .
>>         >> > ***> red in MONK-MEETS-HIMSELF :
>>         >> > meets(monku,monkd,timeu2,timed2,locationu2,locationd3) .
>>         should be false
>>         >> > red in MONK-MEETS-HIMSELF :
>>         >> > meets(monku,monkd,timeu2,timed2,locationu2,locationd3) .
>>         >> > ***> red location(monku,timeu2) == location(monkd,timed2)
>>         . should be
>>         >> > true
>>         >> > red location(monku,timeu2) == location(monkd,timed2) .
>>         >> > ***> location(monkd,timed2) . should be locationd2
>>         >> > red location(monkd,timed2) .
>>         >> >
>>         >> >
>>         
>> -----------------------------------------------------------------------------------
>>         >> > and here is the BOBJ code:
>>         >> > maudevsbobj.bob
>>         >> >
>>         >> >
>>         
>> -----------------------------------------------------------------------------------
>>         >> > th MONK-ON-MOVE is
>>         >> > protecting BOOL .
>>         >> > sorts Monk Time-Of-Day Location-On-Path .
>>         >> > op location : Monk Time-Of-Day -> Location-On-Path .
>>         >> > op meets : Monk Monk Time-Of-Day Time-Of-Day Location-On-Path
>>         >> > Location-On-Path -> Bool .
>>         >> > vars M1 M2 : Monk .
>>         >> > vars T1 T2 : Time-Of-Day .
>>         >> > vars L1 L2 : Location-On-Path .
>>         >> > cq meets(M1,M2,T1,T2,L1,L2) = true if M1 =/= M2 and T1 ==
>>         T2 and L1 ==
>>         >> > L2 .
>>         >> > endth
>>         >> > th MONK-ON-MOVE-UP is
>>         >> > including MONK-ON-MOVE .
>>         >> > op monku : -> Monk .
>>         >> > ops timeu1 timeu2 timeu3 : -> Time-Of-Day .
>>         >> > ops locationu1 locationu2 locationu3 : -> Location-On-Path .
>>         >> > eq location(monku,timeu1) = locationu1 .
>>         >> > eq location(monku,timeu2) = locationu2 .
>>         >> > eq location(monku,timeu3) = locationu3 .
>>         >> > endth
>>         >> > th MONK-ON-MOVE-DOWN is
>>         >> > including MONK-ON-MOVE .
>>         >> > op monkd : -> Monk .
>>         >> > ops timed1 timed2 timed3 : -> Time-Of-Day .
>>         >> > ops locationd1 locationd2 locationd3 : -> Location-On-Path .
>>         >> > eq location(monkd,timed1) = locationd3 .
>>         >> > eq location(monkd,timed2) = locationd2 .
>>         >> > eq location(monkd,timed3) = locationd1 .
>>         >> > endth
>>         >> > th MONK-MEETS-HIMSELF is
>>         >> > protecting BOOL .
>>         >> > including ( MONK-ON-MOVE-UP + MONK-ON-MOVE-DOWN ) .
>>         >> > eq locationd1 = locationu3 .
>>         >> > eq locationd2 = locationu2 .
>>         >> > eq locationd3 = locationu1 .
>>         >> > eq timed1 = timeu1 .
>>         >> > eq timed2 = timeu2 .
>>         >> > eq timed3 = timeu3 .
>>         >> > endth
>>         >> > ***> red in MONK-MEETS-HIMSELF :
>>         >> > meets(monku,monkd,timeu2,timed2,locationu2,locationd2) .
>>         should be true
>>         >> > red in MONK-MEETS-HIMSELF :
>>         >> > meets(monku,monkd,timeu2,timed2,locationu2,locationd2) .
>>         >> > ***> red in MONK-MEETS-HIMSELF :
>>         >> > meets(monku,monkd,timeu2,timed2,locationu2,locationd3) .
>>         should be false
>>         >> > red in MONK-MEETS-HIMSELF :
>>         >> > meets(monku,monkd,timeu2,timed2,locationu2,locationd3) .
>>         >> > ***> red location(monku,timeu2) == location(monkd,timed2)
>>         . should be
>>         >> > true
>>         >> > red location(monku,timeu2) == location(monkd,timed2) .
>>         >> > ***> location(monkd,timed2) . should be locationd2
>>         >> > red location(monkd,timed2) .
>>         >> >
>>         >> >
>>         
>> -----------------------------------------------------------------------------------
>>         >> > Here are my results:
>>         >> > MAUDE:
>>         >> >
>>         >> >
>>         
>> -----------------------------------------------------------------------------------
>>         >> > 
>> esther@ubuntu:~/maude/samples$
>>  maude
>>         >> >     \||||||||||||||||||/
>>         >> >   --- Welcome to Maude ---
>>         >> >     /||||||||||||||||||\
>>         >> >    Maude 2.5 built: May  7 2010 18:28:32
>>         >> >    Copyright 1997-2010 SRI International
>>         >> >   Tue Dec 14 12:20:33 2010
>>         >> > Maude> in maudevsbobj.maude
>>         >> > ==========================================
>>         >> > th MONK-ON-MOVE
>>         >> > ==========================================
>>         >> > th MONK-ON-MOVE-UP
>>         >> > ==========================================
>>         >> > th MONK-ON-MOVE-DOWN
>>         >> > ==========================================
>>         >> > th MONK-MEETS-HIMSELF
>>         >> > ==========================================
>>         >> > ***> red in MONK-MEETS-HIMSELF :
>>         >> > meets(monku,monkd,timeu2,timed2,locationu2,
>>         >> >     locationd2) . should be true
>>         >> > ==========================================
>>         >> > reduce in MONK-MEETS-HIMSELF : meets(monku, monkd,
>>         timeu2, timed2,
>>         >> > locationu2,
>>         >> >     locationd2) .
>>         >> > rewrites: 8 in 0ms cpu (0ms real) (~ rewrites/second)
>>         >> > result Bool: true
>>         >> > ==========================================
>>         >> > ***> red in MONK-MEETS-HIMSELF :
>>         >> > meets(monku,monkd,timeu2,timed2,locationu2,
>>         >> >     locationd3) . should be false
>>         >> > ==========================================
>>         >> > reduce in MONK-MEETS-HIMSELF : meets(monku, monkd,
>>         timeu2, timed2,
>>         >> > locationu2,
>>         >> >     locationd3) .
>>         >> > rewrites: 7 in 0ms cpu (0ms real) (~ rewrites/second)
>>         >> > result Bool: meets(monku, monkd, timeu2, timeu2,
>>         locationu2, locationu1)
>>         >> > ==========================================
>>         >> > ***> red location(monku,timeu2) == location(monkd,timed2)
>>         . should be
>>         >> > true
>>         >> > ==========================================
>>         >> > reduce in MONK-MEETS-HIMSELF : location(monku, timeu2) ==
>>         >> > location(monkd,
>>         >> >     timed2) .
>>         >> > rewrites: 3 in 0ms cpu (0ms real) (~ rewrites/second)
>>         >> > result Bool: false
>>         >> > ==========================================
>>         >> > ***> location(monkd,timed2) . should be locationd2
>>         >> > ==========================================
>>         >> > reduce in MONK-MEETS-HIMSELF : location(monkd, timed2) .
>>         >> > rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second)
>>         >> > result Location-On-Path: location(monkd, timeu2)
>>         >> > Maude>
>>         >> >
>>         >> > and
>>         >> > BOBJ:
>>         >> >
>>         >> >
>>         
>> -----------------------------------------------------------------------------------
>>         >> > 
>> esther@ubuntu:~/bobj$
>>  java -cp bobj0.9/bobj.jar bobj.BOBJ
>>         >> >                      \|||||||||||||||||/
>>         >> >                    --- Welcome to BOBJ ---
>>         >> >                      /|||||||||||||||||\
>>         >> >       BOBJ version 0.9.255 built: Tue Nov 29 16:53:20 PST
>>         2005
>>         >> >                University of California, San Diego
>>         >> >                   Tue Dec 14 11:38:48 GMT 2010
>>         >> > BOBJ> in maudevsbobj.bob
>>         >> > ==========================================
>>         >> > th MONK-ON-MOVE
>>         >> > ==========================================
>>         >> > th MONK-ON-MOVE-UP
>>         >> > ==========================================
>>         >> > th MONK-ON-MOVE-DOWN
>>         >> > ==========================================
>>         >> > th MONK-MEETS-HIMSELF
>>         >> > ==========================================
>>         >> > ***>  red in MONK-MEETS-HIMSELF :
>>         >> > meets(monku,monkd,timeu2,timed2,locationu2,locationd2) .
>>         should be true
>>         >> > ==========================================
>>         >> > reduce in MONK-MEETS-HIMSELF : meets(monku, monkd,
>>         timeu2, timed2,
>>         >> >     locationu2, locationd2)
>>         >> > result Bool: true
>>         >> > rewrite time: 39ms       parse time: 4ms
>>         >> > ==========================================
>>         >> > ***>  red in MONK-MEETS-HIMSELF :
>>         >> > meets(monku,monkd,timeu2,timed2,locationu2,locationd3) .
>>         should be false
>>         >> > ==========================================
>>         >> > reduce in MONK-MEETS-HIMSELF : meets(monku, monkd,
>>         timeu2, timed2,
>>         >> >     locationu2, locationd3)
>>         >> > result Bool: meets(monku, monkd, timeu2, timeu2, locationu2,
>>         >> >     locationu1)
>>         >> > rewrite time: 7ms       parse time: 4ms
>>         >> > ==========================================
>>         >> > ***>  red location(monku,timeu2) ==
>>         location(monkd,timed2) . should be
>>         >> > true
>>         >> > ==========================================
>>         >> > reduce in MONK-MEETS-HIMSELF : location(monku, timeu2) ==
>>         >> > location(monkd,
>>         >> >     timed2)
>>         >> > result Bool: true
>>         >> > rewrite time: 1ms       parse time: 2ms
>>         >> > ==========================================
>>         >> > ***>  location(monkd,timed2) . should be locationd2
>>         >> > ==========================================
>>         >> > reduce in MONK-MEETS-HIMSELF : location(monkd, timed2)
>>         >> > result Location-On-Path: locationu2
>>         >> > rewrite time: 1ms       parse time: 0ms
>>         >> > BOBJ>
>>         >> >
>>         >> >
>>         
>> -----------------------------------------------------------------------------------
>>         >> > In particular, it seemed odd, that
>>         >> > location(monku, timeu2) == location(monkd, timed2) .
>>         >> > evaluated to 'false' in MAUDE, whereas I expected it to
>>         evaluate to
>>         >> > 'true',
>>         >> > as in BOBJ.
>>         >> > Any hint on why MAUDE evaluates to 'false' would be very much
>>         >> > appreciated!
>>         >> > Best regards,
>>         >> > Esther
>>         >> >
>>         >> >
>>         >> > _______________________________________________
>>         >> > Maude-help mailing list
>>         >> > 
>> Maude-help AT cs.uiuc.edu
>>  
>> <mailto: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
>>  
>> <mailto: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


This message has been scanned for content and viruses by the DIT Information 
Services E-Mail Scanning Service, and is believed to be clean. 
http://www.dit.ie