3

このモデルに一貫性がない理由を知りたいのですが。次のタプルをシェービングに入れることができます。

shaves = {(man,man)} sig Man {shaves: set Man} one sig Barber extends Man {} 

fact {
   Barber.shaves = (m:Man |m not in m.shaves}
}

Barber.shavesは0タプルを生成します。この場合、事実は有効である必要があります。では、なぜ私のモデルに一貫性がないことを許可するのですか？

これについてのアドバイスを本当にいただければ幸いです。

4

2 に答える 2

3

さて、ここに解決策があります。アイデアは本当に単純です、そして私は著者が彼らの本でこれを本当に説明するべきだと思います。

混乱の核心は事実の声明にあります。

Barber.shaves = {m：Man | mはm.shavesにありません}

基本的に、上記のステートメントが言っていることは、Barber.shavesのタプルは自分自身を剃ってはならないということです。たとえば、= Barber.shaves = {（m）}の場合、（m、m）はシェーブ関係セットで発生してはなりません（MUST）。また、m：Manは、自分自身を剃らないすべての男性もBarber.shavesにいる必要があることを示しています。

この問題は、Barberインスタンスに到達したときに発生します。床屋がBarber.shavesにない場合は、m：Manに違反します。床屋が含まれている場合、シェービングには{（barber、barber）}が含まれるため、m.shavesにないmに違反します。

これにより、私のような合金の初心者の混乱が解消されることを願っています。

したがって、私の質問の現在のモデルを考えると、alloyはこの事実を満たすインスタンスを作成できません。

于 2012-11-21T13:11:57.137 に答える
3

英語だけを使った簡単な説明があります。

上記の合金の事実は、理髪師 (理髪師は 1 人しかいないためone sig Barber) が剃る男性のセットは、自分で剃らないすべての男性とまったく同じであると述べています。すべての人が自分で剃るか、理髪師に剃られるため、最初は、このステートメントは理にかなっています。

ひっかけ問題は、「理髪師のひげをそるのは誰か」です。床屋が自分でひげを剃らない場合、その事実は理髪師が自分のひげを剃らなければならないことを強制し、これは理髪師が自分でひげを剃らないという仮定と矛盾しています。理髪師が自分でひげをそる場合、その事実は理髪師が理髪師のひげを剃ってはならないことを強制し、これも逆説であり、そのため事例は見つかりません。

于 2012-11-21T15:34:32.667 に答える