嵌套 OCL for Alls

Question

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

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

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

这是 Class 图：

有人可以提供上述公式的OCL表示吗

Answer 1

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

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

Answer 2

已回答 here 中的问题。

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

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

我觉得这太笨重了！但它似乎是这样！