AlloyのFact

常に成り立つと仮定する制約を記述する

常に真であるとみなされる

モデル全体に適用される

code:alloy

fact { ... }

fact { F }

fact 名前 { F }

sig S { hogehoge }{ F }

factの中にAlloyのPredicateを含めても良い

試行錯誤の段階ではPredicateにしておいて、確定したらfactに持ち上げる感じかなmrsekut.icon

他には、

runの実行結果を見やすくする

AlloyのRunで解析する際のスコープを狭めることができる

などの補助的な目的で用いることもある

『形式手法入門』.icon p.20