\def\ldef{≜}

\def\globally{□}

\def\eventually{◇}

\def\openleftarrowplus{\overset{+}{⇾}}

\def\equalv{⫤}

翻訳: PlusCal/TLA⁺: An Annotated Cheat Sheet

2021年3月27日 2019年の論文 #PlusCal #TLA+

Stephan Merz
stephan.merz@loria.fr

Abstract

この文書は Toolbox と TLC を使用している PlusCal および TLA+ ユーザが遭遇するであろう主な構成要素を要約することを目的としている。これは TLA+ に関する入手可能な入門資料に代わるものではなくリファレンスマニュアルとしての意味もない。著者へのフィードバックは大歓迎です。

Abstract
1 PlusCal
2 TLA⁺
3 オンラインリファレンス
翻訳抄

1 PlusCal

PlusCal は並行アルゴリズムを記述する命令形擬似コードの "look and feel" を持つアルゴリズム言語である。PlusCal は TLA+ に翻訳されることで形式的なセマンティクスを持ち、TLA+ のツールを使用してアルゴリズムを検証することができる。我々はここで "C 構文" で説明するが、Pascal 言語に近い "P 構文" も存在する。

PlusCal アルゴリズムは TLA モジュール内のコメントの中に現れる。トップレベルの構文は以下の通り。

--algorithm name {
  (* グローバル変数宣言 *)
  (* 演算子定義 *)
  (* マクロ定義 *)
  (* プロシジャ *)
  (* アルゴリズム本体、もしくはプロセス宣言 *)
}

変数宣言、オペレータとマクロ定義、プロシジャはオプションである。アルゴリズム本体 (逐次アルゴリズムの場合) またはプロセス宣言 (並行アルゴリズムの場合) のいずれかが必要である。

PlusCal トランスレータは PlusCal アルゴリズムに対応する TLA+ 仕様記述を、アルゴリズムが存在するモジュールの中の、アルゴリズムの直後に埋め込む。翻訳は次の行で区切られている。

\* BEGIN TRANSLATION
...
\* END TRANSLATION

この領域は PlusCal トランスレータが起動するたびに上書きされるのでユーザが触れてはいけない。ただし、TLA+ 定義は PlusCal アルゴリズムの前や、生成された TLA+ 仕様のあとに配置しても良い。特に PlusCal アルゴリズムの前に定義された演算子はアルゴリズムで使用することができる。correctness プロパティはトランスレータによって宣言された変数を参照するため、生成された仕様の下で定義される。

2.1 変数宣言

変数は以下のように宣言される。これらは (必須ではないが) 初期化できる:

variables x, y=0, z \in {1,2,3};

"variables" 句が使用できるのは最大で一つのみだが、任意の数の変数を宣言できることに注意。この例では $x$ , $y$ および $z$ の 3 つの変数を宣言している。変数 $x$ は初期化されず、 $y$ は 0 に初期化され、 $z$ は初期値として 1, 2 または 3 のいずれかを取ることができる。モデル検査中、TLC はデフォルト値として $x$ に特殊な値を割り当て、 $z$ に対する 3 つの初期値のすべてを探索する。

2.2 演算子定義

TLA+ と同様に (後述)、演算子はアルゴリズムを記述するためのユーティリティ関数を表している。構文は後述する TLA+ の定義と同じである。例えば

define {
  Cons(x,s) == << x >> \o s
  Front(s) == [i \in 1 .. Len(s)-1 |-> s[i]]
}

は要素 $x$ をシーケンス $s$ の前に付加する演算子 ${\it Cons}$ と、空ではないシーケンスから最後の要素を除いたサブシーケンスを生成する演算子 ${\it Front}$ を宣言している。繰り返しになるが、単一の "define" 句に区切り記号無しで任意の数の演算子定義を含むことができる。

2.3 マクロ

マクロはアルゴリズムに挿入できる複数の PlusCal ステートメントを表し、パラメータを持つことができる。定義された演算子とは対照的に、マクロは再帰を使用できず、ラベルやループ、プロシジャ呼び出し、return ステートメントなどの複雑なステートメントを含むことができない。以下に 2 つの例を示す:

macro send(to, msg) {
  network[to] := Append(@, msg)
}
macro rcv(p, var) {
  await Len(network[p]) > 0;
  var := Head(network[p]);
  network[p] := Tail(@)
}

