Maude-help mailing list

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

Max,

Lefthand sides of rules must be terms in normal form, only constructors. 
Maude reduces a term to its normal form before applying a rule. Try 

> crl [take] : f(N) f(M) [p(N), think] => [p(N), eat] if M == s(N) rem 2.

Cheers,

Paco


On 10/12/2013, at 20:54, Max Jonas Werner wrote:

> 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
> 
> _______________________________________________
> Maude-help mailing list
> Maude-help AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help