Maude-help mailing list

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

Dear Esther,

I don't think you can move so easily from BOBJ into Maude. Maude is a rewrite 
engine. To do something like monku == monkd Maude tries to simplify both 
monku and monkd using the equations as rewrite rules until no further 
equation can be applied. If they reduce to the same term then true is 
returned. 

When rewriting 
  location(monku, timeu2) == location(monkd, timed2) .
the term on the left is rewriten to 
  locationu2
and the one on the right to 
  location(monkd, timeu2)
Since they are different, false is given as result. 

Cheers, 

Francisco


El 14/12/2010, a las 13:36, esther loeliger escribió:

> 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