これらのマクロは、プロセスでインデックス付けされた FIFO キューによって表現されているネットワークでの送受信操作を表している。最初のマクロはメッセージを宛先のプロセスのキューに追加している。2 番目のマクロは、プロセス $p$ のキューに少なくとも 1 つのメッセージが到着するまでブロックし、キュー内の最初のメッセージを変数 ${\it var}$ に割り当て、そのキューから削除する。マクロを使用する場合は、プロセス $p$ 宛に値 $x+1$ を送信するのであれば send(p, x+1) のように、コード内にステートメントとして呼び出しを挿入するだけである。

2.4 プロシジャ

プロシジャ宣言はマクロ宣言と似ているが、ローカル変数宣言¹を持つことができる。プロシジャ本体にはプロシジャ呼び出し (再帰的呼び出しでも) を含む任意のステートメントを含めることができる。

procedure p(x,y)
    variable z=x+1 \* プロシジャローカル変数
{
    call q(z,y);
l:  y := y+1;
    return
}

プロシジャのパラメータは変数とみなされ代入することができる。プロシジャの制御フローは return ステートメントに到達する必要があり、プロシジャによって計算された結果は変数 - おそらくパラメータ - に格納される必要がある。プロシジャ呼び出しの前にはキーワード call を付け、その後にラベルを付ける必要がある。

PlusCal トランスレータにはプロシジャを処理するためのスタックが導入されているため、プロシジャを使用する PlusCal アルゴリズムは標準モジュール Sequences を EXTENDS するモジュールに含める必要がある。

2.5 プロセス

PlusCal アルゴリズムは 1 つまたは複数のプロセステンプレートを宣言することができ、各プロセステンプレートは複数のインスタンスを持つことができる。プロセステンプレートは以下のようになる:

process (name [= | \in] e)
  variables ... \* プロセスローカル変数
{
  (* プロセス本体 *)
}

" ${\it name}=e$ " の形式では、プロセス ID が (式の値である) $e$ となるプロセスのインスタンスが 1 つ生成される。また " ${\it name} \in e$ " では、集合 $e$ の要素ごとにプロセスインスタンスが 1 つ生成される。異なるテンプレートから複数のプロセスインスタンスを生成するためには、すべてのプロセス ID が比較可能であり、かつユニークとなるようにすることが重要である。例えば整数のみ、文字列のみを、モデル値のみを使用するなど。プロセス本体の中ではプロセス ID は self で参照することができる (構文から想像される name ではなく)。プロセスは概念的には、アルゴリズムの実行開始時点から (非同期に) 並行して実行される: PlusCal では実行中にプロセスを動的に生成することはサポートしていない。

2.6 PlusCal ステートメント

PlusCal のステートメントは単純な命令形言語に期待されるもので、同期および仕様化に有用な非決定論的選択のプリミティブが追加されている。

代入は x := e と書く。PlusCal はまた配列の構成要素への代入 x[i,j] := e もサポートしており、その翻訳には TLA+ の EXCEPT 形式が使用される。PlusCal には式の値を表示する print e という文もある²。ただし TLC はデフォルトで幅優先状態列挙戦略 (breadth-first state enumeration strategy) を採用しているため、コンソールへの出力と実際の実行フロートの関係を理解することは必ずしも容易ではないかもしれない。

条件分は通常

if (exp) ... else ...

という形式をとり else の分岐は省略が可能である。同様に while ループは

while (exp) ...

と書く。

その他の制御フローを変更するステートメントはプロシジャコールや return (上記参照)、ラベル $l$ にジャンプする goto l などがある (PlusCal のラベルについては後述)。

アサーションは assert e 形式で PlusCal に埋め込むことができる。このステートメントは、述語 $e$ が true の場合は何の効果もなく、そうでない場合は中断する (TLC で反例トレース (counterexample trace) を生成する)。skip も存在する。これは何もせず assert TRUE と等価である。

assert e (when e と書くこともできる) というステートメントは、条件が true となるまで実行をブロックする。これは、例えばメッセージを実際に受信するまでメッセージの受信処理をブロックするなど、並列プロセスを同期させるときに有用である。

