問題タブ [alloy]

合金の Web サイトで、署名がセットを定義することを読みました。この定義を考えると、私は以下の合金コードを理解しようとしていました:

署名が実際にセットを定義する場合、セットが単項関係であるのに、署名定義に非常に多くのパラメーターがあるのはなぜですか? 私が間違っているとすれば、この定義をどのように解釈するのでしょうか。

次の例を使用して、誰かが述語を理解するのを手伝ってくれませんか。

上記のコードについて、以下の質問があります。

1）上記の述語が真の場合はどうなりますか？

2）それが偽の場合はどうなりますか？

3）誰かが上記のコードを使用し、コードを通じて述語の意味を明確にする少しの合金コードを見せてもらえますか？

上記の述語をどのように使用するかを理解しようとしています。

以下の定義を考えると：

addr : Name -> some Addr関係で、2 番目の列の名前の多重度はどのくらいなのか、興味がありました。また、以下は可能ですか

2 番目の列で j が複数回発生する可能性があるかどうかを学習しようとしています

本で次の定義を見ました。

どこ

Alloyアナライザーで遊んだ後、これは

Book を引数として指定し、量指定子を使用する 2 番目のアプローチを使用しないことの利点は何ですか?

私は合金での述語の使用を知っていますが、以下の説明に少し驚いていました：

誰かが私に上記を説明してもらえますか？

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

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

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

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

次のような単純なモデルがあるとします: sig P{r:some P} sig Q{} run {} for 2 P, 2 Q

このモデルのインスタンス数を減らすために、合金が対称性を破る述語を生成する方法を知っている人はいますか?

私は合金の高次定量化について読んでいて、次のことを見ました：lone p：some X | F
さて、キーワード'some'がpまたはXを変更するかどうか混乱しています。それは、Xが空でないことを意味するのでしょうか、それともpのカーディナリティが>=1であることを意味するのでしょうか。

以下で

以下はどういう意味ですか？署名の定義とどのように関連していますか？これはsigの関係ですか？

本当に不可解な質問があります。この述語のインスタンスが見つからないようです。以下はコードです。

インスタンスを取得できないのはなぜですか? コードをトレースしたところ、基本的なトレースは次のようになります: init -> together -> unlockopen -> getin.

これらの先行する各述語は、後続の述語の制約を満たす必要があります。では、getin を除く残りの述語のインスタンスを取得できるのはなぜでしょうか。

これについてのガイダンスを本当に感謝します。