実践的な例 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

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
 "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
<!-- Generated by graphviz version 2.43.0 (0)
 -->
<!-- Title: graph Pages: 1 -->
<svg width="539pt" height="249pt"
 viewBox="0.00 0.00 538.50 249.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 245)">
<title>graph</title>
<polygon fill="white" stroke="transparent" points="-4,4 -4,-245 534.5,-245 534.5,4 -4,4"/>
<!-- N6 -->
<g id="node1" class="node">
<title>N6</title>
<polygon fill="#ffd700" stroke="#ffd700" points="299.5,-145 143.5,-145 143.5,-85 299.5,-85 299.5,-145"/>
<text text-anchor="middle" x="221.5" y="-131.4" font-family="Times,serif" font-size="12.00" fill="#000000">Room</text>
<text text-anchor="middle" x="221.5" y="-118.4" font-family="Times,serif" font-size="12.00" fill="#000000">($NoBadEntry_r&#39;)</text>
<text text-anchor="middle" x="221.5" y="-105.4" font-family="Times,serif" font-size="12.00" fill="#000000">currentKey: Key1</text>
<text text-anchor="middle" x="221.5" y="-92.4" font-family="Times,serif" font-size="12.00" fill="#000000">keys: Key0, Key1, Key2</text>
</g>
<!-- N4 -->
<g id="node2" class="node">
<title>N4</title>
<polygon fill="#ffd700" stroke="#ffd700" points="176,-36 51,-36 51,0 176,0 176,-36"/>
<text text-anchor="middle" x="113.5" y="-21.4" font-family="Times,serif" font-size="12.00" fill="#000000">Key1</text>
<text text-anchor="middle" x="113.5" y="-8.4" font-family="Times,serif" font-size="12.00" fill="#000000">($NoBadEntry_k&#39;)</text>
</g>
<!-- N6&#45;&gt;N4 -->
<g id="edge1" class="edge">
<title>N6&#45;&gt;N4</title>
<path fill="none" stroke="#e41a1c" d="M143.28,-86.35C129.81,-80.07 118.75,-73.37 114.5,-67 110.52,-61.04 109.1,-53.67 108.97,-46.5"/>
<polygon fill="#e41a1c" stroke="#e41a1c" points="112.47,-46.53 109.56,-36.35 105.49,-46.13 112.47,-46.53"/>
<text text-anchor="middle" x="148.5" y="-57.4" font-family="Times,serif" font-size="12.00" fill="#e41a1c">currentKey</text>
</g>
<!-- N6&#45;&gt;N4 -->
<g id="edge5" class="edge">
<title>N6&#45;&gt;N4</title>
<path fill="none" stroke="#ff7f00" d="M206.75,-84.79C200.35,-74.16 192.11,-62.63 182.5,-54 177.14,-49.19 171,-44.85 164.64,-41.01"/>
<polygon fill="#ff7f00" stroke="#ff7f00" points="166.31,-37.94 155.88,-36.08 162.88,-44.04 166.31,-37.94"/>
<text text-anchor="middle" x="208.5" y="-57.4" font-family="Times,serif" font-size="12.00" fill="#ff7f00">keys</text>
</g>
<!-- N1 -->
<g id="node5" class="node">
<title>N1</title>
<polygon fill="#ffd700" stroke="#ffd700" points="385.5,-36 331.5,-36 331.5,0 385.5,0 385.5,-36"/>
<text text-anchor="middle" x="358.5" y="-14.9" font-family="Times,serif" font-size="12.00" fill="#000000">Key2</text>
</g>
<!-- N6&#45;&gt;N1 -->
<g id="edge6" class="edge">
<title>N6&#45;&gt;N1</title>
<path fill="none" stroke="#ff7f00" d="M263.35,-84.98C283.18,-71.23 306.55,-55.02 325.17,-42.11"/>
<polygon fill="#ff7f00" stroke="#ff7f00" points="327.4,-44.83 333.62,-36.25 323.41,-39.07 327.4,-44.83"/>
<text text-anchor="middle" x="320.5" y="-57.4" font-family="Times,serif" font-size="12.00" fill="#ff7f00">keys</text>
</g>
<!-- N0 -->
<g id="node6" class="node">
<title>N0</title>
<polygon fill="#ffd700" stroke="#ffd700" points="282.5,-36 228.5,-36 228.5,0 282.5,0 282.5,-36"/>
<text text-anchor="middle" x="255.5" y="-14.9" font-family="Times,serif" font-size="12.00" fill="#000000">Key0</text>
</g>
<!-- N6&#45;&gt;N0 -->
<g id="edge4" class="edge">
<title>N6&#45;&gt;N0</title>
<path fill="none" stroke="#ff7f00" d="M231.89,-84.98C236.34,-72.53 241.51,-58.08 245.88,-45.88"/>
<polygon fill="#ff7f00" stroke="#ff7f00" points="249.25,-46.85 249.33,-36.25 242.66,-44.49 249.25,-46.85"/>
<text text-anchor="middle" x="257.5" y="-57.4" font-family="Times,serif" font-size="12.00" fill="#ff7f00">keys</text>
</g>
<!-- N5 -->
<g id="node3" class="node">
<title>N5</title>
<polygon fill="#ffd700" stroke="#ffd700" points="125,-138.5 0,-138.5 0,-91.5 125,-91.5 125,-138.5"/>
<text text-anchor="middle" x="62.5" y="-124.9" font-family="Times,serif" font-size="12.00" fill="#000000">Guest0</text>
<text text-anchor="middle" x="62.5" y="-111.9" font-family="Times,serif" font-size="12.00" fill="#000000">($NoBadEntry_g&#39;)</text>
<text text-anchor="middle" x="62.5" y="-98.9" font-family="Times,serif" font-size="12.00" fill="#000000">keys: Key1</text>
</g>
<!-- N5&#45;&gt;N4 -->
<g id="edge2" class="edge">
<title>N5&#45;&gt;N4</title>
<path fill="none" stroke="#a65628" d="M58.16,-91.41C57.02,-79.61 57.49,-65.32 63.5,-54 65.68,-49.89 68.59,-46.16 71.91,-42.8"/>
<polygon fill="#a65628" stroke="#a65628" points="74.45,-45.23 79.71,-36.03 69.86,-39.94 74.45,-45.23"/>
<text text-anchor="middle" x="77.5" y="-57.4" font-family="Times,serif" font-size="12.00" fill="#a65628">keys</text>
</g>
<!-- N2 -->
<g id="node4" class="node">
<title>N2</title>
<polygon fill="#ffd700" stroke="#ffd700" points="399,-133 318,-133 318,-97 399,-97 399,-133"/>
<text text-anchor="middle" x="358.5" y="-118.4" font-family="Times,serif" font-size="12.00" fill="#000000">Guest1</text>
<text text-anchor="middle" x="358.5" y="-105.4" font-family="Times,serif" font-size="12.00" fill="#000000">keys: Key2</text>
</g>
<!-- N2&#45;&gt;N1 -->
<g id="edge3" class="edge">
<title>N2&#45;&gt;N1</title>
<path fill="none" stroke="#a65628" d="M358.5,-96.58C358.5,-82.65 358.5,-62.86 358.5,-46.76"/>
<polygon fill="#a65628" stroke="#a65628" points="362,-46.31 358.5,-36.31 355,-46.31 362,-46.31"/>
<text text-anchor="middle" x="372.5" y="-57.4" font-family="Times,serif" font-size="12.00" fill="#a65628">keys</text>
</g>
<!-- N3 -->
<g id="node7" class="node">
<title>N3</title>
<polygon fill="#ffd700" stroke="#ffd700" points="481.5,-241 311.5,-241 311.5,-194 481.5,-194 481.5,-241"/>
<text text-anchor="middle" x="396.5" y="-227.4" font-family="Times,serif" font-size="12.00" fill="#000000">FrontDesk</text>
<text text-anchor="middle" x="396.5" y="-214.4" font-family="Times,serif" font-size="12.00" fill="#000000">lastKey: Room&#45;&gt;Key2</text>
<text text-anchor="middle" x="396.5" y="-201.4" font-family="Times,serif" font-size="12.00" fill="#000000">occupant: Room&#45;&gt;Guest1</text>
</g>
<!-- N3&#45;&gt;N2 -->
<g id="edge8" class="edge">
<title>N3&#45;&gt;N2</title>
<path fill="none" stroke="#377eb8" d="M353.41,-193.85C347.41,-188.8 342.08,-182.86 338.5,-176 332.96,-165.38 335.77,-152.92 340.82,-142.12"/>
<polygon fill="#377eb8" stroke="#377eb8" points="344,-143.6 345.68,-133.13 337.85,-140.26 344,-143.6"/>
<text text-anchor="middle" x="390.5" y="-166.4" font-family="Times,serif" font-size="12.00" fill="#377eb8">occupant [Room]</text>
</g>
<!-- N3&#45;&gt;N1 -->
<g id="edge7" class="edge">
<title>N3&#45;&gt;N1</title>
<path fill="none" stroke="#4daf4a" d="M429.67,-193.72C434.88,-188.54 439.52,-182.59 442.5,-176 444.88,-170.73 443.68,-168.66 442.5,-163 431.55,-110.45 422.27,-97.26 390.5,-54 387.98,-50.57 385.17,-47.09 382.29,-43.73"/>
<polygon fill="#4daf4a" stroke="#4daf4a" points="384.82,-41.31 375.55,-36.17 379.59,-45.96 384.82,-41.31"/>
<text text-anchor="middle" x="484" y="-111.9" font-family="Times,serif" font-size="12.00" fill="#4daf4a">lastKey [Room]</text>
</g>
</g>
</svg>