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宣言するだけです。