TL;DR
- TLA+ の仕様は
MODULEで始まるモジュールとして書き、PlusCal のアルゴリズムはその中のコメントに書く。 - 基本的な値は文字列、整数、ブール値、モデル値の 4 種類で、型は集合、タプル（シーケンス）、構造体、関数の 4 種類である。
内容
モジュール
TLA+ の仕様は、左右を 4 つ以上のハイフンで囲んだ MODULE の行で始め、4 つ以上の等号の行で終える。MODULE の後には、ファイル名と同じモジュール名を書く。ほかのモジュールを取り込むには EXTENDS を使う。1 行コメントは \*、ブロックコメントは (* ... *) で書く。式はすべて、TRUE のような値か、+ のような演算子のどちらかである。
---- MODULE wire ----
EXTENDS Integers
...
====PlusCal のアルゴリズム
PlusCal は、TLA+ のパーサに無視されるようにコメントの中に書く。具体的には --algorithm <アルゴリズム名> から end algorithm までに書く。アルゴリズム名もモジュール名と同じくファイル名にする。アルゴリズムの中では variables で変数を初期化する。変数は , か ; で区切る。
(*--algorithm wire
variables
people = {"alice", "bob"},
acc = [p \in people |-> 5];
...
end algorithm;*)値と演算子
TLA+ の基本的な値は、文字列、整数、ブール値、モデル値の 4 種類である。論理演算子は次のとおりである。
| 意味 | 書き方 |
|---|---|
| 等しい | x = y |
| 等しくない | x /= y または x # y |
| 論理積（AND） | x /\ y |
| 論理和（OR） | x \/ y |
| 否定（NOT） | ~x |
| 代入（PlusCal） | x := y |
Integers モジュールを取り込むと、+、-、*、% などの算術演算と、範囲演算子 .. が使える。除算は \div で、小数の演算はできない。
集合
TLA+ の型は、集合、タプル（シーケンス）、構造体、関数の 4 種類である。集合は {"a", "b", "c"} のように書き、次の演算子が使える。
| 書き方 | 意味 |
|---|---|
x \in set | x が set に含まれるか |
x \notin set | x が set に含まれないか |
set1 \subseteq set2 | set1 が set2 の部分集合か |
set1 \union set2 | 和集合（\cup でもよい） |
set1 \intersect set2 | 積集合（\cap でもよい） |
set1 \ set2 | 差集合 |
Cardinality(set) | 要素の個数（FiniteSets モジュールが必要） |
集合を絞り込むには {x \in set: <条件式>}、各要素を変換するには {<式>: x \in set} と書く。タプルは <<"a", {1, 2}>> のように書く。