Maude-help mailing list

[Rubén Rafael Rubio Cuéllar <rubenrub AT ucm.es>]

Hello Mohamed,

The problem is that the op keyword in the following declaration should be ops.

op inRq exPr exDc exDa inAc inRj : -> Act .
op ini rqd dcd dad acd rjd  : -> Value .

With op, you are declaring a single operator with all these tokens as its name, while with ops, you are declaring an operator for each token (as if you have written op ini : -> Value ., op rqd : -> Value, and so on). For example, with your current file, you can check using reduce ini rqd dcd dad acd rjd . that ini rqd dcd dad acd rjd is successfully parsed as a constant of sort Value, but reduce ini . does not work because ini alone is not a term. The difference between op and ops is explained in Section 3.4 of the Maude manual.

Best regards, Rubén.