実践的な例 Alloy part 3

_main.md

Alloy part 3

前回の続き。

ホテルの客室施錠

錠前は次の性質を持つ。

• 現在の鍵の組み合わせを保持する
• 疑似乱数を生成する（フィードバックレジスタ）
• 鍵の組み合わせは、現在か次のもののみが錠前を開く

鍵は次のように更新される。

1. ホテルは次の利用者に新しい鍵を渡す
2. 次の組み合わせが挿入された時点で、組み合わせが遷移する。以前の鍵は使えなくなる。

hotel1.als

NoIntervening がコメントアウトされているため、宿泊客のチェックインと入室の間にイベントが起き、反例を示す。

フレーム条件とは

https://en.wikipedia.org/wiki/Problem_frames_approach

イベントに基づくモデル化

プリミティヴな操作の代わりに、イベントに着目したシグネチャが使える。階層を持つことによる括りだしとトレースの可視化に利点がある。伝統的なフレーム条件に対しReiterの方法と呼ぶ。操作と構成要素が一対一になるときに計算が効率的になる。

The Frame Problem in the Situation Calculus: A Simple Solution (Sometimes) and a Completeness Result for Goal Regression

event_hotel_t0.svg

event_hotel_t1.svg

event_hotel_t2.svg

event_hotel_t3.svg

event_hotel_t4.svg

hotel.als

module chapter6/hotel1 --- the model up to the top of page 191
open util/ordering[Time] as to
open util/ordering[Key] as ko

// 鍵の組み合わせ、物理的な鍵をカードと呼ぶ
sig Key {}
// Idiom
sig Time {}

sig Room {
  keys: set Key,
  currentKey: keys one -> Time
  }

fact DisjointKeySets {
  -- each key belongs to at most one room
  // Guest との混同を避ける制限演算子
  Room <: keys
    in Room lone-> Key
  }

one sig FrontDesk {
  lastKey: (Room -> lone Key) -> Time,
  occupant: (Room -> Guest) -> Time
  }

sig Guest {
  keys: Key -> Time
  }

fun nextKey [k: Key, ks: set Key]: set Key {
  min [k.nexts & ks]
  }

pred init [t: Time] {
  no Guest.keys.t
  no FrontDesk.occupant.t
  all r: Room | FrontDesk.lastKey.t [r] = r.currentKey.t
  }

pred entry [t, t': Time, g: Guest, r: Room, k: Key] {
  // pre cond. 錠前を開ける鍵は宿泊客が持つ鍵のうちの一つ
  k in g.keys.t
  let ck = r.currentKey |
    // post cond. カードに記録された鍵は錠前の現在の鍵と一致して錠前は変化しない
    (k = ck.t and ck.t' = ck.t)
    // あるいは次の鍵と一致して錠前が次に進む
    or (k = nextKey[ck.t, r.keys] and ck.t' = k)
  // frame cond. 状態のどの部分が変化しないか
  noRoomChangeExcept [t, t', r]
  noGuestChangeExcept [t, t', none]
  noFrontDeskChange [t, t']
  }

// 他の客室
pred noRoomChangeExcept [t, t': Time, rs: set Room] {
  all r: Room - rs | r.currentKey.t = r.currentKey.t'
  }

// 宿泊客が持つ鍵の集合
pred noGuestChangeExcept [t, t': Time, gs: set Guest] {
  all g: Guest - gs | g.keys.t = g.keys.t'
  }

// フロントの記録
pred noFrontDeskChange [t, t': Time] {
  FrontDesk.lastKey.t = FrontDesk.lastKey.t'
  FrontDesk.occupant.t = FrontDesk.occupant.t'
  }

pred checkout [t, t': Time, g: Guest] {
  let occ = FrontDesk.occupant {
    some occ.t.g
    occ.t' = occ.t - Room ->g
    }
  FrontDesk.lastKey.t = FrontDesk.lastKey.t'
  noRoomChangeExcept [t, t', none]
  noGuestChangeExcept [t, t', none]
  }

pred checkin [t, t': Time, g: Guest, r: Room, k: Key] {
  // 宿泊客は鍵を得る
  g.keys.t' = g.keys.t + k
  let occ = FrontDesk.occupant {
    // 利用者なし
    no occ.t [r]
    // 客を登録
    occ.t' = occ.t + r -> g
    }
  let lk = FrontDesk.lastKey {
    // フロントは客室の最新の鍵を更新
    lk.t' = lk.t ++ r -> k
    // 鍵とは系列の次のもの
    k = nextKey [lk.t [r], r.keys]
    }
  noRoomChangeExcept [t, t', none]
  noGuestChangeExcept [t, t', g]
  }

fact traces {
  init [first]
  all t: Time-last | let t' = t.next |
    some g: Guest, r: Room, k: Key |
      entry [t, t', g, r, k]
      or checkin [t, t', g, r, k]
      or checkout [t, t', g]
  }

// fact NoIntervening {
//   all t: Time-last | let t' = t.next, t" = t'.next |
//     all g: Guest, r: Room, k: Key |
//       checkin [t, t', g, r, k] => (entry [t', t", g, r, k] or no t")
//   }

assert NoBadEntry {
  all t: Time, r: Room, g: Guest, k: Key |
    let t' = t.next, o = FrontDesk.occupant.t[r] |
      entry [t, t', g, r, k] and some o => g in o
  }

// This generates a counterexample similar to Fig 6.6
check NoBadEntry for 3 but 2 Room, 2 Guest, 5 Time

hotel_t0.svg

hotel_t1.svg

hotel_t2.svg

hotel_t3.svg

hotel_t4.svg