3

Alloy 4.2 のリリース ノートによると、整数に関連するセマンティクスの変更があります。これらの変更は、Alloy book の演習 A.1.6 に影響を与えるようです。

この演習では、次のコードがベースとして提供されます (問題を示すために最後に「Int」を追加しました)。「show」述語を実行すると、ビジュアライザーはインスタンスを表示しますが、このインスタンスには、整数に加えて、さらに 2 つのアトム「Univ0」と「Univ1」が含まれています。

module exercises/spanning

pred isTree(r: univ->univ) {}
pred spans(r1, r2: univ->univ) {}

pred show(r, t1, t2: univ->univ) {
    spans[t1,r] and isTree[t1]
    spans[t2,r] and isTree[t2]
    t1 != t2
}
run show for 3 Int

この 2 つのアトム「Univ0」と「Univ1」の意味は何ですか? なぜ彼らはそこにいるのですか？これらは、Alloy 4.1.10 で実行された同じコードでは表示されません。

4

1 に答える 1

1

ユーザー定義のシグがない場合、Alloy は「Univ」と呼ばれる新しいシグを自動的に合成します。これは、シグを導入しなくてもユニバース全体に式を記述できるため、便利な機能です。

Int のスコープを明示的に指定すると、指定されたスコープ内のすべての Int アトムが確実にユニバースに含まれます。さらに、ユーザー定義の sig がない場合は、合成された Univ sig も作成されます。Int のスコープが明示的に使用されている場合に、Univ sig を合成することが理にかなっているのかどうかは議論の余地があります。

問題を回避するには、いくつかのオプションがあります。

  1. グラフ ノードのタイプを気にしない場合 (つまり、ノードを明示的に Int にしたくない場合) は、単純に実行コマンドを次のように変更できます。

    run show for 3の代わりにrun show for 3 Int。

    これを行うと、Int アトムがなくなり、Univ アトムだけになります。Univ sig が気に入らない場合は、単純に新しい sig を導入してください。たとえば、sig Node {}この場合、すべてのアトムは 型になりNodeます。

  2. グラフを整数のみにしたい場合は、すべての述語に変更できますuniv->univ。Int->Int

  3. ユニバースに Int アトムのみを含めたい場合 (この場合univ->univ、述語を保持できます)、ダミーの署名を導入し、カーディナリティが 0 であることを保証するファクトを追加できます。

    sig Dummy {}
fact { no Dummy }

    この小さな変更により、Univ sig が自動的に合成されず、モデルの残りの部分に影響を与えないことが保証されます。

お役に立てれば。

于 2012-10-02T15:47:04.610 に答える