TLA+ ToolBox
TLA+にはToolBoxというeclipseベースの公式のIDEが付属する。
テキストエディタのフォントについて
デフォルトではテキストエディタで日本語が表示されない。コメントに日本語を使用すると文字化けしてしまう。
テキストエディタのフォントを変更することで日本語が表示される。
テキストエディタのフォント設定はFile > Prefernce > General > Appearance > Colors and Fonts から変更できる。
テキストエディタのフォントを変更することで日本語が表示される。
テキストエディタのフォント設定はFile > Prefernce > General > Appearance > Colors and Fonts から変更できる。
フォントについて
MSゴシックでは”\”(バックスラッシュ)が"\”(円マーク)になってしまうため、他のフォントがよい。例えば以下がある。
エラー表示について
以降で説明する各設定画面にエラーがある場合、控えめな小さい赤い×印が表示される (赤枠で囲った部分)。
Model Overview
TLA+ ToolBoxで作成した仕様に対してモデル検査を行うにはSpec Exploerから“New Model”を選択し、モデルを作成する。
Model Overviewからチェック内容を設定し、チェックを行う。
Model Overviewからチェック内容を設定し、チェックを行う。
Model description
モデルの詳細について記述するスペース。
What is the behavior spec?
| 項目 | 内容 |
|---|---|
| Initial predicate and next-state relation | 初期状態と次の状態の関係を指定し、状態遷移を検証する。 |
| Temporal formula | 時相理論を使用した検証を行う。 |
| No behavior spec | この項目を選択した場合、モデルチェックについては何も行われない。 Model Checking Results PageにあるEvaluate Constant ExpressionのExpressionに式を入力し、 実行ボタンを押すことでValueに式の評価結果が表示される。式をテストしたいときに使う。 |
What is the model?
モジュール内にCONSTANTSで定数を定義すると、このセクションに定数が表示される。定数の値を定義することができる。
上記ではCONSTANT に “Capacity”を定義している。What is the model? のセクションで表示されている”Capacity”を選択し、
Editボタンを押下すると以下のような画面が表示され、値を定義することができる。
Editボタンを押下すると以下のような画面が表示され、値を定義することができる。
定数の定義については型(Type)の定数を参照。
What to check?
モデルに対してTLCがチェックする内容を指定する。
- Deadlock
主に並行処理を検証する際に使用する。awaitは条件が満たされるまでプロセスの実行を除外する。すべてのプロセスが足止めをされた場合、TLCは実行可能なステップがなくなり、デッドロックと判断する。また、単一のプロセスの場合であってもNextで次に実行可能なステップが存在しなかったときに発生する。
- Invariants
不変条件を設定する。式以外にも演算子を定義することができる。不変条件とは常にある条件が成り立つことを示す。例えば車用の信号と歩行者用の信号が同時に青になること、銀行口座の残高がマイナスになるといったことが一瞬でも存在しないことを示す。
- Properties
時相論理を使った活性検査を行う。いつかは必ず何かの条件が成立するなどの検証に使われる。例えば歩行者はいつか横断歩道を渡れる。銀行口座に送金した金額は必ずいつか反映されるなど。
時相論理の[ ]とInvariantsは同じ意味であるのでInvariantsとの使い分けは微妙である。
時相論理の[ ]とInvariantsは同じ意味であるのでInvariantsとの使い分けは微妙である。
補足：活性検査はマルチスレッドに対応していないため、Invariantsで検証可能であればそちらを使う方がチェックにかかる時間は少なくて済む。
How to run?
TLCが使用するメモリ、スレッド数等を指定することができる。
‟Tune these parameters and set defaults”を選択するとTLC Optionsタブが開き、より詳細な設定をすることができる。
‟Tune these parameters and set defaults”を選択するとTLC Optionsタブが開き、より詳細な設定をすることができる。
Spec Options
Model Overview画面にて”Additional Spec Options”をクリックするとSpec Optionsタブが表示される。
Additional Definitions
状態制約や定数の定義で使用する演算子を追加することができる。定数用の複雑なセットアップが必要なときに役立つことがある。
Model Values
モデル値の集合を定義できる。
State Constraint
状態遷移の制限をかける。ここで定義された制約は常にTRUEとなる。
探索する状態空間が大きい場合に制約をかけることで探索範囲を限定し、現実的な時間で検証できることができる。
たとえばキューの長さをLenとしたとき”Len < 10”とするとLenは10未満に制限される。
除外された状態は検証されないため制約条件への違反を見逃す可能性はある。
探索する状態空間が大きい場合に制約をかけることで探索範囲を限定し、現実的な時間で検証できることができる。
たとえばキューの長さをLenとしたとき”Len < 10”とするとLenは10未満に制限される。
除外された状態は検証されないため制約条件への違反を見逃す可能性はある。
Definition Override
定義済みの演算子の定義を上書きできる。
Action Constraint
State Constraintと同様、何らかの制約を掛けることができるようだ。
TLC Options
Model Overview画面にて“Additional TLC Options”をクリックすると表示される。
Checking Mode
- 「Depth-first」にチェックをつけると深さ優先探索になる。
- Simulation Modeは全探索からランダム探索に切り替える。非常に大きな状態空間を全探索する代わりに、小さな状態空間で探索後、本来の状態空間をランダム探索して全探索の代わりとする場合などに使う。
Model Checking Results
モデル検査の結果が表示される。
Evaluate Constant Expression
“No Behaviro Spec”にチェックをつけることでモデル検査を実行せず、”Expression”内に記述した式を評価することができる。
仕様内に記述した定数、演算子は”Expression”内でも参照可能で仕様の記述中に式を試したい時などに利用する。
仕様内に記述した定数、演算子は”Expression”内でも参照可能で仕様の記述中に式を試したい時などに利用する。
[Amazon商品]
