Alloy Analyzer はじめの一歩（デザートは週に三度まで。）

モデリング検査ツール Alloy Analyzer を使いたい！のエントリ。第三回目です。

今回は、自己参照用の関連を定義してみました。

例えば、変更履歴を管理するために、「自身のひとつ前のレコード」の id を、外部キーとして保持するようなケースです。
こういった場合当然

• 同一のレコードが「ひとつ前のレコード」として、複数のレコードから参照されることは有り得ない。
• 循環参照は有り得ない。

ので、この制約を満たしたうえでの定義です。
disj というキーワードが役に立ってくれたけど、こういう使い方でいいのかな。

自己参照用の関連

module ref_myself
sig Current {
  // 複数インスタンスから参照されるpreviousは無い
  previous: disj lone Current
}
fact HistoryOfChain {
  // 循環参照禁止
  no c: Current | c in c.^previous
}
run {}

fact 中に出てくる、 "^" 記号は、Alloyでは、
『関係を辿って辿り着ける要素(関係)すべて』
を示しています。数学用語でいうところの「推移閉包」ってやつらしいんですが、ググればググるほど何なのか解りませんでした。
（数学に関することをググると、いつもそうなる）
なので、『関係を辿って辿り着けるモノすべて』
って丸覚えしたところで、あえて思考を停止することに決めました。