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

<?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="886pt" height="153pt"
 viewBox="0.00 0.00 886.00 153.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 149)">
<title>graph</title>
<polygon fill="white" stroke="transparent" points="-4,4 -4,-149 882,-149 882,4 -4,4"/>
<!-- N6 -->
<g id="node1" class="node">
<title>N6</title>
<polygon fill="#ffd700" stroke="#ffd700" points="387.5,-145 162.5,-145 162.5,-85 387.5,-85 387.5,-145"/>
<text text-anchor="middle" x="275" y="-131.4" font-family="Times,serif" font-size="12.00" fill="#000000">Room</text>
<text text-anchor="middle" x="275" y="-118.4" font-family="Times,serif" font-size="12.00" fill="#000000">($NoBadEntry_r, $NoBadEntry_r&#39;)</text>
<text text-anchor="middle" x="275" y="-105.4" font-family="Times,serif" font-size="12.00" fill="#000000">currentKey: Key0</text>
<text text-anchor="middle" x="275" 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="404,-36 350,-36 350,0 404,0 404,-36"/>
<text text-anchor="middle" x="377" y="-14.9" font-family="Times,serif" font-size="12.00" fill="#000000">Key0</text>
</g>
<!-- N6&#45;&gt;N4 -->
<g id="edge1" class="edge">
<title>N6&#45;&gt;N4</title>
<path fill="none" stroke="#e41a1c" d="M334.52,-84.73C341.98,-79.49 349.06,-73.57 355,-67 360.55,-60.85 364.93,-53.06 368.27,-45.55"/>
<polygon fill="#e41a1c" stroke="#e41a1c" points="371.62,-46.6 372.06,-36.01 365.11,-44.01 371.62,-46.6"/>
<text text-anchor="middle" x="398" y="-57.4" font-family="Times,serif" font-size="12.00" fill="#e41a1c">currentKey</text>
</g>
<!-- N6&#45;&gt;N4 -->
<g id="edge2" class="edge">
<title>N6&#45;&gt;N4</title>
<path fill="none" stroke="#a65628" d="M295.26,-84.9C303.24,-74.51 312.91,-63.13 323,-54 328.58,-48.95 334.96,-44.13 341.34,-39.78"/>
<polygon fill="#a65628" stroke="#a65628" points="343.5,-42.55 349.96,-34.14 339.67,-36.69 343.5,-42.55"/>
<text text-anchor="middle" x="337" y="-57.4" font-family="Times,serif" font-size="12.00" fill="#a65628">keys</text>
</g>
<!-- N3 -->
<g id="node3" class="node">
<title>N3</title>
<polygon fill="#ffd700" stroke="#ffd700" points="230,-36 0,-36 0,0 230,0 230,-36"/>
<text text-anchor="middle" x="115" y="-21.4" font-family="Times,serif" font-size="12.00" fill="#000000">Key1</text>
<text text-anchor="middle" x="115" y="-8.4" font-family="Times,serif" font-size="12.00" fill="#000000">($NoBadEntry_k, $NoBadEntry_k&#39;)</text>
</g>
<!-- N6&#45;&gt;N3 -->
<g id="edge3" class="edge">
<title>N6&#45;&gt;N3</title>
<path fill="none" stroke="#a65628" d="M226.13,-84.98C202.54,-70.98 174.68,-54.43 152.75,-41.42"/>
<polygon fill="#a65628" stroke="#a65628" points="154.44,-38.35 144.06,-36.25 150.87,-44.37 154.44,-38.35"/>
<text text-anchor="middle" x="209" 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="302,-36 248,-36 248,0 302,0 302,-36"/>
<text text-anchor="middle" x="275" y="-14.9" font-family="Times,serif" font-size="12.00" fill="#000000">Key2</text>
</g>
<!-- N6&#45;&gt;N2 -->
<g id="edge4" class="edge">
<title>N6&#45;&gt;N2</title>
<path fill="none" stroke="#a65628" d="M275,-84.98C275,-72.78 275,-58.66 275,-46.61"/>
<polygon fill="#a65628" stroke="#a65628" points="278.5,-46.25 275,-36.25 271.5,-46.25 278.5,-46.25"/>
<text text-anchor="middle" x="289" y="-57.4" font-family="Times,serif" font-size="12.00" fill="#a65628">keys</text>
</g>
<!-- N5 -->
<g id="node5" class="node">
<title>N5</title>
<polygon fill="#ffd700" stroke="#ffd700" points="552.5,-133 405.5,-133 405.5,-97 552.5,-97 552.5,-133"/>
<text text-anchor="middle" x="479" y="-118.4" font-family="Times,serif" font-size="12.00" fill="#000000">FrontDesk</text>
<text text-anchor="middle" x="479" y="-105.4" font-family="Times,serif" font-size="12.00" fill="#000000">lastKey: Room&#45;&gt;Key0</text>
</g>
<!-- N5&#45;&gt;N4 -->
<g id="edge5" class="edge">
<title>N5&#45;&gt;N4</title>
<path fill="none" stroke="#ff7f00" d="M469.32,-96.76C461.51,-83.9 449.6,-66.47 436,-54 429.18,-47.74 421.06,-42.06 413.06,-37.17"/>
<polygon fill="#ff7f00" stroke="#ff7f00" points="414.56,-34 404.15,-32.01 411.05,-40.06 414.56,-34"/>
<text text-anchor="middle" x="493.5" y="-57.4" font-family="Times,serif" font-size="12.00" fill="#ff7f00">lastKey [Room]</text>
</g>
<!-- N0 -->
<g id="node6" class="node">
<title>N0</title>
<polygon fill="#ffd700" stroke="#ffd700" points="629.5,-133 570.5,-133 570.5,-97 629.5,-97 629.5,-133"/>
<text text-anchor="middle" x="600" y="-111.9" font-family="Times,serif" font-size="12.00" fill="#000000">Guest1</text>
</g>
<!-- N1 -->
<g id="node7" class="node">
<title>N1</title>
<polygon fill="#ffd700" stroke="#ffd700" points="878,-133 648,-133 648,-97 878,-97 878,-133"/>
<text text-anchor="middle" x="763" y="-118.4" font-family="Times,serif" font-size="12.00" fill="#000000">Guest0</text>
<text text-anchor="middle" x="763" y="-105.4" font-family="Times,serif" font-size="12.00" fill="#000000">($NoBadEntry_g, $NoBadEntry_g&#39;)</text>
</g>
</g>
</svg>

hotel_t1.svg

hotel_t2.svg

hotel_t3.svg

hotel_t4.svg