AlloyのRun
Predicateを実行するための命令
code:alloy
run show for 4 but 1 Book
上記だとshowが述語に相当する
上記だと本体記述を省略してるので常に真になる
真となる組み合わせがある場合、具体的なobjectの集合を返す
forやbutはなに？mrsekut.icon
インスタンスを探索する範囲を限定するスコープの指定
上記のコードだと、Book以外のsigはたかだか3つのobjectに限定し、Bookは1つのobjectに限定する、というのを表す
これのことをコマンドと呼んでる？