Maude-help mailing list

[esther loeliger <estherloeliger AT gmail.com>]

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

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