空席と売れた席の合計
モデル検査とは、システムが取りうる状態を全部たどって、決まりが破れないかを調べる方法です。TLA+ は状態と歩でシステムを書く言語で、検査器 TLC がそれを調べます。
映画館の予約システムでは、2席が売れるたびに、空席と売れた席の数が変わります。空席と売れた席の合計は、いつも2のはずです。その決まりが破れる動きを、TLC は最短で見つけます。
このレッスンのゴール
メモ
不変条件を書き、壊れたモデルの反例を読める。
重要な言葉
| ことば | いみ | れい |
|---|---|---|
| 状態 | 変数の値の組 | free = 2, sold = 0 |
| ステップ | 状態を次の状態に変える、1回の動き | |
| 不変条件 | どの状態でも成り立つはずの決まり | |
| 初期状態 | 動き出す前の、最初の状態 | |
| 反例 | 不変条件が破れるまでの、ステップの列 | |
| モデル検査 | 全部の状態をたどって決まりを調べること |
学生が入力するセルは、このプレビューでは空白です。
モデルは状態とステップでできる
予約のモデルは、2つの変数でできています。free は空席の数、sold は売れた席の数です。最初は、free が2、sold が0です。
動きは2つです。Sell は席を1つ売り、Refund は1つ払い戻します。決まりは「free + sold はいつも2」です。この決まりが、不変条件です。
予約のモデル
---- MODULE Seats ----
EXTENDS Naturals
VARIABLES free, sold
Init == free = 2 /\ sold = 0
Sell == free > 0 /\ free' = free - 1 /\ sold' = sold + 1
Refund == sold > 0 /\ free' = free + 1 /\ sold' = sold
Next == Sell \/ Refund
Spec == Init /\ [][Next]_<<free, sold>>
Conserved == free + sold = 2
====
TLA+の式の読み方
free' は、動いたあとの free を表します。Sell は「空席があり、空席が1減り、売れた席が1増える」という意味です。/\ は「かつ」、\/ は「または」です。
Next は、Sell か Refund のどちらかが起きることです。Spec は、最初が Init で、そのあとはいつも Next に従う、という意味です。Refund は、わざと誤りを入れてあります。
練習用のフォルダを作る
mkdir -p practice/seatsここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
モデルのファイルを書く
printf '%s\n' "---- MODULE Seats ----" "EXTENDS Naturals" "VARIABLES free, sold" "Init == free = 2 /\ sold = 0" "Sell == free > 0 /\ free' = free - 1 /\ sold' = sold + 1" "Refund == sold > 0 /\ free' = free + 1 /\ sold' = sold" "Next == Sell \/ Refund" "Spec == Init /\ [][Next]_<<free, sold>>" "Conserved == free + sold = 2" "====" > practice/seats/Seats.tlaここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
TLCに不変条件を調べさせる
tlc practice/seats/Seats Conserved | grep -E "^(Error|State|/)"ここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
反例は最も短いステップの列
TLC は、初期状態から近い順に状態をたどります。だから、最初に見つかる反例は、最も短いステップの列です。
出力の State 1 から State 3 が、その列です。各状態に変数の値があり、State 2 と State 3 の見出しが、どの動きで来たかを示します。
反例の3つの状態
| 状態 | したこと | free | sold | free + sold |
|---|---|---|---|---|
| 1 | 最初（Init） | 2 | 0 | 2 |
| 2 | Sell | 1 | 1 | 2 |
| 3 | Refund | 2 | 1 | 3 |
学生が入力するセルは、このプレビューでは空白です。
直すと、不変条件は破れない
直し方は、払い戻しで売れた席を1つ減らすことです。Refund の sold' = sold を sold' = sold - 1 にします。
直したモデルは SeatsFixed.tla に別に書き、同じ不変条件を調べます。TLC は、全部の状態をたどって、破れる状態がなければ、エラーなしと答えます。
直したモデルを書く
printf '%s\n' "---- MODULE SeatsFixed ----" "EXTENDS Naturals" "VARIABLES free, sold" "Init == free = 2 /\ sold = 0" "Sell == free > 0 /\ free' = free - 1 /\ sold' = sold + 1" "Refund == sold > 0 /\ free' = free + 1 /\ sold' = sold - 1" "Next == Sell \/ Refund" "Spec == Init /\ [][Next]_<<free, sold>>" "Conserved == free + sold = 2" "SomeFree == free > 0" "====" > practice/seats/SeatsFixed.tlaここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
直したモデルを調べる
tlc practice/seats/SeatsFixed Conserved | grep "No error"ここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
正しいモデルでも破れる決まり
不変条件が破れたからといって、モデルが間違っているとは限りません。決まりのほうが間違っていることもあります。
直したモデルには、もう1つ SomeFree == free > 0（いつも空席がある）を書きました。2席とも売れれば、この決まりは破れます。
空席がいつもあるか調べる
tlc practice/seats/SeatsFixed SomeFree | grep -E "^(Error|State|/)"ここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
よくある間違い
注意
反例が出たら、モデルが壊れている、と思いがちです。そうとは限りません。反例は、決まりかモデルのどちらかが間違っているという知らせです。反例を読んで、どちらの考えが間違っていたかを決めるのは、人です。
反例を読んだあとの判断
| 反例の様子 | 間違っているのは | 直し方 |
|---|---|---|
| 現実にありえない動きがある | モデルのステップ | ステップの条件を直す |
| 現実にありうる状態で破れた | 不変条件 | 決まりを言い直す |
| 何度調べても破れない | 決まりが弱い | 破れる版で試して確かめる |
学生が入力するセルは、このプレビューでは空白です。
さらに挑戦: 3席にする
SeatsFixed.tla を別の名前でコピーし、free = 2 を3、Conserved の2を3に変えましょう。TLC は何と答えるでしょうか。
次に、Init だけを3にして、Conserved は2のままにします。今度は、何歩目で破れるかを予想してから、確かめましょう。