Maude-help mailing list

[Max Jonas Werner <mail AT makk.es>]

Hi,

I have defined the following module (for modeling the dining philosophers):

mod PHILOSOPH is
        protecting NAT .
        sorts Philo Mode Fork Conf Proc Game .
        subsorts Fork Proc < Conf .
        
        var N : Nat .
        
        ops p_ : Nat -> Philo [ctor] .
        ops f_ : Nat -> Fork [ctor] .
        ops eat think : -> Mode [ctor] .
        op [_,_] : Philo Mode -> Proc [ctor] .
        op __ : Conf Conf -> Conf [ctor assoc comm] .
        
        op C : -> Nat .
        eq C = 2 .
        
        rl [take] : f(N) f(s(N) rem 2) [p(N), think] => [p(N), eat] .
        rl [put] : [p(N), eat] => f(N) [p(N), think] f(s(N) rem 2) .
endm

Here, we have 2 philosophers. The problem is this:

rewrite [1] in PHILOSOPH-CHECK : f 0 f 1 [p 0,think] [p 1,think] .
rewrites: 0 in 0ms cpu (0ms real) (~ rewrites/second)
result Conf: f 0 f 1 [p 0,think] [p 1,think]

Maude does not apply the first rule although it ought to match. Does
anyone have a hint as to why this is so?

Thanks
/max

Attachment: signature.asc
Description: OpenPGP digital signature