最後に、PlusCal には非決定性をモデル化するための 2 つのステートメントが存在する。一つ目の形式である

either \* 一つ目の選択肢
or     \* 二つ目の選択肢
or     \* ...

は固定数の選択肢の中からの選択を表現するのに有用である。この選択肢を制限する便利なイディオムは、分岐に await 文を追加することである。これにより条件が TRUE と評価された選択肢のみが実際に実行される (これはダイクストラの Guarded Command の PlusCal バージョンである)。

二つ目の形式

with (x \in S) ...

は集合 $S$ の要素に基づいた選択を可能にする。変数 $x$ は with 文の本体にスコープが限定されるローカル変数として機能する。例えば通信が必ずしも FIFO ではないモデルでは、 $S$ はプロセスが受信するメッセージの集合であり、with ステートメントはこれらのメッセージのいずれかを処理するために使用することができる。

2.7 セミコロン

C やそれと類似した言語とは異なり、PlusCal は (ステートメントの終わりではなく) ステートメントを区切るためにセミコロンを使用する。特に、これは複合ステートメントの閉じ中括弧の前にセミコロンが必要ないことを意味する (構文エラーとはみなされない)。ただし、閉じ括弧のあとに別のステートメントが続いている場合はセミコロンが必要である。

2.8 ラベル

PlusCal ステートメントにはラベルをつけることができる。ラベルの主な目的は並列プロセスの実行における "原子性の粒度" を示すことである。これは、2 つのラベルの間に配置されたステートメントのグループが他のプロセスによって中断されることなく実行されるという考え方である。ただし、PlusCal のトランスレータは特定のラベル付けルールを課している。最も重要なものは:

プロシジャ、プロセス、またはアルゴリズム本体の最初のステートメントにラベルを付ける必要がある。
while ステートメントにラベルを付ける必要がある。
callc, return または if に続くステートメント、またはラベル付きステートメントを含む verb - either - ステートメントにはラベルを付ける必要がある。
マクロ本体と with ステートメントの本体にはラベルを含めることができない。
同じ変数 (同じ配列の 2 つの要素を含む) へ 2 回の代入はラベルで区切らなければならない。

ラベル付けルールの詳細は Pluscal マニュアルに記載されている。トランスレータは不足しているラベルに関する情報を表示するし、また -label オプション付きで実行すると自動的に不足しているラベルを追加する。

2.9 Fairness の指定

fairness (公平性) 条件は、最終的に "十分な頻度で" 有効化されたステートメントが実行されなければならないことを要求している。これはアルゴリズムが任意の liveness 特性を満たすことを保証するために必要である。PlusCal では、fairness 条件はアルゴリズム、プロセステンプレート、またはラベルに付加することができる。fair algorithm と記述することにより、あるステートメントが有効化されたとき、最終的に (あるプロセスの) あるステートメントが実行されなければならないことを要求する。これは弱い条件である。特に、あるプロセスが常に有効化されていても、他のプロセスも常に有効化されていればまったく実行されない可能性がある。fair process と記述すると、プロセス (より正確にはプロセステンプレートの各インスタンス) が有効化されたままであれば最終的に実行されることが保証される。さらに強い条件である fair+ process ではプロセスに強い公平性が要求される。つまり、無限に繰り返し有効化されているのであれば、たとえ無限に繰り替えしむ効果されていたとしても、最終的には実行される。例えば無限に開放されるセマフォを必要とするプロセスは、競合するプロセスが存在していたとしても、強い公平性の下では最終的にセマフォを獲得することになる。

プロセスに付与された全体的な公平性要件は、個々のアクション (ラベルを付けて導入されたステートメントのグループに相当) に対して調整することができる。l: の代わりに l:- と書くことで、ラベル l で導入されるステートメントのグループに対する公平性仮定を抑止することができる。例えば相互排除アルゴリズムでは非クリティカルセクションに対する公平性の条件を仮定したくない場合がある。逆に l:+ と書くことでそのステートメントのグループに対して強い公平性を仮定する。例えば、弱い公平性のプロセスでセマフォを獲得する場合にのみ、強い公平性を要求することができる。

さらに詳細な公平性の条件を TLA+ で表現することも可能である。詳細は TLA+ に関する文献に記載されている。

