Maude-help mailing list

[Michael Katelman <katelman AT uiuc.edu>]

Esther,

On Tue, Dec 14, 2010 at 10:50 AM, esther loeliger
<estherloeliger AT gmail.com>
 wrote:
>
>
> ---------- Forwarded message ----------
> From: esther loeliger 
> <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>
>
>
> 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 .

This code is problematic in a way similar to the original. As in the
earlier example, Maude can choose to first evaluate

location(monku, timeu2) --> locationu2

 and then

location(monkd, timed2) --> location(monkd, timeu2)

at which point the new equation wouldn't be applicable.

> 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?

That's a good question to which I unfortunately don't know the answer.

-Michael

> -Esther
>
> On 14 December 2010 15:49, Michael Katelman 
> <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>
>>  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>
>> >  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>
>> >>  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
>> >> > 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
>
>