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

<?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="615pt" height="249pt"
 viewBox="0.00 0.00 614.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 610.5,-245 610.5,4 -4,4"/>
<!-- N6 -->
<g id="node1" class="node">
<title>N6</title>
<polygon fill="#ffd700" stroke="#ffd700" points="225,-145 0,-145 0,-85 225,-85 225,-145"/>
<text text-anchor="middle" x="112.5" y="-131.4" font-family="Times,serif" font-size="12.00" fill="#000000">Room</text>
<text text-anchor="middle" x="112.5" y="-118.4" font-family="Times,serif" font-size="12.00" fill="#000000">($NoBadEntry_r, $NoBadEntry_r&#39;)</text>
<text text-anchor="middle" x="112.5" y="-105.4" font-family="Times,serif" font-size="12.00" fill="#000000">currentKey: Key0</text>
<text text-anchor="middle" x="112.5" y="-92.4" font-family="Times,serif" font-size="12.00" fill="#000000">keys: Key0, Key1, Key2</text>
</g>
<!-- N5 -->
<g id="node2" class="node">
<title>N5</title>
<polygon fill="#ffd700" stroke="#ffd700" points="66.5,-36 12.5,-36 12.5,0 66.5,0 66.5,-36"/>
<text text-anchor="middle" x="39.5" y="-14.9" font-family="Times,serif" font-size="12.00" fill="#000000">Key0</text>
</g>
<!-- N6&#45;&gt;N5 -->
<g id="edge1" class="edge">
<title>N6&#45;&gt;N5</title>
<path fill="none" stroke="#e41a1c" d="M38.24,-84.67C32.06,-79.64 26.61,-73.78 22.5,-67 18.53,-60.45 19.2,-52.84 21.81,-45.63"/>
<polygon fill="#e41a1c" stroke="#e41a1c" points="25.17,-46.72 26.34,-36.19 18.86,-43.7 25.17,-46.72"/>
<text text-anchor="middle" x="56.5" y="-57.4" font-family="Times,serif" font-size="12.00" fill="#e41a1c">currentKey</text>
</g>
<!-- N6&#45;&gt;N5 -->
<g id="edge3" class="edge">
<title>N6&#45;&gt;N5</title>
<path fill="none" stroke="#ff7f00" d="M105.83,-84.99C102.44,-74.5 97.51,-63.03 90.5,-54 86.21,-48.47 80.79,-43.49 75.11,-39.14"/>
<polygon fill="#ff7f00" stroke="#ff7f00" points="76.88,-36.1 66.69,-33.21 72.85,-41.83 76.88,-36.1"/>
<text text-anchor="middle" x="112.5" y="-57.4" font-family="Times,serif" font-size="12.00" fill="#ff7f00">keys</text>
</g>
<!-- N2 -->
<g id="node4" class="node">
<title>N2</title>
<polygon fill="#ffd700" stroke="#ffd700" points="421,-36 296,-36 296,0 421,0 421,-36"/>
<text text-anchor="middle" x="358.5" y="-21.4" font-family="Times,serif" font-size="12.00" fill="#000000">Key1</text>
<text text-anchor="middle" x="358.5" y="-8.4" font-family="Times,serif" font-size="12.00" fill="#000000">($NoBadEntry_k&#39;)</text>
</g>
<!-- N6&#45;&gt;N2 -->
<g id="edge4" class="edge">
<title>N6&#45;&gt;N2</title>
<path fill="none" stroke="#ff7f00" d="M187.64,-84.98C225.49,-70.37 270.49,-52.99 304.81,-39.74"/>
<polygon fill="#ff7f00" stroke="#ff7f00" points="306.12,-42.98 314.19,-36.11 303.6,-36.45 306.12,-42.98"/>
<text text-anchor="middle" x="279.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="224.5,-36 102.5,-36 102.5,0 224.5,0 224.5,-36"/>
<text text-anchor="middle" x="163.5" y="-21.4" font-family="Times,serif" font-size="12.00" fill="#000000">Key2</text>
<text text-anchor="middle" x="163.5" y="-8.4" font-family="Times,serif" font-size="12.00" fill="#000000">($NoBadEntry_k)</text>
</g>
<!-- N6&#45;&gt;N1 -->
<g id="edge5" class="edge">
<title>N6&#45;&gt;N1</title>
<path fill="none" stroke="#ff7f00" d="M131.17,-84.99C134.73,-79.11 138.33,-72.92 141.5,-67 145.19,-60.11 148.86,-52.49 152.11,-45.38"/>
<polygon fill="#ff7f00" stroke="#ff7f00" points="155.36,-46.69 156.26,-36.13 148.98,-43.82 155.36,-46.69"/>
<text text-anchor="middle" x="162.5" y="-57.4" font-family="Times,serif" font-size="12.00" fill="#ff7f00">keys</text>
</g>
<!-- N3 -->
<g id="node3" class="node">
<title>N3</title>
<polygon fill="#ffd700" stroke="#ffd700" points="473.5,-138.5 243.5,-138.5 243.5,-91.5 473.5,-91.5 473.5,-138.5"/>
<text text-anchor="middle" x="358.5" y="-124.9" font-family="Times,serif" font-size="12.00" fill="#000000">Guest0</text>
<text text-anchor="middle" x="358.5" y="-111.9" font-family="Times,serif" font-size="12.00" fill="#000000">($NoBadEntry_g, $NoBadEntry_g&#39;)</text>
<text text-anchor="middle" x="358.5" y="-98.9" font-family="Times,serif" font-size="12.00" fill="#000000">keys: Key1</text>
</g>
<!-- N3&#45;&gt;N2 -->
<g id="edge2" class="edge">
<title>N3&#45;&gt;N2</title>
<path fill="none" stroke="#a65628" d="M358.5,-91.49C358.5,-77.93 358.5,-60.58 358.5,-46.26"/>
<polygon fill="#a65628" stroke="#a65628" points="362,-46 358.5,-36 355,-46 362,-46"/>
<text text-anchor="middle" x="372.5" y="-57.4" font-family="Times,serif" font-size="12.00" fill="#a65628">keys</text>
</g>
<!-- N4 -->
<g id="node6" class="node">
<title>N4</title>
<polygon fill="#ffd700" stroke="#ffd700" points="518.5,-241 348.5,-241 348.5,-194 518.5,-194 518.5,-241"/>
<text text-anchor="middle" x="433.5" y="-227.4" font-family="Times,serif" font-size="12.00" fill="#000000">FrontDesk</text>
<text text-anchor="middle" x="433.5" y="-214.4" font-family="Times,serif" font-size="12.00" fill="#000000">lastKey: Room&#45;&gt;Key1</text>
<text text-anchor="middle" x="433.5" y="-201.4" font-family="Times,serif" font-size="12.00" fill="#000000">occupant: Room&#45;&gt;Guest0</text>
</g>
<!-- N4&#45;&gt;N3 -->
<g id="edge7" class="edge">
<title>N4&#45;&gt;N3</title>
<path fill="none" stroke="#377eb8" d="M407.35,-193.66C401.78,-188.17 396.18,-182.11 391.5,-176 384.89,-167.36 378.79,-157.23 373.68,-147.78"/>
<polygon fill="#377eb8" stroke="#377eb8" points="376.64,-145.89 368.91,-138.64 370.43,-149.13 376.64,-145.89"/>
<text text-anchor="middle" x="443.5" y="-166.4" font-family="Times,serif" font-size="12.00" fill="#377eb8">occupant [Room]</text>
</g>
<!-- N4&#45;&gt;N2 -->
<g id="edge6" class="edge">
<title>N4&#45;&gt;N2</title>
<path fill="none" stroke="#4daf4a" d="M480.12,-193.81C486.29,-188.81 491.77,-182.9 495.5,-176 507.43,-153.96 536.77,-160.47 482.5,-85 468.05,-64.9 445.56,-50.37 423.69,-40.14"/>
<polygon fill="#4daf4a" stroke="#4daf4a" points="424.94,-36.87 414.38,-36.02 422.1,-43.27 424.94,-36.87"/>
<text text-anchor="middle" x="560" y="-111.9" font-family="Times,serif" font-size="12.00" fill="#4daf4a">lastKey [Room]</text>
</g>
<!-- N0 -->
<g id="node7" class="node">
<title>N0</title>
<polygon fill="#ffd700" stroke="#ffd700" points="596,-235.5 537,-235.5 537,-199.5 596,-199.5 596,-235.5"/>
<text text-anchor="middle" x="566.5" y="-214.4" font-family="Times,serif" font-size="12.00" fill="#000000">Guest1</text>
</g>
</g>
</svg>

hotel_t2.svg

hotel_t3.svg

hotel_t4.svg