Alloy time flow model

alloy.als

// まず時間を表すシグネチャを作る。

sig Time {}

// シーケンシャルなものとして設定する

open util/ordering [Time]

// 時間によって変化するものは、

currentKey : keys one -> Time

// などのように、末尾にTimeをつける。各時間にかならず１つ存在するなら "one"、最大で1つ(たかだかひとつ)なら、

lastKey : (Room -> lone Key) -> Time

// とする。時間によって変化する述語には、かならず変化前、変化後の時間を最初のパラメータとして入れる。

pred entry (t, t' : Time, g : Guest, k : Key) {
    // 定義
}

// 初期値を設定する述語

pred init (t : Time) {
    no Guest.keys.t
}

// 時間変化はfactで記述する。ここがすべての時間を司るエントリーコードとなる。

fact Traces {
     first.init
     all t : Time - last | let t' = t.next |
          some g : Guest, k : Key |
               論理
}

// 時間が変化しても変化しないルール(Assert)

assert NoBadEntry {
     all t : Time, (追加の要素) |
          ...
}