履修条件が輪になる
Alloy とは、物と物の関係を集合として書き、決まりが破れる小さな例を機械に探させる言語です。見つかった反例は、点と矢印の図として読めます。
大学の履修条件には、「科目Aの前に科目Bを取る」という関係があります。AとBが互いに前提だと、誰もどちらも履修できません。この輪を、Alloy は反例として見つけます。
このレッスンのゴール
メモ
Alloy が示す反例を、集合と関係として読める。
重要な言葉
| ことば | いみ | れい |
|---|---|---|
| 集合 | 同じ種類の物の集まり | sig Course |
| 関係 | 物と物のつながり | prereq |
| fact | モデルが必ず守る決まり | |
| assert | 成り立つはずの主張。check で調べる | |
| スコープ | 調べる物の数の上限 | for 4 |
| インスタンス | 決まりを満たす、小さな具体例 |
学生が入力するセルは、このプレビューでは空白です。
sigは集合、関係は線になる
sig Course { prereq: set Course } は、「科目の集合 Course があり、各科目に前提の科目の集まり prereq がある」という意味です。
fact noSelf は、自分自身を前提にする科目はない、という決まりです。この決まりが、輪を防ぐのに足りるかどうかを、assert で調べます。
履修条件のモデル
sig Course { prereq: set Course }
fact noSelf { no c: Course | c in c.prereq }
assert NoTwoLoop { no disj a, b: Course | a in b.prereq and b in a.prereq }
check NoTwoLoop for 4
assertとcheckは反例を探す
assert NoTwoLoop は、「別々の2科目 a と b が、互いに前提になることはない」という主張です。disj は、別々の2つ、という意味です。
check NoTwoLoop for 4 は、科目が4つまでの世界を全部調べて、この主張が破れる例を探します。見つかれば SAT、なければ UNSAT です。
練習用のフォルダを作る
mkdir -p practice/coursesここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
モデルのファイルを書く
printf '%s\n' "sig Course { prereq: set Course }" "fact noSelf { no c: Course | c in c.prereq }" "assert NoTwoLoop { no disj a, b: Course | a in b.prereq and b in a.prereq }" "check NoTwoLoop for 4" > practice/courses/courses.alsここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
Alloyに反例を探させる
alloy practice/courses/courses.alsここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
反例の読み方
出力の Course$0 と Course$1 は、名前のない2つの科目です。Course$0->Course$1 は、0番の前提に1番がある、という1本の線です。
線が2本あり、0から1へ、1から0へ向いています。つまり、2科目が互いに前提です。skolem の行は、反例で a と b になった科目を示します。
出力の行の意味
| 行 | 意味 |
|---|---|
| SAT | 反例が見つかった |
| this/Course={...} | 反例に出てきた科目 |
| prereq={A->B, ...} | A の前提に B がある線 |
| skolem $NoTwoLoop_a | 反例で a になった科目 |
学生が入力するセルは、このプレビューでは空白です。
factに輪の禁止を足して直す
直し方は、輪そのものを禁じる fact を足すことです。c.^prereq は、c から前提をたどって行ける科目の全部です。前提の前提、そのまた前提も入ります。
no c: Course | c in c.^prereq は、どの科目も、たどって自分へ戻らない、という決まりです。run Chain は、前提が1つでもある例を探します。
直したモデルを書く
printf '%s\n' "sig Course { prereq: set Course }" "fact noLoop { no c: Course | c in c.^prereq }" "assert NoTwoLoop { no disj a, b: Course | a in b.prereq and b in a.prereq }" "check NoTwoLoop for 4" "run Chain { some prereq } for 3" > practice/courses/fixed.alsここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
直したモデルを調べる
alloy practice/courses/fixed.alsここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
よくある間違い
注意
check が UNSAT なら、これで安心、と思いがちです。fact が強すぎて、誰もいない世界しか許さなくても、check は UNSAT になります。同じモデルで run を動かし、本物の例が出ることを確かめましょう。出なければ、モデルが空です。
さらに挑戦: 輪の長さを変える
fixed.als を別の名前でコピーし、fact を fact noSelf { no c: Course | c in c.prereq } に戻しましょう。主張を、3科目の輪を禁じるものに書き換えて、check を調べます。
SAT になれば、図を描いてみましょう。何科目が、どの向きの輪になっているかを、言葉で説明してください。