¹これらの変数は $x=v$ という形式で初期化できるが、 $x \in S$ のような初期化はできない。
²このステートメントの利用は標準モジュール TLC を EXTEND する必要がある。

2 TLA⁺

PlusCal アルゴリズムは TLA+ 仕様言語に翻訳され、アルゴリズムの特性を検証するために TLA ツール (特に TLA ツールボックスと TLC モデルチェッカー) が死寄す荒れる。TLA+ は通常の数学的集合論に基づいており型付けされていない。PlusCal を効率的に使用するためには少なくともいくつかの TLA+ 構文を知る必要がある。

PlusCal アルゴリズムに現れるすべての式は TLA+ で記述されている。
検証される特性 (PlusCal コードに挿入されたアサーション以外) も TLA+ で記述される。

TLA+ には ASCII 構文があるが、標準の数学表記を使用してツールボックスから pretty-print できる。以下では ASCII ソースと同様に pretty-print バージョンを示す。

2.1 全体の構造

2.1.1 モジュールと宣言

TLA+ 仕様はモジュールで構成されている。TLA+ のモジュールは次のようなヘッダ行 (少なくとも4 つの '-' 記号) で始まり、

---------- MODULE Name ----------

そして最後は次のような行 (少なくとも 4 つの '=' 記号) で終わる。

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

モジュールは他のモジュールを EXTEND することでその内容を取り込むことができるが、これは基本的に拡張モジュールの内容を拡張しているモジュールにコピーすることと同じである。また、インスタンスを生成しようとしているモジュールの式によって (定数や変数の) パラメータをインスタンス化するように他のモジュールの INSTANCE を生成することもできる。これは、下位レベルの仕様が上位レベルの仕様を改良 (または実装) していることを示す場合などに便利である。

モジュールは通常、定数または変数パラメータを宣言する³。例えば

CONSTANTS Node, Edge
VARIABLES leader network

