\( \def\ldef{\ \ :=\ } \) \( \def\rdef{\overset{\triangle}{=}} \) \( \def\globally{□} \)

TLA+

Takami Torao TLC2 #TLA+ #TLC #PlusCal
  • このエントリーをはてなブックマークに追加

概要

TLA+ (temporal logic of actions plus) は時相論理と振る舞いの論理を組み合わせた、並行処理と分散システム向けに設計された高レベルモデリング言語。形式仕様記述としてシステムやアルゴリズムなどのクリティカルな部分の設計エラーを定性的に検出することを目的としている。

TLA+ はシステムやアルゴリズムをステートマシンの観点での離散ベントの連続として抽象化する。TLA+ ではある状態から次の状態への変化を一つのステップとし、状態の変化の連続を振る舞い (behaviour) とする。どのような振る舞いが許可されるかのチェックはアサーションであり、全てのアサーションを記述することは仕様化 (specify) である。

TLA+ の難しい点は機能要件をステートマシンに抽象化することと言われている。ステートマシンの振る舞いは 1) 取りうる初期状態2) 各状態が取りうる次の状態の 2 点で抽象化することができる (取りうる次の状態が存在しないときシステムは halt する)。TLA+ ではシステムの状態を表すために必要な変数とその初期状態、各変数間の関連と次の状態への遷移を定義することでその仕様を記述する。そして、システムがステップを進行するごとに "正しい状態" の要件を満たしているかをチェックして "正しく動く" ことを検証する。

PlusCal はステートマシン風の TLA+ を逐次処理向けの記述ができるようにアレンジした言語であり、最終的に TLA+ にトランスパイルされて検証が行われる。

  1. 概要
  2. 環境設定と TLC の実行
  3. 最初の TLA+: TickTack
    1. 基本的な TLA+ の記述
    2. TLC の結果とエラーの検出
  4. 時相論理演算子: 独立した 2 変数のシステム
    1. 例: 逐次処理
      1. TLA+ での表現
  5. 参照

環境設定と TLC の実行

実際の TLA+ を記述する前に、まず Visual Studio Code (vscode) の TLA+ 拡張機能を使用した TLA+ の記述と検証方法について説明しよう。TLA+ 拡張機能の詳細については公式サイトの Wiki を参照。

  1. Visual Studio Code のサイトから vscode をダウンロードしてインストールし、拡張機能のマーケットプレイスから TLA+ の拡張機能を追加する。

    Fig 1. Visual Studio Code の TLA+ 拡張機能。
  2. vscode 上でプロジェクトを作成して TickTack.tla というファイルに以下の TLA+ での振る舞いを記述する (TickTack は後に例示する)。ここでファイル名は MODULE に指定した名前と同じ名前にすることに注意。

    Fig 2. vscode でシンタックスハイライトされたコード。
  3. TickTack.tla ファイルを右クリックして "Check models with TLC" を選択すると、初回は TickTack.cfg ファイルを作成するように誘導される。この cfg ファイル (モデルファイル) では TickTack モジュールで使用する定数などの具体値を指定できるが、ひとまずこの例では INIT (取りうる初期状態) と NEXT (各状態が取りうる次の状態) の定義とのマッピングのみを指定する。

    Fig 3. モデルファイルの作成。
  4. 再び TickTack.tla を右クリックして "Check models with TLC" を選択すると TLC が起動してチェックの結果が表示される。TLC とは TLA+ で記述された仕様に対して状態モデルのチェックを行うプログラムである (TLC は Java で実装されているためコマンドラインから Java を起動できるようにしておく必要があるかもしれない)。

    Fig 4. TickTack 仕様の検証結果。

    結果 Status 右上の "Full output" をクリックすると以下のような TLC 出力の詳細が表示される。

    Full output
    java.exe -cp "c:\Users\Takami Torao\.vscode\extensions\alygin.vscode-tlaplus-1.5.2\tools\tla2tools.jar" -XX:+UseParallelGC tlc2.TLC TickTack.tla -tool -modelcheck -coverage 1 -config TickTack.cfg
    
    TLC2 Version 2.16 of 31 December 2020 (rev: cdddf55)
    Running breadth-first search Model-Checking with fp 79 and seed -6110106979511870660 with 1 worker on 24 cores with 7266MB heap and 64MB offheap memory [pid: 18816] (Windows 10 10.0 amd64, Oracle Corporation 11 x86_64, MSBDiskFPSet, DiskStateQueue).
    Starting SANY...
    Parsing file C:\Users\Takami Torao\git\sample.tla-plus\TickTack.tla
    Semantic processing of module TickTack
    SANY finished.
    Starting... (2021-02-05 02:23:10)
    Computing initial states...
    Finished computing initial states: 2 distinct states generated at 2021-02-05 02:23:11.
    Model checking completed. No error has been found.
      Estimates of the probability that TLC did not check all reachable states
      because two distinct states had the same fingerprint:
      calculated (optimistic):  val = 2.2E-19
    The coverage statistics at 2021-02-05 02:23:11
    <Init line 3, col 1 to line 3, col 4 of module TickTack>: 2:2
      line 3, col 9 to line 3, col 20 of module TickTack: 2
      |line 3, col 15 to line 3, col 20 of module TickTack: 1:3
    <tick line 4, col 1 to line 4, col 4 of module TickTack>: 0:1
      line 4, col 9 to line 4, col 13 of module TickTack: 3
      |line 4, col 9 to line 4, col 9 of module TickTack: 2
      line 4, col 18 to line 4, col 23 of module TickTack: 1
    <tack line 5, col 1 to line 5, col 4 of module TickTack>: 0:1
      line 5, col 9 to line 5, col 13 of module TickTack: 3
      |line 5, col 9 to line 5, col 9 of module TickTack: 2
      line 5, col 18 to line 5, col 23 of module TickTack: 1
    End of statistics.
    Progress(1) at 2021-02-05 02:23:11: 4 states generated (501 s/min), 2 distinct states found (250 ds/min), 0 states left on queue.
    4 states generated, 2 distinct states found, 0 states left on queue.
    The depth of the complete state graph search is 1.
    The average outdegree of the complete state graph is 0 (minimum is 0, the maximum 0 and the 95th percentile is 0).
    Finished in 483ms at (2021-02-05 02:23:11) 

    ここでは Success と表示されていることから TickTack システムが取りうる全ての状態で仕様を満たしていることがわかる。

  5. TLA+ で記述した仕様は [View]-[Command Palette...] メニューまたは CTRL+Shift+P ショートカットを使って LaTeX または PDF に出力することができる。PDF 化には latex コマンドを求められるが、ローカルに LaTeX をインストールしていない場合は overleaf などのサイトにファイル内容をコピーして生成することもできる。

    Fig 5. LaTeX 形式で出力し PDF 化した "公式な表現の" TickTack システム仕様。

