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

<?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="1002pt" height="262pt"
 viewBox="0.00 0.00 1002.00 262.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 258)">
<title>graph</title>
<polygon fill="white" stroke="transparent" points="-4,4 -4,-258 998,-258 998,4 -4,4"/>
<!-- N9 -->
<g id="node1" class="node">
<title>N9</title>
<polygon fill="#ffd700" stroke="#ffd700" points="512,-132 356,-132 356,-85 512,-85 512,-132"/>
<text text-anchor="middle" x="434" y="-118.4" font-family="Times,serif" font-size="12.00" fill="#000000">Room</text>
<text text-anchor="middle" x="434" y="-105.4" font-family="Times,serif" font-size="12.00" fill="#000000">currentKey: Key0</text>
<text text-anchor="middle" x="434" y="-92.4" font-family="Times,serif" font-size="12.00" fill="#000000">keys: Key0, Key1, Key4</text>
</g>
<!-- N8 -->
<g id="node2" class="node">
<title>N8</title>
<polygon fill="#ffd700" stroke="#ffd700" points="452,-36 398,-36 398,0 452,0 452,-36"/>
<text text-anchor="middle" x="425" y="-14.9" font-family="Times,serif" font-size="12.00" fill="#000000">Key0</text>
</g>
<!-- N9&#45;&gt;N8 -->
<g id="edge1" class="edge">
<title>N9&#45;&gt;N8</title>
<path fill="none" stroke="#e41a1c" d="M431.99,-84.84C431.11,-75.31 430.05,-64.11 429,-54 428.73,-51.45 428.45,-48.79 428.16,-46.13"/>
<polygon fill="#e41a1c" stroke="#e41a1c" points="431.62,-45.63 427.02,-36.08 424.67,-46.41 431.62,-45.63"/>
<text text-anchor="middle" x="465" y="-57.4" font-family="Times,serif" font-size="12.00" fill="#e41a1c">currentKey</text>
</g>
<!-- N9&#45;&gt;N8 -->
<g id="edge11" class="edge">
<title>N9&#45;&gt;N8</title>
<path fill="none" stroke="#377eb8" d="M407.98,-84.72C403.49,-79.39 399.48,-73.39 397,-67 394.06,-59.41 396.09,-51.61 400.15,-44.56"/>
<polygon fill="#377eb8" stroke="#377eb8" points="403.21,-46.29 406.14,-36.11 397.5,-42.24 403.21,-46.29"/>
<text text-anchor="middle" x="411" y="-57.4" font-family="Times,serif" font-size="12.00" fill="#377eb8">keys</text>
</g>
<!-- N5 -->
<g id="node9" class="node">
<title>N5</title>
<polygon fill="#ffd700" stroke="#ffd700" points="305,-36 251,-36 251,0 305,0 305,-36"/>
<text text-anchor="middle" x="278" y="-14.9" font-family="Times,serif" font-size="12.00" fill="#000000">Key1</text>
</g>
<!-- N9&#45;&gt;N5 -->
<g id="edge12" class="edge">
<title>N9&#45;&gt;N5</title>
<path fill="none" stroke="#377eb8" d="M394.23,-84.94C369.58,-70.95 338.15,-53.13 314.2,-39.53"/>
<polygon fill="#377eb8" stroke="#377eb8" points="315.84,-36.44 305.41,-34.55 312.38,-42.53 315.84,-36.44"/>
<text text-anchor="middle" x="375" y="-57.4" font-family="Times,serif" font-size="12.00" fill="#377eb8">keys</text>
</g>
<!-- N2 -->
<g id="node10" class="node">
<title>N2</title>
<polygon fill="#ffd700" stroke="#ffd700" points="640,-36 586,-36 586,0 640,0 640,-36"/>
<text text-anchor="middle" x="613" y="-14.9" font-family="Times,serif" font-size="12.00" fill="#000000">Key4</text>
</g>
<!-- N9&#45;&gt;N2 -->
<g id="edge13" class="edge">
<title>N9&#45;&gt;N2</title>
<path fill="none" stroke="#377eb8" d="M479.63,-84.94C509.78,-70.03 548.76,-50.76 576.78,-36.91"/>
<polygon fill="#377eb8" stroke="#377eb8" points="578.42,-40 585.84,-32.43 575.32,-33.73 578.42,-40"/>
<text text-anchor="middle" x="554" y="-57.4" font-family="Times,serif" font-size="12.00" fill="#377eb8">keys</text>
</g>
<!-- N12 -->
<g id="node3" class="node">
<title>N12</title>
<polygon fill="#ffd700" stroke="#ffd700" points="214,-247.5 116,-247.5 116,-187.5 214,-187.5 214,-247.5"/>
<text text-anchor="middle" x="165" y="-233.9" font-family="Times,serif" font-size="12.00" fill="#000000">Checkin0</text>
<text text-anchor="middle" x="165" y="-220.9" font-family="Times,serif" font-size="12.00" fill="#000000">guest: Guest0</text>
<text text-anchor="middle" x="165" y="-207.9" font-family="Times,serif" font-size="12.00" fill="#000000">key: Key1</text>
<text text-anchor="middle" x="165" y="-194.9" font-family="Times,serif" font-size="12.00" fill="#000000">room: Room</text>
</g>
<!-- N12&#45;&gt;N9 -->
<g id="edge16" class="edge">
<title>N12&#45;&gt;N9</title>
<path fill="none" stroke="#a65628" d="M185.85,-187.33C197.08,-173.82 212.1,-158.83 229,-150 274.08,-126.46 292.15,-142.05 342,-132 343.27,-131.74 344.55,-131.48 345.83,-131.22"/>
<polygon fill="#a65628" stroke="#a65628" points="346.75,-134.6 355.8,-129.09 345.29,-127.75 346.75,-134.6"/>
<text text-anchor="middle" x="245.5" y="-153.4" font-family="Times,serif" font-size="12.00" fill="#a65628">room</text>
</g>
<!-- N6 -->
<g id="node4" class="node">
<title>N6</title>
<polygon fill="#ffd700" stroke="#ffd700" points="270.5,-126.5 189.5,-126.5 189.5,-90.5 270.5,-90.5 270.5,-126.5"/>
<text text-anchor="middle" x="230" y="-111.9" font-family="Times,serif" font-size="12.00" fill="#000000">Guest0</text>
<text text-anchor="middle" x="230" y="-98.9" font-family="Times,serif" font-size="12.00" fill="#000000">keys: Key1</text>
</g>
<!-- N12&#45;&gt;N6 -->
<g id="edge2" class="edge">
<title>N12&#45;&gt;N6</title>
<path fill="none" stroke="#a65628" d="M159.57,-187.43C158.71,-175.17 159.73,-161.18 166,-150 169.84,-143.14 175.38,-137.28 181.61,-132.32"/>
<polygon fill="#a65628" stroke="#a65628" points="183.66,-135.16 189.8,-126.52 179.61,-129.45 183.66,-135.16"/>
<text text-anchor="middle" x="182.5" y="-153.4" font-family="Times,serif" font-size="12.00" fill="#a65628">guest</text>
</g>
<!-- N12&#45;&gt;N5 -->
<g id="edge6" class="edge">
<title>N12&#45;&gt;N5</title>
<path fill="none" stroke="#ff7f00" d="M154.7,-187.38C146.63,-159.17 139.56,-116.19 158,-85 175.86,-54.79 213.02,-37.48 241.28,-28.23"/>
<polygon fill="#ff7f00" stroke="#ff7f00" points="242.33,-31.57 250.86,-25.29 240.27,-24.88 242.33,-31.57"/>
<text text-anchor="middle" x="169" y="-105.4" font-family="Times,serif" font-size="12.00" fill="#ff7f00">key</text>
</g>
<!-- N6&#45;&gt;N5 -->
<g id="edge9" class="edge">
<title>N6&#45;&gt;N5</title>
<path fill="none" stroke="#4daf4a" d="M239.25,-90.44C246.23,-77.58 255.91,-59.73 263.85,-45.08"/>
<polygon fill="#4daf4a" stroke="#4daf4a" points="267.08,-46.47 268.77,-36.01 260.93,-43.13 267.08,-46.47"/>
<text text-anchor="middle" x="273" y="-57.4" font-family="Times,serif" font-size="12.00" fill="#4daf4a">keys</text>
</g>
<!-- N11 -->
<g id="node5" class="node">
<title>N11</title>
<polygon fill="#ffd700" stroke="#ffd700" points="634,-254 536,-254 536,-181 634,-181 634,-254"/>
<text text-anchor="middle" x="585" y="-240.4" font-family="Times,serif" font-size="12.00" fill="#000000">Checkin1</text>
<text text-anchor="middle" x="585" y="-227.4" font-family="Times,serif" font-size="12.00" fill="#000000">(post)</text>
<text text-anchor="middle" x="585" y="-214.4" font-family="Times,serif" font-size="12.00" fill="#000000">guest: Guest1</text>
<text text-anchor="middle" x="585" y="-201.4" font-family="Times,serif" font-size="12.00" fill="#000000">key: Key4</text>
<text text-anchor="middle" x="585" y="-188.4" font-family="Times,serif" font-size="12.00" fill="#000000">room: Room</text>
</g>
<!-- N11&#45;&gt;N9 -->
<g id="edge17" class="edge">
<title>N11&#45;&gt;N9</title>
<path fill="none" stroke="#a65628" d="M535.97,-181.76C516.11,-167.68 493.45,-151.62 474.54,-138.23"/>
<polygon fill="#a65628" stroke="#a65628" points="476.32,-135.2 466.14,-132.27 472.27,-140.91 476.32,-135.2"/>
<text text-anchor="middle" x="526.5" y="-153.4" font-family="Times,serif" font-size="12.00" fill="#a65628">room</text>
</g>
<!-- N3 -->
<g id="node6" class="node">
<title>N3</title>
<polygon fill="#ffd700" stroke="#ffd700" points="706.5,-126.5 625.5,-126.5 625.5,-90.5 706.5,-90.5 706.5,-126.5"/>
<text text-anchor="middle" x="666" y="-111.9" font-family="Times,serif" font-size="12.00" fill="#000000">Guest1</text>
<text text-anchor="middle" x="666" y="-98.9" font-family="Times,serif" font-size="12.00" fill="#000000">keys: Key4</text>
</g>
<!-- N11&#45;&gt;N3 -->
<g id="edge3" class="edge">
<title>N11&#45;&gt;N3</title>
<path fill="none" stroke="#a65628" d="M600.08,-180.8C605.31,-170.36 611.71,-159.28 619,-150 623.58,-144.18 629.08,-138.56 634.69,-133.46"/>
<polygon fill="#a65628" stroke="#a65628" points="637.06,-136.04 642.33,-126.85 632.47,-130.75 637.06,-136.04"/>
<text text-anchor="middle" x="635.5" y="-153.4" font-family="Times,serif" font-size="12.00" fill="#a65628">guest</text>
</g>
<!-- N11&#45;&gt;N2 -->
<g id="edge7" class="edge">
<title>N11&#45;&gt;N2</title>
<path fill="none" stroke="#ff7f00" d="M585.4,-180.81C586.2,-154.22 588.34,-117.11 594,-85 596.3,-71.92 600.2,-57.73 603.86,-45.87"/>
<polygon fill="#ff7f00" stroke="#ff7f00" points="607.27,-46.73 606.98,-36.13 600.6,-44.59 607.27,-46.73"/>
<text text-anchor="middle" x="605" y="-105.4" font-family="Times,serif" font-size="12.00" fill="#ff7f00">key</text>
</g>
<!-- N3&#45;&gt;N2 -->
<g id="edge10" class="edge">
<title>N3&#45;&gt;N2</title>
<path fill="none" stroke="#4daf4a" d="M655.78,-90.44C648.01,-77.46 637.19,-59.39 628.37,-44.67"/>
<polygon fill="#4daf4a" stroke="#4daf4a" points="631.33,-42.79 623.19,-36.01 625.32,-46.39 631.33,-42.79"/>
<text text-anchor="middle" x="656" y="-57.4" font-family="Times,serif" font-size="12.00" fill="#4daf4a">keys</text>
</g>
<!-- N7 -->
<g id="node7" class="node">
<title>N7</title>
<polygon fill="#ffd700" stroke="#ffd700" points="98,-235.5 0,-235.5 0,-199.5 98,-199.5 98,-235.5"/>
<text text-anchor="middle" x="49" y="-220.9" font-family="Times,serif" font-size="12.00" fill="#000000">Checkout</text>
<text text-anchor="middle" x="49" y="-207.9" font-family="Times,serif" font-size="12.00" fill="#000000">guest: Guest0</text>
</g>
<!-- N7&#45;&gt;N6 -->
<g id="edge4" class="edge">
<title>N7&#45;&gt;N6</title>
<path fill="none" stroke="#a65628" d="M65.14,-199.32C79.67,-184.64 102.19,-163.78 125,-150 141.86,-139.81 161.73,-131.37 179.62,-124.87"/>
<polygon fill="#a65628" stroke="#a65628" points="181.05,-128.08 189.32,-121.47 178.73,-121.48 181.05,-128.08"/>
<text text-anchor="middle" x="141.5" y="-153.4" font-family="Times,serif" font-size="12.00" fill="#a65628">guest</text>
</g>
<!-- N10 -->
<g id="node8" class="node">
<title>N10</title>
<polygon fill="#ffd700" stroke="#ffd700" points="488,-254 232,-254 232,-181 488,-181 488,-254"/>
<text text-anchor="middle" x="360" y="-240.4" font-family="Times,serif" font-size="12.00" fill="#000000">Entry</text>
<text text-anchor="middle" x="360" y="-227.4" font-family="Times,serif" font-size="12.00" fill="#000000">($NoBadEntry_e, $NoBadEntry_e&#39;, pre)</text>
<text text-anchor="middle" x="360" y="-214.4" font-family="Times,serif" font-size="12.00" fill="#000000">guest: Guest0</text>
<text text-anchor="middle" x="360" y="-201.4" font-family="Times,serif" font-size="12.00" fill="#000000">key: Key1</text>
<text text-anchor="middle" x="360" y="-188.4" font-family="Times,serif" font-size="12.00" fill="#000000">room: Room</text>
</g>
<!-- N10&#45;&gt;N9 -->
<g id="edge18" class="edge">
<title>N10&#45;&gt;N9</title>
<path fill="none" stroke="#a65628" d="M384.64,-180.87C393.66,-167.83 403.78,-153.19 412.51,-140.58"/>
<polygon fill="#a65628" stroke="#a65628" points="415.48,-142.43 418.29,-132.22 409.72,-138.45 415.48,-142.43"/>
<text text-anchor="middle" x="422.5" y="-153.4" font-family="Times,serif" font-size="12.00" fill="#a65628">room</text>
</g>
<!-- N10&#45;&gt;N6 -->
<g id="edge5" class="edge">
<title>N10&#45;&gt;N6</title>
<path fill="none" stroke="#a65628" d="M301.29,-180.91C293.21,-175.24 285.23,-169.2 278,-163 268.18,-154.58 258.45,-144.21 250.34,-134.85"/>
<polygon fill="#a65628" stroke="#a65628" points="252.79,-132.33 243.67,-126.95 247.45,-136.85 252.79,-132.33"/>
<text text-anchor="middle" x="294.5" y="-153.4" font-family="Times,serif" font-size="12.00" fill="#a65628">guest</text>
</g>
<!-- N10&#45;&gt;N5 -->
<g id="edge8" class="edge">
<title>N10&#45;&gt;N5</title>
<path fill="none" stroke="#ff7f00" d="M345.15,-180.73C329.02,-141.88 303.62,-80.71 289.12,-45.79"/>
<polygon fill="#ff7f00" stroke="#ff7f00" points="292.24,-44.16 285.17,-36.27 285.77,-46.85 292.24,-44.16"/>
<text text-anchor="middle" x="336" y="-105.4" font-family="Times,serif" font-size="12.00" fill="#ff7f00">key</text>
</g>
<!-- N4 -->
<g id="node11" class="node">
<title>N4</title>
<polygon fill="#ffd700" stroke="#ffd700" points="850,-241 680,-241 680,-194 850,-194 850,-241"/>
<text text-anchor="middle" x="765" y="-227.4" font-family="Times,serif" font-size="12.00" fill="#000000">FrontDesk</text>
<text text-anchor="middle" x="765" y="-214.4" font-family="Times,serif" font-size="12.00" fill="#000000">lastKey: Room&#45;&gt;Key4</text>
<text text-anchor="middle" x="765" y="-201.4" font-family="Times,serif" font-size="12.00" fill="#000000">occupant: Room&#45;&gt;Guest1</text>
</g>
<!-- N4&#45;&gt;N3 -->
<g id="edge15" class="edge">
<title>N4&#45;&gt;N3</title>
<path fill="none" stroke="#e41a1c" d="M709.86,-193.84C696.59,-185.93 683.73,-175.75 675,-163 669.8,-155.4 667.26,-145.81 666.1,-136.85"/>
<polygon fill="#e41a1c" stroke="#e41a1c" points="669.58,-136.47 665.31,-126.78 662.6,-137.02 669.58,-136.47"/>
<text text-anchor="middle" x="727" y="-153.4" font-family="Times,serif" font-size="12.00" fill="#e41a1c">occupant [Room]</text>
</g>
<!-- N4&#45;&gt;N2 -->
<g id="edge14" class="edge">
<title>N4&#45;&gt;N2</title>
<path fill="none" stroke="#984ea3" d="M776.29,-193.73C781.23,-180.6 784.73,-163.97 779,-150 755.5,-92.64 690.79,-53.96 649.45,-34.27"/>
<polygon fill="#984ea3" stroke="#984ea3" points="650.79,-31.03 640.24,-30.01 647.85,-37.38 650.79,-31.03"/>
<text text-anchor="middle" x="816.5" y="-105.4" font-family="Times,serif" font-size="12.00" fill="#984ea3">lastKey [Room]</text>
</g>
<!-- N0 -->
<g id="node12" class="node">
<title>N0</title>
<polygon fill="#ffd700" stroke="#ffd700" points="922,-235.5 868,-235.5 868,-199.5 922,-199.5 922,-235.5"/>
<text text-anchor="middle" x="895" y="-214.4" font-family="Times,serif" font-size="12.00" fill="#000000">Key3</text>
</g>
<!-- N1 -->
<g id="node13" class="node">
<title>N1</title>
<polygon fill="#ffd700" stroke="#ffd700" points="994,-235.5 940,-235.5 940,-199.5 994,-199.5 994,-235.5"/>
<text text-anchor="middle" x="967" y="-214.4" font-family="Times,serif" font-size="12.00" fill="#000000">Key2</text>
</g>
</g>
</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