Maude-help mailing list

[esther loeliger <estherloeliger AT gmail.com>]

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