0

私の次の主張に対する反例が常にある理由について、私は本当に混乱しています。

//assertions must NEVER by wrong
assert Symmetric{
all r: univ -> univ | some ~r iff (some x, y: univ | x not in y and y not in x and 
                                  (x->y in r) and (y->x in r))
}

check Symmetric

反例は、常に univ セット内の 1 つの要素を示しています。ただし、y にない ~r iff x と x にない y があると指定したため、これは当てはまりません。唯一の要素は、このステートメントを満たすべきではありません。

しかし、モデルが私の主張の反例を示し続けるのはなぜでしょうか?

---INSTANCE---
integers={}
univ={Univ$0}
Int={}
seq/Int={}
String={}
none={}
this/Univ={Univ$0}
skolem $Symmetric_r={Univ$0->Univ$0}

いくつかのガイダンスに本当に感謝します！

4

1 に答える 1

1

Alloyでは、アサーションは論理文（モデルのプロパティ）の正確さをチェックするために使用され、モデルに常に保持される必要があるプロパティを指定するためには使用されません。だからあなたはそれを指定しませんでした

xがyになく、yがxにない場合は〜r iff

代わりに、Alloyにすべての二項関係について正しいかどうかを尋ね、Alloyはそれが正しくrないsome ~r iff x not in y and y not in x [...]と答え、そのプロパティが成り立たない具体的な例（反例）を示しました。

他のいくつかのポイント

  • some ~r「rが対称である」という意味ではありません。それは単に、の転置がr空ではないことを意味しますが、これは同じではありません。二項関係は、転置と等しい場合は対称であるため、それr = ~rを表現するために書くことができます。

  • あなたの代わりにsome x, y: univ | x not in y and y not in x and [...]同等に書くことができますsome disj x, y: univ | [...];

  • ただし、そのsome式は実際には対称性を表現していません。これは、「x->yとy->xの両方がrに含まれるようなx、yがいくつかある」ためです。代わりに、「すべてのx、yについて、x-> yがrにある場合、y->xもrにある」のように言いたいと思います。

于 2012-11-26T15:37:47.153 に答える