以下は、2つのデスクトップのAlloy表現です。でfact、私は最初のデスクトップは2個のアイコン、AとBが含まれている、と私は実際にこれを入れて2番目のデスクトップは、1個のアイコン、私はちょうど二つのデスクトップがあることを指定したいのですがA.が含まれていることを指定します。
#Desktop = 2
私が行ったときはrun、コマンドを、私はこのメッセージが表示されました：No instance found。からそれを省略しfact、代わりにrunコマンドでデスクトップの数を指定した場合：
run {} but 2 Desktop
次に、目的のインスタンスが生成されました。どうして？のデスクトップの数を制限すると機能しないのにfact、runコマンドのデスクトップの数を制限すると機能するのはなぜですか？
open util/ordering[Desktop]
sig Desktop {
icons: set Icon
}
abstract sig Icon {}
one sig A extends Icon {}
one sig B extends Icon {}
fact {
first.icons = A + B
first.next.icons = A
}
Alloy Referenceの283ページによると、署名に明示的な境界が指定されておらず、暗黙的な境界が見つからない場合、その署名はデフォルトで最大3つの要素になります。run {#Desktop = 3}デフォルトで動作します。
あなたも持っていopen util/ordering[Desktop]ます。そのモジュールはで始まり、スコープに制約をmodule util/ordering[exactly elem]追加しexactlyます。これは、暗黙の境界が正確に3つの要素であるため、run {#Desktop = 2}失敗することを意味します。追加run {#Desktop = 2} for 2すると、署名ごとに2つの要素への暗黙のバインドが変更されるため、成功します。
この記事はインターネットから収集されたものであり、転載の際にはソースを示してください。
侵害の場合は、連絡してください[email protected]
コメントを追加