はグラフのノードとエッジを表す定数セットと、リーダー選出アルゴリズムで使用する 2 つの変数を宣言している (アルゴリズムが PlusCal で宣言されている場合、変数宣言は PlusCal トランスレータによって生成される。

TLA+ は型付けではないため、これらの宣言は定数または変数の型を示していない (意味的にはすべての TLA+ 値が設定される)。ただし、仕様には ${\rm ASSUME} \ {\it Edge} \subseteq {\it Node} \times {\it Node}$ のような定数パラメータに関する仮定が含むことができ、これらの仮定は TLC でチェックされる。変数の特性は不変性 (invariant) や時相論理特性などの式を用いて表現される。

2.1.2 演算子定義

TLA+ モジュールの大部分は演算子の定義で構成されている。演算子はデータに対する有用な操作や、アルゴリズムの初期条件や取りうる遷移など、仕様全体の部分式を表している。繰り返しになるが、PlusCal を使用する場合はほとんどの定義が PlusCal トランスレータによって生成される。ただし、PlusCal アルゴリズムは TLA+ モジュール (あるいは何らかの拡張モジュール) で定義された演算子を使用することができ、PlusCal アルゴリズムの correctness 特性は通常、生成された TLA+ 翻訳の下で TLA+ モジュールの部分で示される。

演算子の定義⁴は ${\it op}(p_1,\ldots,p_n) \ldef e$ の形式を取る。ここで $p_1,\ldots,p_n$ はこの定義のパラメータであり、 $e$ は定義の本体であり ${\it op}$ を含まない TLA+ 式で表される。各パラメータ $p_i$ は識別子または $f(\_,\ldots,\_)$ 形式ののどちらかである。後者は演算子のパラメータを示し、アンダースコアの数は演算子のアリティ、つまり演算子が期待する引数の数を示している。例えば ${\it Apply}(f(\_), x) \ldef f(x)$ は単項演算子のパラメータ $f$ と通常のパラメータ $x$ を取る。

TLA+ では現在のコンテキストで既に存在する名前は再利用できないという一般的なルールが適用される。したがって、上記の ${\it Apply}$ の定義は、 $f$ や $x$ が既に定数や変数パラメータとして、あるいは演算子名として導入されいているコンテキストでは違反となる。しかし、パラメータ記号の範囲はそれが現れた定義に限定されているため、後続の定義ではパラメータ名に $x$ を再利用することは許される。

2.1.3 再帰演算子

関数定義の特殊なケースとして、すべての $x \in S$ を ( $x$ を含んでいるだろう) 式 $e$ に変換する定義域 $S$ を持つ関数を定義するために $f[x \in S] \ldef e$ と書くことができる。この場合、 $e$ は $x$ を含んでいるかもしれない。例えば自然数上の階乗を定義するために ${\it frac}[n \in {\it Nat}] \ldef {\rm IF} \ n=0 \ {\rm THEN} \ 1 \ {\rm ELSE} \ n*{\it frac}[n-1]$ と書くことができる。TLA+ では再帰的な演算子を定義することもできる。この場合、再帰的な演算子の名前とアリティは定義の前に宣言する必要がある。 $\begin{array}{l} & {\rm RECURSIVE} \ {\it Fact}(\_) \\ & {\it Fact}(n) \ldef {\rm IF} \ n=0 \ {\rm THEN} \ 1 \ {\rm ELSE} \ n * {\it Fact}(n-1) \end{array}$ これは再帰的な (関数ではなく) 演算子を定義している; 特に ${\it Fact}$ は定義域を持たないことに注意。相互再帰演算子はその定義の前にすべての演算子名とアリティを宣言することで導入することができる。

2.1.4 定理

最後に、TLA+ モジュールは定理を保証しその証明を含むことができる。証明は TLA+ の対話型証明支援システムである TLAPS (TLA Proof System) によってチェックされる。その代わり、モデル検査で検証されるべき性質は TLA+ ツールボックスの TLC ペインに入力する必要がある。このためここでは定理や証明の構文については説明しない。

2.2 論理

$\land$ , $\lor$ , $\Rightarrow$ , $\equiv$ , $\lnot$ 　/\, \/, =>, <=>, ~: これらは命題論理 (論理積、論理和、含意、等価、否定) の標準演算子である。
$=$ , $\ne$ 　 =, #: 等号と不等号を示す (後者は ~= と書くこともできる)。
${\rm TRUE}$ , ${\rm FALSE}$ 　 TRUE, FALSE: 論理定数の真 (true) と偽 (false)。
$\forall x:P(x)$ , $\exists x:P(x)$ 　 \A x : P(x), \E x : P(x): 論理数量詞 "forall" と "exists" を表す。現在のスコープで既に使用されている変数を再利用することはできない。言い換えると、 $x$ が (現在の演算子定義の定数、変数、演算子またはパラメータとして) すでに導入されている場合 $\forall x:P(x)$ と書くことは違反だが、ある新しい変数 $y$ に対して $\forall y:P(y)$ と書かなければならない。集合 $S$ に制限され $[\forall|\exists]x \in S:P(x)$ と書かれる数量詞の "有限バージョン" が存在するこれらは TLC が評価できる唯一の形式である。
${\rm CHOOSE} \ x:P(x)$ 　 CHOOSE x : P(x): $P(x)$ が true となる、任意だが固定された値 $x$ を示すか、それ以外の場合はある未特定の固定値を示す。繰り返しになるが、取りうる値の選択をある集合 $S$ に制限する有限バージョンがあり、これが TLC で受け入れられる唯一の形式である。数学用語ではこの演算子は "ヒルベルトの $\epsilon$ 演算子" として知られている。これは決定的な選択を表していることを理解することが重要で、式を複数回評価しても同じ結果が得られる。CHOOSE 式が最も有用なのは述語を満たす一意の値が存在する場合である。例えばシーケンス $s$ の長さは ${\rm CHOOSE} \ n \in {\it Nat}: {\rm DOMAIN} \ s = 1..n$ と定義することができる。もう一つの有用なパラダイムはある集合 $S$ を "null 値" で拡張することである⁵: ${\it notAn}S \ldef {\rm CHOOSE} \ x:x \not\in S$ 集合 $S \cup \{{\it notAn}S\}$ は関数型プログラミングのオプション型に似ている。

2.3 集合

$\{e_1,\ldots,e_n\}$ 　 {e1, ..., en}: 式 $e_1,\ldots,e_n$ (に対応する値) を含む集合を示す。特に $\{\}$ は空集合である。
$x \in S$ , $x \not\in S$ , $S \subseteq T$ 　 x \in S, x \notin S, S \subseteq T: それぞれ $x$ が集合 $S$ の要素である場合、または要素でない場合、 $S$ が $T$ の部分集合である場合に true である。
$\cup$ , $\cap$ , $\backslash$ 　 \cup (または \union), \cap (または \inter), \: 和集合、共通部分、および差を表す。
${\rm UNION} \ S$ 　 UNION S: 一般化された和集合: $S$ は集合の集合であることが期待され、結果はそれらの集合の和集合となる。例えば ${\rm UNION} \ \{\{1,2\},\{3,4\}\} = \{1,2,3,4\}$ であり、より一般的には ${\rm UNION} \ \{A,B\}=A \cup B$ である。
${\rm SUBSET} \ S$ 　 SUBSET S: $S$ のすべての部分集合の集合を示す。例えば ${\rm SUBSET} \ \{1,2\} = \{\{\}, \{1\}, \{2\}, \{1,2\}\}$
$\{x \in S: P(x)\}$ 　 {x \in S : P(x)}: 述語 $P(x)$ が true となる $S$ の要素による部分集合を表す。例えば自然数 $n$ に対して $n$ が素数のときに ${\it isPrime}(n)$ が true となると仮定すると、 $\{n \in 1..100: {\it isPrime}(n)\}$ は 1 から 100 までの区間の素数の集合となる。
$\{e(x):x \in S\}$ 　 {e(x) : x \in S}: 演算子 $e$ を $S$ のすべての要素に適用することによって得られる値の集合を示す。この構成は関数型プログラミングのマップ演算子に似ている。例えば $\{2*n+1:n \in 0..99\}$ は自然数の中の最初の 100 個の奇数の集合を示す。
${\it Cardinality}(S)$ 　 Cardinality(S): 有限集合 $S$ の要素数。この演算子はモジュール FiniteSets で定義されていて使用するには EXTENDS する必要がある。このモジュールでは集合が有限であるかをチェックするための述語 ${\it isFiniteSet}$ も定義している。

2.4 関数

TLA+ の関数はその定義域上のすべてである。すべての関数は (ちょうど TLA+ の値のように) 集合だが、関数がどのような集合を示しているかは分からないため、関数の値をプリミティブなクラスとして考える (オタク向け: 集合論の多くの表現では関数はペアの集合であるがこれは TLA+ では強制されない)。プログラミング用語の観点では関数は配列に類似しているが、そのインデックス集合や定義域が有限である必要はない。TLA+ では関数に配列構文を使用している。

$[x \in S \mapsto e(x)]$ 　 [x \in S |-> e(x)]: $S$ のすべての要素 $x$ を $e(x)$ に写像する、定義域 $S$ を持つ関数を示す。例えば $[n \in {\it Nat} \mapsto n+1]$ は自然数上の successor 関数である。この表現は関数型プログラミングの $\lambda$ 式に似ている。
${\rm DOMAIN} \ f$ 　 DOMAIN f: 関数 $f$ の定義域を示す。TLA+ には関数 $f$ の値域に対する標準表記はないが、 $\{f[x] : x \in {\rm DOMAIN} \ f\}$ として簡単に定義できる。
$f[x]$ 　 f[x]: 引数 $x$ に関数 $f$ を適用した結果を示す。この式は $x \in {\rm DOMAIN} \ f$ の場合にのみ意味を持つ。
$[f \ {\rm EXPECT} \ ![x] = e]$ 　 [f EXPECT ![x] = e]: $f$ と同じ定義域を持ち、引数 $x$ を $e$ に写すことを除いて $f$ と同じ働きをする関数を表す。例えば ${\it succ}$ を前述の successor 関数とすると、 $[{\it succ} \ {\rm EXPECT} \ ![0] = 42]$ はすべての自然数を一つ後ろに写すが 0 は 42 に写す関数となる。 $e$ という関数の中では $f[x]$ を参照するために記号 @ を使うことができる。例えば $[{\it count} \ {\rm EXPECT} \ ![p] = @ + 1]$ は ${\it count}[p]$ を 1 増やすように関数 ${\it count}$ を更新する。いくつかの引数で関数を更新することは $[f \ {\rm EXCEPT} \ ![x] = a, ![y] = b, ![z] = c]$ のように書くことができる。
$[S \to T]$ 　 S -> T: 定義域が $S$ であり、すべての $x \in S$ に対して $f[x] \in T$ が成り立つようなすべての関数の集合を表す。
$[r \ {\rm EXCEPT} \ !.{\it fld} = e]$ 　 [r EXCEPT !.fld = e]: フィールド ${\it fld}$ が値 $e$ を保持することを除いて $r$ と同じレコードを表す (示しているフィールドはレコード $r$ に存在する必要がある)。関数の ${\rm EXCEPT}$ 構文に類似した一般化により複数のレコードフィールドを更新することができる。

TLA+ は複数の引数を取る関数に対して $f[x,y]$ が $f[\langle x,y\rangle]$ の省略形であり、したがって $f \in [X \times Y \to Z]$ であるという規則を採用している。この規則は ${\rm EXCEPT}$ 式にも適用され $[f \ {\rm EXCEPT} \ ![x,y]=e]$ と書くことができる。

2.5 レコード

TLA+ レコードは有限集合のフィールド (文字列として表される) から値への関数である。そのため、原則的にレコードに対して標準の関数操作を適用することができる。しかし TLA+ ではレコードのための特別な構文を導入している。

$[{\it fld}_1 \mapsto e_1, \ldots, {\it fld}_n \mapsto e_n]$ 　 [fld1 |-> e1, ..., fldn |-> en]: 値 $e_i$ を保持するフィールド ${\it fld}_i$ を持つレコードを構築する。例えば $[{\it kind} \mapsto {\tt "request"},\ {\it sndr} \mapsto p, {\it clk} \mapsto 42]$ はプロセス $p$ によって送信された論理クロック値 42 を持つリクエストメッセージを表すことができる。
$r.{\it fld}$ 　 r.fld: レコード $r$ からフィールド ${\it fld}$ の値を選択する。

2.6 数値

算術演算子は、標準モジュール Naturals または Integers のどちらかを EXTENDS してインポートする必要がある (TLA+ には実数用の標準モジュール Reals もあるがこれは必要ない)。

${\it Nat}$ , ${\it Int}$ 　 Nat, Int: 自然数 $(0, 1, \ldots)$ と整数の集合を表す。
$i..j$ 　 i..j: -3..5 のような整数の区間。
$+$ , $-$ , $*$ , $\div$ , ${\it mod}$ 　 +, -, *, \div, %: 標準的な算術演算子 (加算、減算、乗算、除算と余剰)。

2.7 タプルとシーケンス

タプルとシーケンスは共に数学的オブジェクトだが使用方法が異なる。タプルは固定数の構成要素を持つが、シーケンスは様々な長さを持つことができる。TLA+ では、タプルとシーケンスはある自然数 $n$ に対して定義域 $1..n$ を持つ関数として表現される (特に、空のシーケンスは $1..0$ を持つ)。したがって標準関数操作が適用され、シーケンス $s$ の $i$ 番目の要素は $s[i]$ として得られる。シーケンス操作は標準モジュール Sequences を EXTENDS してインポートする必要がある。

$\langle e_1,\ldots,e_n\rangle$ 　 <<e1, ..., en>>: 要素 $e_1,\ldots,e_n$ をこの順序で持つシーケンスを表す。特に << >> は空のシーケンスである。
$s \circ t$ 　 s \o t: シーケンス $s$ と $t$ の連結を表す。例えば $\langle 1,2\rangle \circ \langle 3,4\rangle = \langle 1,2,3,4\rangle$ となる。
${\it Seq}(S)$ 　 Seq(S): 集合 $S$ の要素を持つ全ての有限シーケンスの集合。
$S \times T$ 　 S \X t: $S$ と $T$ の集合積、つまり $s \in S$ と $t \in T$ のすべてのペア $\langle s,t\rangle$ を表す。
${\it Len}(s)$ 　 Len(s): シーケンス $s$ の長さを表す。
${\it Append}(s,e)$ 　 Append(s,e): シーケンス $s$ の末尾に要素 $e$ を追加する。
${\it Head}(s)$ , ${\it Tail}(s)$ 　 Head(s), Tail(s): それぞれシーケンス $s$ の先頭の要素と、先頭の要素が削除された残りの要素を示す。これらの演算子はシーケンス $s$ が空でない場合にのみ明確に定義される。
${\it SubSeq}(s,m,n)$ 　 SubSeq(s,m,n): シーケンス $\langle s[m],s[m+1],\ldots,s[n]\rangle$
${\it SelectSeq}(s,P(\_))$ 　 SelectSeq(s, P(_)): 述語 $P$ を満たすシーケンス $s$ の要素のサブシーケンスを表す。例えば $n$ が素数のときに ${\it isPrime}(n)$ が true となる場合 ${\it SelectSeq}(\langle 2,3,4,5,6,7,8\rangle,{\it isPrime}) = \langle 2,3,5,7\rangle$

TLA+ では他にもシーケンスに対する多くの演算子を簡単に定義できる。例えばシーケンスに対する "map" 演算は ${\it Map}(s,f(\_)) \ldef [i \in {\rm DOMAIN} \ s \mapsto f(s[i])]$ その他の演算では、例えば "null 値" $e$ から始まりシーケンス $s$ のすべての要素に ${\it op}$ を適用する "reduce" 操作のように、再帰的な定義を必要とする。 $\begin{array}{l} & {\rm RECURSIVE} \ {\it Reduce}(\_,\_,\_) \\ & {\it Reduce}(s, {\it op}(\_,\_),e) \ldef {\rm IF} \ s=\langle\rangle \ {\rm THEN} \ e \\ & \ \ \ \ {\rm ELSE} \ {\it op}({\it Head}(s), {\it Reduce}({\it Tail}(s), {\it op}, e)) \end{array}$

文字列は文字のシーケンスとして表現される。文字がどのように表現されるかは規定されておらず、リテラル文字列は "string" と表記される。しかし TLC では文字列をネイティブに扱うため、文字列に適用されるシーケンス演算子は対応していない。

2.8 様々な構造

${\rm IF} \ P \ {\rm THEN} \ t \ {\rm ELSE} \ e$ 　 IF P THEN t ELSE e: 条件式。 $t$ と $e$ が共に式である場合は式として使用できるが、より一般的には項としても使用できる。例として前述の階乗関数の定義を参照。
${\rm CASE} \ p_1 \to e_1 □ p_2 \to e_2 \ldots □ {\rm OTHER} \ \to e$ 　 CASE p1 -> e1 [] p2 -> e2 ... [] OTHER -> e: 条件式を 2 つ以上の分岐に一般化する。これは $p_i$ が true であるような $e_i$ と等しく、ガード $p_i$ のどれも true でない場合は $e$ となる ( ${\rm OTHER}$ 分岐はオプション)。複数の $p_i$ が true の場合は、どの分岐が評価されるかは固定されているが指定されていない:　この場合、対応するすべての $e_i$ が同じ値で評価されることを保証せよ。
${\rm LET} \ x \ldef t \ {\rm IN} \ e$ 　 LET x == t IN e: 関数型プログラミング言語の "let" 構造と同様に、ユーザがローカル定義を導入できるようにする。

³定数パラメータの値はアルゴリズムの実行中にずっと固定されたままである。TLA+ 変数はプログラム変数に類似しており、異なる実行状態で異なる値を想定している。
⁴記号 $\ldef$ は ASCII で == と書く。
⁵賢明な読者はこのフォームが TLC で評価できないことに気づくだろう。ただし TLC Toolbox は ${\it notAn}S$ の代わりに特別な "モデル値" を使用する。

3 オンラインリファレンス

learntla.com: 新規参入者が PlusCal と TLA+ を学ぶ手助けとなる Web サイト。同じ著者によるより完全な紹介付きの出版本 ("Practical TLA+") もある。
http://lamport.azurewebsites.net/tla/tla.html: 多くの参照素材のあるオフィシャル TLA+ ウェブサイト。
http://lamport.azurewebsites.net/video/videos.html: Leslie Lamport による TLA+ のビデオコース (ただ PlusCal はカバーしていない)。
http://lamport.azurewebsites.net/tla/c-manual.pdf: 講義でも使用されている C 構文の PlusCal マニュアル。

翻訳抄

PlusCal と TLA+ のリファレンスとして有用なチートシート。

S.Merz (2019) PlusCal / TLA⁺: An Annotated Cheat Sheet

翻訳: PlusCal/TLA+: An Annotated Cheat Sheet