最初の TLA+: TickTack

システム状態を表す最も簡単な例として 0 と 1 の状態を交互にとる TickTack システムについて考えてみよう。

TLA+ による仕様の構築は (個人の経験的に) 以下の手順で行う。

  1. 目的のシステムに必要な振る舞いを定義する。
  2. 振る舞いが機能するために必要な状態変数を定義する。
  3. 全ての振る舞いを初期状態 (Init) と次の状態 (Next) で記述する。
  4. 振る舞いが正しいことをチェックするアサーションを作成する。

まず最初に、この TickTack システムの要件は以下の一つの振る舞いで表すことができる。

システムは 0 と 1 の状態を交互にとる。

この振る舞いを表すためには 0 か 1 かどちらかの値をとる単一の変数 \(t\) があれば十分である。\(t\) の初期状態は 0 または 1 のどちらでも許容できるため \({\it Init} \ldef t \in \{0, 1\}\) と定義することができる。

TLA+ ではあるステップの状態変数を \(x\) としたとき、その変数の次のステップでの状態を \(x'\) (\(x\)-プライム) と表現する。言い換えると「\(x'\) はこのステップで \(x\) に起きた変化」である。つまりこの TickTack システムの例では、\(t=0\) は次のステップで \(t=1\) となることから \(t'=1\) であり、同様に \(t=1\) は次のステップで \(t=1\) となることから \(t'=0\) である。これは: \[ \begin{eqnarray*} {\it Next} & \ldef & {\sf IF} \ t=0 \ {\sf THEN} \ t'=1 \ {\sf ELSE \ IF} \ t=1 \ {\sf THEN} \ t'=0 \\ & \equiv & (t = 0 \land t' = 1) \lor (t = 1 \land t' = 0) \end{eqnarray*} \] と表すことができる。

基本的な TLA+ の記述

TickTack の仕様として必要なアサーションは以下のように表現できる。\[ \begin{eqnarray*} {\it Init} & \ldef & t \in \{0, 1\} \\ {\it Next} & \ldef & (t = 0 \land t' = 1) \lor (t = 1 \land t' = 0) \end{eqnarray*} \] この仕様を TLA+ で表現すると以下のような記述となる。

---- MODULE TickTack ----
VARIABLES t
Init == t \in {0, 1}
tick == t = 0 /\ t' = 1
tack == t = 1 /\ t' = 0
Next == tick \/ tack
====

