Maude-help mailing list

["Ding, Hui" <huiding AT cs.uiuc.edu>]

Can we specify the following rule in Maude functional module? I cannot figure it out.

 

If PropertyMap (AA, A, B) = BB and PropertyMap (BB, B, C) = CC

Then PropertyMap (AA, A, C) = CC

 

AA stands for a certain property of component A, and BB stands for a certain property of component B.

 "PropertyMap (AA, A, B) = BB" means component A's property AA is mapped to component B's property BB.

That is, the above is a transitive rule.

 

The sort, op, vars declaration is as follows:

 

sort Component .

sort Property .

op PropertyMap: Property Component Component-> Property .

 

vars AA BB CC : Property .

vars A B C : Component.