Alloyガール 迷宮編 3

Alloyの制約パラグラフのリファクタリング

僕: 今日はちょっとしたTipsを紹介しようかなと思う
Alloy: 前回も本題の迷路の生成は進んでなかったと思うけど
僕: いちおう進捗はあるんだけど、その中で気がついたこととか記録しておきたくてね

僕: 迷宮編1 で作ったsimple_maze.alsの制約のうちいくつかは、もっとシンプルに書けるということに気がついたんだ。たとえばこれ

  // 全ての位置が paths に含まれている
  all col: Col, row: Row | (col -> row) in paths[Col, Row]

僕: わざわざ all e | F の形式で書いてるけど、これって結局 Col -> Row が paths[Col, Row] に含まれるってことだからこれでいいはず

  // 全ての位置が paths に含まれている
  Col -> Row in paths[Col, Row]

Alloy: なるほど。おそらく出力されるSATも同一になると思うよ
僕: ただ、Alloyに慣れないうちはこういう書き換えにも慎重になるんだよ。よく勘違いで解がなくなってしまったり、思っていたような制約が効かなくなるという失敗をやるからね
Alloy: わたしは言われた通りに解析しているだけなのだけど
僕: うん、間違っているのは僕なんだけど、まあともかく間違えてないか確認しながら書き換えたい。実はAlloy本を読み返しているとそういうときに使える方法がちゃんと書かれてたよ

  pred constrain1 {
    all col: Col, row: Row | (col -> row) in paths[Col, Row]
  }
  pred constrain2 {
    Col -> Row in paths[Col, Row]
  }
  assert checkConstrainEquality {
    constrain1 iff constrain2
  }
  check checkConstraintEquality for 10 Col, 10 Row

僕: iff は論理式がどちらも真か、どちらも偽の時に真になる二項演算子だ
Alloy: <=> という演算子を使うこともできるわね
僕: まあようするにどちらの制約も同じ意味の時に真になる。これを check で反例がないか確認して、みつからなければ大丈夫だろうと。もちろん指定したスコープの範囲内ではみつからないということだけど
Alloy: 厳密に言うと、fact や signature のブロックにあるその他の制約の元においては同じ結果になるということを確認したことになるのだけどね
僕: というと?
Alloy: つまり、simple_maze.alsに上のassert+checkを追加して検証した場合、"paths の連結は反射的"などのその他の制約を満たすような組み合わせのpathsしか検証の対象にならないのだから、"一般的に"2つの論理式が同じ意味かどうか確認しているわけではないということね
僕: なるほど、そうか。"一般的"に置き換え可能かどうかチェックしようと思ったら上のような検証のためだけのファイルを作ってチェックしたほうがいいんだね
Alloy: 今回のケースでは問題ないようだけどね

Ruby: (今回出番がなかった…)