順番に説明しよう。まずモジュールという大きな単位があり、1 行目と 7 行目のように ---- MODULE モジュール名 ---- で始まり ==== で終了する。またモジュール中の ---- は可読性のための罫線として使用することができる。これらは 4 文字以上の - または = であれば良い。

2 行目の VARIABLES変数宣言でシステムで使用する状態変数を定義している (最後の S は省略可能で VARIABLE でも良い)。ここでは 0 または 1 のシステム状態を保持するために一つの変数 \(t\) を宣言している。

3 行目の Initシステムの取りうる初期状態 \(t \in \{0,1\}\) を定義している。一般的なプログラミング言語が具体値を「代入」するのに対して、仕様記述言語では仕様が満たすべき条件を「定義」する点で少し意味が異なることに注意。

4-6 行目はシステムが次に取りうる状態を表す Next と、その部品となる tick および tack を定義している。TLA+ では /\ が論理積 \(\land\)、\/ が論理和 \(\lor\) を表している。

t'次のステップで \(t\) がとるべき値である。したがって、例えば tick は \(t=0 \land t'=1\) つまり「ステップ開始時の \(t\) が 0 で次のステップに引き継ぐ \(t\) が 1 となる」というアサーションを定義している。これは条件文として if \(t=0\) then \(t'=1\) と等価とも言える。

システムの "取りうる初期状態" と "次に取りうる状態" の定義がモデルファイル TickTack.cfgINITNEXT で指定できることは先に述べた。したがって InitNext には任意の定義名をつけることができる。

またこの例では使用していないが TLA+ の記述では (* block comment *)\* line comment 形式のコメントを使用することができる。

TLC の結果とエラーの検出

TLA+ での記述により TickTack システムの仕様は以下の 2 点に明文化されたステートマシンとして表現できるようになった。

  1. システムの初期状態は \(t \in \{0, 1\}\) である。
  2. 全てのステップで状態は \((t=0 \land t'=1) \lor (t=1 \land t'=0)\) である。

また TLC によってこれらの状態モデルに矛盾がないこと、つまり上記 2 つのアサーションが TickTack システムで取りうる全ての状態に対して成功することが検証された。TLA+ では \(t\) がどのような過程を経て \(t'\) に変化するかを詳細に説明することなく、ステップの前後の状態にのみ着目している点に注意。

ではここで未定義の状態を生成するような修正を加えて TLC がどのように振る舞うかを見てみよう。Fig 6 は \(t=1\) の時に \(t'=2\) となる可能性を追加した仕様とその結果である。

Fig 6. 未定義の状態が発生するケースを追加したバージョンとその TLC チェック結果。

このエラーは「初期状態 \(t=1\) で開始し tack を通過したあとに \(t=2\) (未定義の状態) となり halt します」ということを伝えている。つまり設計者は \(t=2\) という予期しない状態を設計として排除するか、\(t=2\) となるケースを正しい仕様として考慮しなければならない。

時相論理演算子: 独立した 2 変数のシステム

前述の TickTack システムは単一の変数だけだったため単純に状態変化をステップとみなすことができた。しかし 2 つ以上の独立した状態変数で構成されるシステムではある値が変化したときに別の値が変化しているとは限らない。このようなシステムでは特定の状態変数に対して変化しないステップを仕様として許可する必要がある (このような状態変数が変化しないステップをスタッターステップ (stuttering step) と呼ぶ)。

TickTack システムを少し拡張して時刻のみを表示する時計について考える (これは Specifying Systems [1] の最初の例と同じ)。時刻 \(hr\) は 1 から 12 のいずれかの数値であり、表示の切り替わり (ステップ) には時刻が加算され 12 を超えるケースに限り 1 となる。したがって初期状態と次の状態の 2 つのアサーションは以下のように表すことができる。\[ \begin{eqnarray*} {\it HCinit} & \ldef & hr \in \{1, \ldots, 12\} \\ {\it HCnxt} & \ldef & hr' = hr + 1 \ \mbox{if} \ hr \ne 12 \ \mbox{else} \ 1 \end{eqnarray*} \] ここで時相論理演算子 (temporal logic operator) の Globally を導入し、\(\globally F\) を \(F\) が常に true であることを主張するアサーションとする。つまり \(\globally {\it HCnxt}\) は動作のすべてのステップで \({\it HCnxt}\) が true であるというアサーションである。したがって式 (\(\ref{hc_def1}\)) はこの動作の全てを記述している仕様である。\[ \begin{equation} {\it HCinit} \land \globally{\it HCnxt} \label{hc_def1} \end{equation} \]

時計が独立した単独のシステムであればこの仕様の記述は適切である。ただし時計がシステムの一部で、例えば気温と同時に表示されるようなケースでは、時刻を表す \(hr\) と温度を表す \(tmp\) の 2 つの変数で表示される。この場合、温度の変化がありながら時刻は変化していないという表示の切り替わりケースがあることから \(hr\) を変更しないステップを許可する必要がある。\[ {\it HCinit} \land \globally ({\it HCnxt} \lor (hr' = hr)) \] このようなステップをスタッターステップ (stuttering step) と呼ぶ。時計の仕様は \({\it HCnxt}\) とスタッターステップを許可する必要がある。TLA では \({\it HCnxt} \lor (hr'=hr) \equiv [{\it HCnxt}]_{hr}\) と書くためよりシンプルに式 (\(\ref{hc_def2}\)) のように書くことができる。\[ \begin{equation} {\it HC} \ldef {\it HCinit} \land \globally [{\it HCnxt}]_{hr} \label{hc_def2} \end{equation} \] この仕様では時計がある時刻を示したあとに永久にスタッターステップを繰り返す (つまり時計が止まる) ことを許容している点に注意。

時間である \(hr\) に小数が付加されたり無理数や虚数になることはないため、\({\it HC} \Rightarrow \globally {\it HCinit}\) はあらゆる状況で成り立たなければならない。あらゆる状況で成り立つ時相式は定理 (theorem) と呼ばれる。

例: 逐次処理

The TLA+ Video Course で例示しているプログラムを使用して説明する。以下のようなプログラムは:

int i = 0;
void main(){
  i = someNumber();  // pc = "start"
  i += 1;            // pc = "middle"
}

仕様化された数式および TLA+ として以下のように表現することができる。これは元のプログラムとよく似ているが、プログラムが実行を表しているのに対して、仕様化された数式および TLA+ はステートマシンの状態が仕様に準拠しているか否かの true/false のみを表していることに注意。ここで各ステップは TLA+ の慣習として変数 pc を用いて識別している。

Init == (pc = "start") /\ (i = 0)
Next == \/ /\ pc = "start"
           /\ i' \in 0..1000
           /\ pc' = "middle"
        \/ /\ pc = "middle"
           /\ i' = i + 1
           /\ pc' = "done"
\[ \begin{eqnarray*} {\it Init} & \ldef & pc = \mbox{"start"} \ \mbox{and} \ i = 0 \\ & \equiv & (pc = \mbox{"start"}) \ \land \ (i = 0) \\ {\it Next} & \ldef & \mbox{if} \ pc = \mbox{"start"} \ \mbox{then}\\ && \ \ \ i' \in \{0, \ldots, 1000\} \ \mbox{and} \ pc' = \mbox{"middle"} \\ && \mbox{else if} \ pc = \mbox{"middle"} \ \mbox{then}\\ && \ \ \ i' = i + 1 \ \mbox{and} \ pc' = \mbox{"done"} \\ && \mbox{else} \ \mbox{false} \\ & \equiv & ((pc = \mbox{"start"}) \land (i' \in \{0, \ldots, 100\}) \land (pc' = \mbox{"middle"})) \\ && \lor ((pc = \mbox{"middle"}) \land (i' = i + 1) \land (pc' = \mbox{"done"})) \end{eqnarray*} \]

変数 x は \(x\) の現在の値、それにプライムが付いた変数 x' は \(x\) の次の値をそれぞれ表している (つまり x' として表されている変数は次のステップでは x として現れる)。

AND, OR はそれぞれ数学記号 \(\land\) と \(\lor\) に倣って /\\/ で表す。これらは従来の数式のように二項演算子として表記する以外にリストのように書くこともできる。\(\land\) と \(\lor\) はともに可換であり左右のオペランドを交換できる。

集合と包含 \(x \in \{0,\ldots,100\}\) は x \in 0..100 のように表す。

ステートマシンに基づく TLA+ の記述は UML の状態遷移図と親和性が良い。状態遷移図としては Fig 1 のように表すことができる。

Fig 1. UML での状態遷移図。

TLA+ で逐次処理を記述するとき 1) 実行中の位置を保持する状態変数を導入し (変数名は慣習的に pc とする)、2) 各ステップごとに状態チェックを定義し、3) 最終的に仕様は \({\it Init} \ \cap \ \globally [{\it Next}]_x\) の形式になる。しかし、現実問題として全てのステップにユニークな名前をつけることは煩雑な作業である。これらの 3 つの特徴を DSL 化したものが PlusCal である。

TLA+ での表現

参照

  1. Leslie Lamport (2002), Specifying Systems.
  2. Leslie Lamport (2020), A PlusCal User’s Manual P-Syntax Version 1.8.
  3. LEARN TLA+
F