[TLA+] TLA+の基本的な文法

小室 啓

2019.02.18

この記事は公開されてから1年以上経過しています。情報が古い可能性がありますので、ご注意ください。

こむろ＠札幌です。寒すぎる。

自分の場合、自分なりの理解をしてある程度納得した上でないと文章にまとめられないため、しばらく時間がかかると思うのですがのんびりやっていこうと思います。

はじめに

ひとまず前回単純なC言語のプログラムの動作をTLA+で表現するところまで確認しました。今回はTLA+の文法と仕様のチェックについて確認します。

前回のコード

前回のコードは以下の通り。

--------------------------- MODULE SimpleProgram ---------------------------
EXTENDS Integers

VARIABLES i, pc

Init == (pc = "start") /\ (i = 0)

Pick == /\ pc = "start"
        /\ i' \in 1..1000
        /\ pc' = "middle"

Add1 == /\ pc = "middle"
        /\ i' = i + 1
        /\ pc' = "done"

Next == \/ Pick \/ Add1
=============================================================================
\* Modification History
\* Last modified Fri Jan 25 11:34:26 JST 2019 by komurohiraku
\* Created Fri Jan 25 11:18:28 JST 2019 by komurohiraku

今回はここから。

文法とその意味

簡単な抽象コードから文法を確認していきます。

開始と終了

TLA+のコードはこのセクション内に記述します。この中に記述されたコードが解析の対象になります。

----------MODULE SimpleProgram----------

========================================

開始セクション ---- の MODULE にモジュール名を記述します。ここの名称は.tla のファイル名と同一にします。違反した場合は以下のようなパースエラーが発生します。

EXPORT

Javaにおけるimport に相当します。他のモジュールを読み込み、その中に定義されているコードを利用できます。他にも INSTANCE があるようですが、ひとまず今は利用しません。

今回は Integers というモジュールを読み込んでいます。これはTLA+インストール時にデフォルトで用意されているモジュールの一つです。数値計算や数値集合表現が定義されています。

今回このモジュールで利用しているのは以下の2つです。

  • 数値の集合表現 {1..10}
    • これは数値集合の簡易表現です。この場合、{1,2,3,4,5,6,7,8,9,10} と同等の集合を表します。
  • 数値計算 i+1

いずれもIntegers モジュールに依存しているため、このモジュールがないとコードのパースに失敗します。

同じようなモジュールに Naturals があります。こちらは自然数を扱うためのモジュールです。

Integers はこのモジュールを拡張し、負の値を扱うことが出来ます。定義を覗いてみます。定義へのジャンプはMacの場合、 Command + Click で可能です。 Integers のモジュール

-. a == 0 - a

実は他にも `Int` の定義があるのですがこちらはダミー定義になっており、実体は別にあります。とりあえず今回はこういうモジュールがあるんだな程度でスルーします。

VARIABLES

状態変数の宣言。i と pc を定義します。SpecにおいてGlobalな変数として定義されます。

=と==の違い

通常のプログラミング言語と異なり、= と == の意味が逆になります。それぞれ 代入（もしくは定義）, 比較 を表現しています。

TLA+において == は define となり、代入や定義を表します。= は比較を表します。原則はこうなっていますが、一部Contextや記述された箇所によって微妙に異なることがあるので少々注意が必要です。

Label

今回のコードで Pick == や Add1 == といった式が出てきています。これらはLabelをつけて式をグルーピングして見やすくしたものです。基本的にTLA+ではInit StateとNext Stateさえ定義していれば問題ないようです。実際、Labelを全て取っ払って以下のように定義しても意味は代わりません。

Init == (pc = "start") /\ (i = 0)

Next == \/ ((pc = "start") /\ (i' \in 1..1000) /\ (pc' = "middle"))
        \/ ((pc = "middle") /\ (i' = i + 1) /\ (pc' = "done"))

ただ、単純な仕様であればこのように式をすべて並べて書いてしまってもよいですが、なかなか読み解くのは大変です。可読性が著しく低下しますので、式の複雑さを鑑みて、適度にグルーピングすることが好ましいかと思います。 *1

Init state

VARIABLES で定義した変数の初期値を定義します。変数は一通り初期化してから使用します。

Init == (pc = "start") /\ (i = 0)

== はdefinesと読み替えます。pc = "start" とi=0 を初期値とします。いきなり原則を破りますが、ここでの = は 現在の 変数への代入として読みます。比較演算ではありません。

/\ この記号は AND に相当します。TLA+は基本的に論理演算の集合です。代入に関しては問答無用でTRUE が返ってくるため、式 Initは、TRUE AND TRUE となり、式の最終的な評価は TRUE となります。

通常のプログラム言語ではよく明示的に初期値を設定せずとも問題ないものがあります。しかしTLA+では未定義の状態というのは許可されません。そのため、 Init State での初期値設定を省くと変数の利用ができません。

current state is not a legal state
While working on the initial state:
/\ i = null
/\ pc = "start"

Next state

Initial Stateで変数の初期状態を全て定義しました。Next Stateでは、変数の取りうるすべての値域と状態遷移を式で表記し、取りうる変数の組み合わせの集合を定義します。。

Next == \/ Pick \/ Add1

\/ は OR に相当します。

この式では Pick という式と Add1 という式を評価しその結果を OR でつなぎます。論理演算なので交換則が成り立ちます。そのため以下でも同じ結果を得ることが出来ます。

Next == \/ Add1 \/ Pick

OR でそれぞれの状態を表す式をつなぐことで、すべての取りうる状態の集合を表現できます。

この式の場合、Pick は 1..1000 すなわち 1000通り の状態を集合として表現します。Add1 は i＋1 の演算のみですが、これもそれぞれの i に 1状態 を追加します。これが 1000通り あるため合計で2000通りの集合。プラスして初期状態で1通り。画像にするとこんな感じです。集合として被る部分はないので単純に集合の要素の合計数です。

これらの状態すべてを検査し、未定義の状態や矛盾した状態がないかを確認するのが最終的な目的です。

検証

さっそくすべての組み合わせを検査してみましょう。TLA+ではモデルを作成し、検証します。TLC Model Checker メニューから New Model を選択。Model名を適当に入力します（デフォルトは Model_1）

作成すると以下のようなOverviewが表示されます。

Initial predicate and next-state relation が空の場合があります。その場合はチェックを入れた上で、それぞれ先程定義した Init, Next を指定します。

TLA+は.tla ファイルに仕様を記述し、Model には様々な状態や外部から入力する初期定数、各状態における不変的な値の条件等の設定を定義します。この2つを組み合わせて、膨大な状態の組み合わせから仕様の矛盾がないかをチェックします。

Model Overviewの上のほうにある緑の実行ボタン。これが検査の実行になります。

実行してみましたが失敗しました。左のペインには状態数やコンソール出力等々が表示されます。右ペインは主にエラー表示になります。

Deadlock

このエラーは何かという問題があります。このエラーは終了状態が定義されていない際に表示されるエラーとのこと。

Deadlock reached.

i' = i + 1 の i について何も評価していません。そのため、この i が宙ぶらりんであるためこのエラーが表示されます。このDeadlockは意図的に評価の対象から外すことが可能です。以下の該当チェックを外します。

これで検証を再度実行します。

今度はすべての状態を確認できました。 No errors でFinishしているのがわかります。これで、C言語で書かれたプログラムの仕様は (Deadlock reachedの問題はあるものの) 矛盾なく、エラーもないことを確認できました。

まとめ

TLA+の具体的なコードを例に基本的な文法を確認しました。既存のプログラミング言語とは全く異なり、どちらかというと数学的な考えが色濃く出ているため非常に見慣れない記述が多く出てきています。集合と論理演算の基本がある程度わかっていれば、そこまで理解に迷うことはないと思います。（今の所）

仕様を記述という特性上、実装の詳細を意識してしまうとうまく表現できません。そのため、何ができるべきなのかにフォーカスして考える必要があるため、なかなか変換が難しい。これでようやくLv1。まだまだ先は長い。

Lamport先生の動画を見ると、ここに書いた以上に細かくガイドされています。実際のコードの抽象化をもっと細かいステップで確認したい場合確認してみると良いかと思います。

次回はまた別の仕様で。

参照

脚注

  1. 実際Lamport先生の動画では、一度この長い式に落としてからグループ分けを行っています。 ↩
*