avlTree.als に合金モデルがあります。このモデルは、整数演算、特にプラス関数とマイナス関数を使用します。このモデルにはいくつかのアサーションが含まれており、Alloy Analyzer GUI を使用してこれらを適切に実行できます。
test.als に別の合金モデルがあります。このモデルは、(「open avlTree」を使用して) avlTree をインポートし、avlTree モデルの関係についていくつかのアサーションを持ちます。しかし、Alloy Analyzer GUI でこれらのアサーションを実行しようとすると、次のメッセージが表示されます。
構文エラーが発生しました:
「プラス」という名前が見つかりません。
構文エラーへのリンクは、avlTree モデルに移動します。そのため、avlTree モデルの整数演算の使用は、そのモデルを単独で実行すると正常に機能するように見えますが、別のモデルにインポートしようとすると壊れます。これに対する修正はありますか？
Alloy 4.2を実行しています。