問題タブ [alloy]

私が次のことをするとしましょう：

順序付け/最初にはどのような値がありますか? 未定義ですか？曖昧さをなくすためにモジュール エイリアスを使用する必要がありますか?

少し前にSoftware Abstractionsの第 2 版を入手しましたが、関数名の綴りについて記憶を新たにする必要があったとき、elems「ああ、よかった、判読しにくい手書きの文字を読もうとする代わりに、新しい版を確認できる」と思いました。初版の見返しにある注記。」

しかし、インデックスに「seq」や「elems」、その他のヘルパー関数の名前が見つかりません。またseq、付録 B の言語リファレンスでキーワードについての言及も見当たりません。

次の 1 つまたは複数に該当する可能性があります。どれの？

• 私は何かが欠けています。(なに? どこ?)
• このキーワードは、他の単項演算子のseqように厳密にはキーワードではないため、付録 B ではカバーされていません。set（説明してください！）
• シーケンスのサポートは、第 2 版が発行された後に Alloy 4 に追加されたため、クイック ガイドの Alloy 4 の新機能の説明とWeb サイトの Alloy 4 の文法を参照して、本を補足する必要があります。(ああ、わかりました。ページは遅く、ビットは高速です。)
• 他の ...

ここで一般的に役立つ質問をしようとすると、私は尋ねていると思います: Alloy Analyzer 4.2 (または任意の 4.*) によって実装された言語とソフトウェア抽象化第 2 版で定義された言語との間の関係は正確には何ですか?

Alloy Analyzer を使用して、特定のスコープ内の述語からすべてのソリューションを列挙したいと考えています。Alloy はこの機能をサポートしていますか? 可能であれば、コマンドラインから呼び出す方法は?

ありがとうございました

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

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

と

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

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

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

以下を含む合金モデルがあります。

2 つの署名を等しくするにはどうすればよいですか?

次の合金モデルを検討してください。

このモデルのすべてのインスタンスがシグニチャー C の 7 つのアトムを持っている理由を理解run show for 7しています (まあ、それは正確ではありません。util/ordering が伝えるため、順序付けられたシグニチャーは常にスコープが許す限り多くのアトムを持つことを理解しています)。私はそうです。しかし、それは理由とまったく同じではありません。)

しかし、このモデルのインスタンスに署名 B のアトムがないのはなぜでしょうか? これは、util/ordering で実行される特別な処理の副作用ですか? (意図的? 意図的でない?) util/ordering は、最上位の署名にのみ適用されることを意図していますか?

それとも、私が行方不明になっていることが他にあるのでしょうか?

this からのモデルでは、これは抽象化されています。B と C の和集合に A のような名前を付けたいと思っています。空でない。現時点では、これらの目標のいずれか 2 つを達成できるようです。3つすべてを同時に管理する方法はありますか？

run show for 3 but 3 B, 3 C[補遺: 指定することで、私の 3 つの目標が達成されることに気付きました。対照的に、run show for 2 but 3 Bインスタンスはまったく生成されません。おそらく、スコープ指定のセマンティクスをよりよく理解する必要があります。]

// .. 同様に項目 4 から 10

選択したアイテムの価格の合計が最小になるように、n (n = 1 ～ 10) のアイテムを選択することはできますか?

n=3 アイテムの場合、結果は item1、item2、item3 になります。

可能であれば、このことを Alloy でどのように書くのですか?

親切な返信をありがとうございました。