uml - 嵌套 OCL forAlls

Question

我在一阶逻辑中有以下公式。

forAll a:A | forAll b :B | if a.r1=b then a.r2=b

简单地说，对于所有类型 A 的对象和所有类型 B 的对象，如果它们与 r1 相关，那么它们也与 r2 相关。

这是类图：

请有人提供上述公式的OCL表示。

Answer 1

我没有方便的方法来测试它，但我认为语法是r1->forall(i | r2->exists(i)).

可能更简单，如果你只想说那r1是 的一个子集r2，你可以声明它。

Answer 2

在这里回答的问题。

我重复答案以遵循堆栈溢出规则：

A.allInstances()->forAll(a | B.allInstances()->forAll(b | a.r1=b implies 
a.r2=b))

这对我来说似乎很笨重！但它似乎是什么！