3

モジュールに sig B に関連する sig A があるとします。

いくつかのインスタンスがあると想像してください:

A$1 -> B$1   , A$2 -> B$2

と

A$1 -> B$2   , A$2 -> B$1

このインスタンスのみが生成されるように、B$1 と B$2 は (特定の条件下で) 同等であることを表現したいと思います。A$1 -> B , A$2 -> B.

解決策の 1 つは、sig B を宣言するときにキーワード「one」を使用することかもしれませんが、B には複数のフィールドがあり、B アトムが必ずしも equal ではないため、私の場合は機能しません。つまり、2 つのアトムは、同じ値のフィールドを持つ場合にのみ同等です。

理想的には、 B の番号付けを削除したいのですが、それでもいくつかのアトム B を持つことができます。

4

2 に答える 2

4

Alloy Analyzer では、後続のインスタンスの生成方法 (または対称性を破る方法) をあまり制御できないため、通常、これらの問題をモデル レベルで回避する必要があります。

あなたの例では、おそらくこれが正しいモデルです

sig B{}

one sig BA extends B {}

sig A {
  b: one BA
}

run { #A=2 }
于 2013-06-18T14:57:46.303 に答える
1

最初に、説明した 2 つのインスタンスは同等であると言いますが、表面的なレベルでは、A$1 と A$2 の値が異なるように見えます。次に、「2つのアトムは、フィールドが同じ値である場合にのみ同等です」と言います。それが同等の定義である場合、2 つのインスタンスは同等ではありません。2 つのインスタンスが等しい場合、定義は必要なものをキャプチャしていません。

（1）Bアトムは（1a）常に同等であるか、（1b）特定の状況下で同等であり、（2）すべてのフィールドが同一または同等の値を持っている場合、Aアトムは同等であるという意味のように聞こえます. そして、同等の A アトムを禁止したい場合と同様です。その場合、あなたの仕事は次のとおりです。

  • 2 つの B 要素が同等である場合にのみ true となる述語を定義します。
  • 2 つの A 要素が等しい場合にのみ true となる述語を定義します。
  • インスタンス内の 2 つの A アトムが同等ではないことを指定する述語 (またはファクト) を定義します。

問題が、アナライザーがモデルのインスタンスを示しているだけで、それらが互いに興味深いほど区別されていないということである場合は、Aleksandar Milicevic の回答を参照してください。

于 2013-06-18T16:12:06.323 に答える