AlloyのCheck
AlloyのAssertionが真であるかどうかを確認する
真でない場合は反例を出してくれる
https://alloytools.org/tutorials/online/sidenote-format-check.html
反例がなかった場合
指定されたスコープ内では、反例はなかったということ
反例があった場合
ただし、その反例はShrinkingされてるわけではない
なので、自分でスコープを狭めてCheckする、のような操作は必要
例
code:alloy
check acyclic for 5
ちなみに、acyclicは自分で定義したAlloyのAssertion
/mrsekut-book-4274068587/143 (4.6 コマンドとスコープ)