alloy - Alloy 4の関数と述語の違いは?

Question

Alloy 4 の述語と関数の違いを理解するのに苦労しています。Software Abstractions のセクション 4.5.2 を読みましたが、まだ明確ではありません。誰かが私を理解するのを手伝ってもらえますか?

Answer 1

関数は、すべての呼び出しサイトでインライン化されるパラメーター化された式を単純に表します。

述語は式、つまりブール式を表すので、その意味ではブール式を返す関数のようなものです。もう 1 つの違いは、Alloy では、Alloy の「run」および「check」コマンドを使用して述語を「run」および「check」できることです。述語を実行すると、Alloy はその述語が成立するモデルを見つけるように指示されますが、述語をチェックすると、その述語が成立しないモデルが存在するかどうかを確認するよう Alloy に指示されます。