Skip to content

Instantly share code, notes, and snippets.

@ksoda
Last active July 24, 2020 15:51
Show Gist options
  • Save ksoda/bd5a348d8f2fc78ea1a0552a793f8ce1 to your computer and use it in GitHub Desktop.
Save ksoda/bd5a348d8f2fc78ea1a0552a793f8ce1 to your computer and use it in GitHub Desktop.
実践的な例 Alloy part 3

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

Display the source blob
Display the rendered blob
Raw
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Display the source blob
Display the rendered blob
Raw
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Display the source blob
Display the rendered blob
Raw
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Display the source blob
Display the rendered blob
Raw
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Display the source blob
Display the rendered blob
Raw
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
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
Display the source blob
Display the rendered blob
Raw
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Display the source blob
Display the rendered blob
Raw
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Display the source blob
Display the rendered blob
Raw
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Display the source blob
Display the rendered blob
Raw
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Display the source blob
Display the rendered blob
Raw
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment