[TLA+] 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通り。画像にするとこんな感じです。集合として被る部分はないので単純に集合の要素の合計数です。