翻訳: A PlusCal User's Manual

• ^*このマニュアルには C-Syntax 版もある。２つの構文の詳細については 3 ページ参照。

Table of Contents

1. Preface
2. 2 つの構文
3. 1 Introduction
4. 2 Getting Started
   1. 2.1 Typing the Algorithm
   2. 2.2 The TLA+ Module
   3. 2.3 Translating and Executing the Algorithm
   4. 2.4 Checking the Results
   5. 2.5 停止の確認
   6. 2.6 A Multiprocess Algorithm
   7. 2.7 Where Labels Must and Can't Go
5. 3 The Language
   1. 3.1 Expressions
   2. 3.2 The Statements
      1. 3.2.1 Assignment
      2. 3.2.2 If
      3. 3.2.3 Either
      4. 3.2.4 While
      5. 3.2.5 Await (When)
      6. 3.2.6 With
      7. 3.2.7 Skip
      8. 3.2.8 Print
      9. 3.2.9 Assert
      10. 3.2.10 Call と Return
      11. 3.2.11 Goto
   3. 3.3 プロセス
   4. 3.4 プロシジャ
   5. 3.5 マクロ
   6. 3.6 定義
   7. 3.7 Labels
   8. 3.8 The Translation's Definitions and Declarations
6. 4 Checking and Algorithm
   1. 4.1 Running the Translator
   2. 4.2 Specifying the Constants
   3. 4.3 Constants
   4. 4.4 Understanding TLC's Output
   5. 4.5 不変性チェック
   6. 4.6 終了, Liveness, 公平性
   7. 4.7 Additional TLC Features
      1. 4.7.1 Deadlock Checking
      2. 4.7.2 Multithreading
      3. 4.7.3 Symmetry
7. 5 TLA+ Expressions and Definitions
   1. 5.1 Numbers
   2. 5.2 Strings
   3. 5.3 Boolean Operators
   4. 5.4 Sets
   5. 5.5 Functions
   6. 5.6 Records
   7. 5.7 The Except Construct
   8. 5.8 Tuples and Sequences
   9. 5.9 Miscellaneous Constructs
   10. 5.10 Temporal Operators
       1. 5.10.1 Fairness
       2. 5.10.2 Liveness
       3. 5.10.3 One Algorithm Implementing Another
   11. TLA+ Definitions
8. References
9. A The Grammar
10. B The TLA+ Translation
11. C Translator Options
12. Useful Tables
13. Index
14. 翻訳抄

Preface

2 つの構文

PlusCal には p-構文と c-構文の 2 つの構文がある。以下は 2 つの構文で書かれたコードのスニペットである:

while x > 0 do
  if y > 0 then y := y-1;
                x := x-1;
           else x := x-2
  end if
end while;
print y;

while (x > 0)
  { if (y > 0) { y := y-1;
                 x := x-1 }
    else x := x-2  } ;
print y;

p-構文は語数が多いためコードの意味がより明確に形、また "\(\}\)" の代わりに明確な \({\tt end}\) を使用するため構文エラーを発見しやすくなる。しかし c-構文バージョンはより短く賢明な書式設定によってコードの意味は十分に明確である。C++, C#, Java など、C 言語から派生した限度でのプログラミングに慣れている場合は c-構文バージョンの方が良いかも知れない。

このマニュアルでは p-構文バージョンについて説明する。c-構文バージョンのマニュアルは TLA+ ツールの Web サイトから入手できる。

1 Introduction

2 Getting Started

2.1 Typing the Algorithm

2.2 The TLA+ Module

2.3 Translating and Executing the Algorithm

2.4 Checking the Results

2.5 停止の確認

アルゴリズム EuclidAlg が常に停止 (終了) することを確認するには -termination オプションを付けて変換を実行する。またはファイルのコメントまたはモジュールの前後に

PlusCal options (-termination)

の行を配置することでも行える (options ステートメントに入れるときはオプション名から "-" を省略できる)。これにより停止を保証する適切な変換が生成される。次に新しいモデルを生成すると Model Overview ページの What to check? セクションの Properties 部分に Termination が追加されるだろう。これにより TLC は取りうるすべての実行が停止することを確認する (Termination プロパティはすべての PlusCal アルゴリズムのツールボックスに含まれているが、そのボックスはモデル作成時にルートモジュールに Termination プロパティが指定されている場合にのみ確認される)。

TLC が非停止実行 (non-terminating execution) を検出すると、プロパティ Termination に違反していることを示すエラーメッセージが生成され、ツールボックスのエラートレースウィンドウに非停止のトレースが表示される。36 ページのセクション 4.4 ではこのトレースの解釈方法について説明している。

2.6 A Multiprocess Algorithm

2.7 Where Labels Must and Can't Go

3 The Language

3.1 Expressions

3.2 The Statements

3.2.1 Assignment

3.2.2 If

3.2.3 Either

3.2.4 While

3.2.5 Await (When)

\({\tt await} \ expr\) ステートメントを含むステップは、Boolean 式 \(expr\) の値が \({\tt TRUE}\) のときにのみ実行できる。通常 \({\tt await}\) はステップの先頭に記述されるが、ステップ内のどこに記述してもかまわない。例えば次の 2 つのコードは等価である。

\({\tt a}\) から \({\tt b}\) へのステップは \({\tt y+1}\) の現在の値が正の場合にのみ実行できる。(ステップは全体が一度に実行されなければならないことに注意; ステップの一部を単独で実行することはできない。) \({\tt await}\) の代わりに \({\tt when}\) を使うこともできる。

3.2.6 With

\({\tt with} \ id \in S \ {\tt do} \ body \ {\tt end \ with};\) ステートメントは非決定論的に選択された \(S\) の要素に等しい識別子 \(id\) を持つステートメント列 \(body\) を実行することによって実行される。(シンボル \(\in\) は "\({\tt \backslash in}\)" でタイプされる。) \(S\) が空集合であれば実行不可能である。したがってこの \({\tt with}\) ステートメントは以下と等しい \[ {\tt await} \ S \ne {\tt \{\}}; \ {\tt with} \ id \in S \ {\tt do} \ body \ {\tt end \ with}; \] 以下の 2 つのステートメントは等価である。(式 \({\tt \{} expr {\tt \}}\) は \(expr\) に等しい要素を 1 つ含む集合に等しい。)

一般に \({\tt with}\) ステートメントは次の形式となる。\[ {\tt with} \ id_1 \star expr_1 \ ; \ \ldots \ ; \ id_n \star expr_n \ {\tt do} \ body \ {\tt end \ with}; \] ここで \(\star\) は \(=\) か \(\in\) のいずれかである。(\(id_i \star expr_i\) の項目間にはセミコロンの代わりにコンマを使っても良い。) このステートメントは次と等価である。\[ {\tt with} \ id_1 \star expr_1 \ {\tt do} \ \ldots \ {\tt with} \ id_n \star expr_n \\ {\tt do} \ body \ {\tt end \ with} \ \ldots \ {\tt end with}; \] \({\tt with}\) の本体にはラベルを含んではならない。この規則と 30 ページのセクション 3.7 でのラベルが必要な場合の規則をあわせると、\({\tt with}\) 文の本体には次のような者を記述してはならない。

• \({\tt while}\) ステートメント。

• 同じ変数に値を代入する 2 つの別々の代入文。(単一の多重代入は同じ変数の異なる構成要素に値を代入することができる。)

• \({\tt return}\) に続くステートメント、または \({\tt call}\) に続く \({\tt return}\) 以外のステートメント。

3.2.7 Skip

\({\tt skip;}\) ステートメントは何も行わない。

3.2.8 Print

\({\tt print} \ expr{\tt ;}\) ステートメントは \({\tt skip}\) と等価だが、\(expr\) の現在の値を TLC に表示させる。

3.2.9 Assert

\({\tt assert} \ expr{\tt ;}\) ステートメントは式 \(expr\) が TRUE と等しい場合は \({\tt skip}\) と等価である。もし \(expr\) が偽に等しい場合、この文を実行すると TLC はアサーションに失敗したというエラーメッセージおよび \({\tt assert}\) ステートメントの場所を表示する。ステップの後にある \({\tt await}\) ステートメントにより、\({\tt assert}\) ステートメントを含むステップが実行されなくとも TLC がアサーションの失敗を報告する場合がある。

\({\tt assert}\) ステートメントを含むアルゴリズムは \(TLC\) モジュールを \({\tt extends}\) したモジュール内になければならない。

3.2.10 Call と Return

\({\tt call}\) と \({\tt return}\) ステートメントは 26 ページのセクション 3.4 で説明する。

3.2.11 Goto

\({\tt goto} \ lab {\tt ;}\) ステートメントの実行は現在のステップの実行を終了し \(lab\) とラベル付けされたステートメントに制御が移る。どのような制御経路においても \({\tt goto}\) の直後にはラベルを指定しなければならない。(定義による制御経路では \({\tt goto}\) の意味は無視され、構文的には次の文に進む。)

\({\tt goto}\) が \({\tt while}\) や \({\tt if}\) の中にジャンプすることは合法だが、そのようなトリックは避けるべきである。

3.3 プロセス

マルチプロセスアルゴリズムは 1 つ以上のプロセスを含んでいる。プロセスは 2 つの方法のいずれかで開始する:

\({\tt process} \ ProcName \in IdSet\)
\({\tt process} \ ProcName = Id\)

最初の形式はプロセス集合を開始し、2 つ目はプロセスを個別に開始する。識別子 \(ProcName\) はプロセスまたはプロセス集合の名前である。要素 \(Id\) と集合 \(IdSet\) の要素はプロセス識別子と呼ばれる。同じアルゴリズム内の異なるプロセスのプロセス識別子はすべて異なっていなければならない。これは TLA+ のセマンティクスでそれらが異なっている必要があることを暗示していることを意味し、直感的には、通常それらが同じ "型" でなければならないことを意味する (例えば TLA+ のセマンティクスは文字列と数値が等しいかどうかを特定しない)。TLC にる実行の場合、これは TLA+ ブック [3] の 264 ページで定義されているように、すべてのプロセス識別子が比較可能な値でなければならないことを意味する。

\(ProcName\) という名前に意味はなく、これを変更しても \({\tt process}\) 文の意味は何ら変わることはない。この名前は TLA+ 翻訳後の文に現れ、異なるプロセス文に対しては異なるべきである。

上記ページ 12 のセクション 2.6 で説明したように \({\tt process}\) ステートメントの後には任意でローカル変数の宣言が続く。プロセス本体は "\({\tt begin}\)" で始まり "\({\tt end \ process}\)" で終わる。最初のステートメントにはラベルを付けなければならない。プロセス集合の本体内での \({\tt self}\) は現在のプロセスの識別子に等しい。

マルチプロセスアルゴリズムは、任意のプロセスの選択を繰り返し、そのステップの実行が可能であればそのプロセスの 1 ステップを実行することによって進行する。プロセスが終了しており、次のステップに条件式が偽となる \({\tt await}\) ステートメントが含まれている場合、またはそのステップに "\({\tt await} \in S\)" という形式のステートメントが含まれていて \(S\) が空集合に等しい場合、そのプロセスの次のステップは実行不可能である。12 ページのセクション 2.6 で説明したように、どのプロセスのステップを実行するかについては公平性条件を指定することができる。

3.4 プロシジャ

アルゴリズムは 1 つ以上のプロシジャを持つことがある。その場合、アルゴリズムは \(Sequences\) モジュールを \({\tt extends}\) した TLA+ モジュール内になければならない。

アルゴリズムのプロシジャは、グローバル変数宣言と (必要であれば) \({\tt define}\) セクションに続いて、単一プロセスアルゴリズムの \({\tt begin}\) またはマルチプロセスアルゴリズムの最初のプロセスの前に配置する。\(PName\) という名前のプロシジャは次のように開始する \[ {\tt procedure} \ PName {\tt (}param_1,\ldots,param_n {\tt )} \] ここで識別子 \(param_i\) はプロシジャの形式パラメータ (formal parameters) である。これらのパラメータは変数として扱われ、代入することができる。37 ページのセクション 4.5 で説明されているように、パラメータに初期値を割り当てることもできる。

\({\tt procedure}\) ステートメントの後には、オプションでプロシジャのローカル変数宣言が続く。これらはグローバル変数の宣言と同じ形式を持つが、初期化は "\(variable = expression\)" 形式しか持たない。プロシジャのローカル変数はプロシジャに入るたびに初期化される。

任意の変数宣言の後にはプロシジャの本体が続く。これは "\({\tt begin}\)" で始まり \({\tt end \ procedure}\)" で終わる。プロシジャの本体はラベル付きのステートメントで開始しなければならない。本体の後には暗黙のラベル \({\tt Error}\) がある。もし制御がこのポイントに到達した場合、プロセス (マルチプロセスアルゴリズム) または完全なアルゴリズム (単一プロセスアルゴリズム) の実行は停止する。

プロシジャ \(PName\) はステートメント \[ {\tt call} \ PName{\tt (}expr_1,\ldots,expr_n{\tt );} \] で呼び出すことができる。この呼び出しを実行すると、式 \(expr_i\) の現在の値が対応するパラメータ \(param_i\) に代入され、プロシジャのローカル変数が初期化され、プロシジャ本体の先頭に制御が置かれる。

\({\tt return}\) ステートメントはパラメータとプロシジャのローカル変数に以前の値、つまりプロシジャが最後に呼び出される前の値を代入し、制御を \({\tt call}\) ステートメントの直後のポイントに戻す。

\({\tt call}\) と \({\tt return}\) ステートメントは、プロシジャのパラメータとローカル変数への代入と見なされる。特に、1 つの変数に値を代入できるのは 1 つのステップ内で最大 1 つの代入文だけである、というルールに含まれている。例えば \(x\) をプロシジャ \(P\) のローカル変数としたとき、\(P\) の本体内で \(P\) を (再帰的に) 呼び出すステップでは \(x\) に値を代入することはできない。

マルチプロセスアルゴリズムにおいてプロシジャ本体の識別子 \({\tt self}\) は、そのプロシジャを実行しているプロセスのプロセス識別子に等しい。

\({\tt return}\) ステートメントは引数を持たない。PlusCal プロシジャは明示的に値を返さない。値を返すには、プロシジャでグローバル変数に設定し、呼び出し直後のコードでその変数を読み取る。例えばマルチプロセスアルゴリズムでは、プロシジャ \(P\) はグローバル変数 \({\tt rVal}\) を使用して次にように値を返すことができる

\({\tt rVal[self] :=} \ldots ;\)
\({\tt return};\)

プロセス集合内のプロセスから \(P\) を呼び出すコードは次のようになる: \[ {\tt call \ P(17); \ \ lab: \ x \ := \ ... \ rVal[self] \ ...;} \] 単一プロセスからの呼び出しの場合、コードには \({\tt self}\) の代わりにプロセスの識別子が含まれる。

どのような制御パスにおいても \({\tt return}\) ステートメントの直後にはラベルをつけなければならない。\({\tt call}\) ステートメントは、制御パスの中でラベルの後に続くか、あるいはステートメントの並びの中で \({\tt return}\) ステートメントの直前に現われなければならない。

\({\tt call}\ P\) ステートメントの直後に \({\tt return}\) ステートメントが続く場合、プロシジャ \(P\) からのリターンと \({\tt return}\) ステートメントによるリターンの両方が 1 つの実行ステップの一部として実行される。これらのステートメントが (再帰的な) プロシジャ \(P\) 内にある場合、この 2 つのリターンの組み合わせは、基本的に末尾再帰をループに置き換えるという標準的な最適化である。

3.5 マクロ

マクロはその呼び出しが翻訳時に展開されることを除けばプロシジャに似ている。マクロは、それが呼び出されたステップ内で実行されるプロシジャと見なすことができる。

マクロの宣言はプロシジャ宣言とよく似ている。例えば:

macro P(s, i) begin await s ≧ i;
                    s := s - 1;
end macro;

違いはマクロ本体にはラベルや \({\tt while}\), \({\tt call}\), \({\tt return}\) ステートメントが含まれないことである。マクロ本体には前方で宣言されたマクロの呼び出しを含むことができる。マクロの宣言はグローバル変数の宣言と \({\tt define}\) セクションの直後に配置される。

マクロ呼び出しは \({\tt call}\) が省略されている点を除けばプロシジャ呼び出しと同じである。例えば: \[ {\tt P(sem, y+17);} \] マクロ呼び出しの翻訳は、呼び出しの引数を宣言のパラメータに置き換えてマクロ宣言の本体から得られる一連のステートメントに置き換える。したがってこの \({\tt P}\) マクロの呼び出しは次のように展開される。

await sem ≧ (y + 17);
sem := sem - (y + 17);

マクロ呼び出しを翻訳するとき、置換は構文的なものであり、マクロ定義内のパラメータ以外の記号は呼び出しのコンテキストで持っている意味となる。例えばマクロ定義の本体にシンボル \({\tt q}\) が含まれており、そのマクロが "\({\tt with q \in \ldots}\) ステートメント内で呼び出されていた場合、マクロ展開の \({\tt q}\) は \({\tt with}\) ステートメントの束縛された \({\tt q}\) である。

マクロをその定義で置き換えるとき、翻訳はマクロ本体内の式のマクロパラメータ \(id\) のすべてのインスタンスを対応する式で置き換える。すべてのインスタンスには、次の式のように束縛変数としての \(id\) の使用も含まれる。\[ [ id \in 1 .. N \mapsto \mbox{FALSE} ] \] ここで \(id\) に \(y+17\) のような式を代入すると翻訳が解析されたときに謎のエラーが発生する。PlusCal を使用するときは TLA+ の慣習に従って既に意味を持つ識別子に新しい意味を割り当てないようにする。

3.6 定義

アルゴリズム式は "\({\tt BEGIN \ TRANSLATION}\)" 行の前にある TLA+ モジュールで定義された任意の演算子 (operator) を使用することができる。アルゴリズム変数の TLA+ 宣言はその行の後に続くことから、それらの演算子の定義はアルゴリズム変数から参照することはできない。PlusCal の \({\tt define}\) ステートメントではアルゴリズムのグローバル変数に依存する演算子となる TLA+ 宣言を書くことができる。例えばアルゴリズムが次のように開始しているとする:

(記号 "\(\overset{\Delta}{=}\)" は "\({\tt ==}\)" とタイプされる。) 演算子 \({\tt zy}\) と \({\tt zx}\) はアルゴリズムの残りのどの位置でも式として使用できる。2 つの表記の間にはセミコロンなどの区切り記号は必要ない。55 ページのセクション 5.11 では TLA+ 定義の書き方について説明している。

\({\tt define}\) ステートメントで使用できる変数は、その直前でアルゴリズム名に続く \({\tt variable}\) ステートメントで宣言された変数、\(pc\) 変数、プロシジャがある場合は \(stack\) 変数である。ローカルプロセス変数とプロシジャ変数は \({\tt define}\) ステートメントに書くことはできない。\({\tt define}\) ステートメントの定義はアルゴリズム変数を参照する必要はない。あなたは \({\tt define}\) ステートメントに記述する必要がなくても \({\tt define}\) ステートメントに記述することを好むかもしれない。しかし \({\tt define}\) ステートメントでは "\({\tt END \ TRANSLATION}\)" 行の後に定義または宣言されたシンボルを参照することはできない。そしてそれが定義するシンボルは "\({\tt BEGIN \ TRANSLATION}\)" 行より前に使用することはできない。

定義は、\({\tt define}\) ステートメントに含まれる者も含めて、PlusCal から TLA+ への翻訳では展開されない。定義された記号はすべて PlusCal コードに現われるのとまったく同じように翻訳に現われる。特にアルゴリズム本体で定義されたシンボルを評価する場合、たとえそのシンボルが変数への代入の後に現われたとしても、その定義に登場する変数が現在のステップの最初に持っている値を使用する。例えば変数 \({\tt x}\) が \({\tt sim}\) の定義の前に現われる場合、次の 2 つのコードスニペットは逐次アルゴリズムであっても異なる結果を生成することができる:

\({\tt x}\) の値が "\({\tt old}\)" のときに実行された場合、\({\tt sim}\) を評価すると最初のスニペットでは \({\tt x}\) の値には "\({\tt old}\)" が使われ、2 番目のスニペットでは "\({\tt new}\)" が使われるだろう。

3.7 Labels

3.8 The Translation's Definitions and Declarations

4 Checking and Algorithm

4.1 Running the Translator

4.2 Specifying the Constants

4.3 Constants

4.4 Understanding TLC's Output

4.5 不変性チェック

セクション 2 の例では TLC を使って数式の不変性をチェックする方法 - つまりアルゴリズムが到達可能なすべての状態で式が true となることを説明している。不変性の重要な例は型の正確さである。通常の型付きプログラミング言語では型の正確さは構文上の条件である。PlusCal は型がないため、型の正確さはアルゴリズムの特性であり、各変数の値が適切な集合の要素であることをアサートする。例えば我々は p の値が常に素数である場合に限り、つまり次の式が不変である場合に限り変数 p が素数型を持つという。ここで \({\it Nat}\) は自然数の集合である。\[ p \in \{i \in {\it Nat}:\forall j \in 2..(i-1): i\ \%\ j \ne 0\} \] (もしいまこの不変性を理解していなくても、セクション 5 を読めば理解できるはずである) TLC はこの式が不変性かどうかを調べることができる。通常のプログラミングの型チェックと同様に、型の正しさをチェックすることは PlusCal アルゴリズムの単純なエラーを発見するのに良い方法である。

アルゴリズムが型と一致しているためには、その変数の初期値が正しい "型" である必要がある。変数に初期値が設定されていない場合、そのデフォルトの初期値は defaultInitValue という名の不定型の定数である。デフォルトでツールボックスのモデルはこれをモデル値として設定する (35 ページ参照)。defaultInitValue が不定型であるため、これは変数に対する型一致値ではない。したがってアルゴリズムは変数が正しく初期化されないと型が正しくないことになる。型をチェックしたくなる変数の中にはプロシジャパラメータがある。アルゴリズムでは以下の例のようにプロシジャの形式パラメータに初期値を割り当てることができる:

procedure Foo (p1 = 0, p2 = {"a", "b"})

プロシジャ変数の宣言と同様に、形式パラメータ \(p\) の初期値宣言は \(p={\it expression}\) でなければならない。

プロシジャの形式パラメータはプロシジャが呼び出されたときに対応する引数と同じ値に設定されるため、その初期値は実行には影響を与えない。これらの初期値は TLA+ 仕様の対応する変数が常に正しい型の値を持つことを保証するためだけに使用される。

4.6 終了, Liveness, 公平性

セクション 2.5 では単一プロセスアルゴリズムの終了をチェックする方法を紹介した。終了は liveness 特性と呼ばれる一般的な特性の特殊ケースであり、最終的に何かが起こることを保証している。我々は TLC を使ってより一般的にアルゴリズムの liveness 特性をチェックすることができる。

アルゴリズムはいくつかの仮定 - 通常はアクションの公平性仮定 (fairness assumptions of action) - のもとでのみ liveness 特性を満たす。PlusCal アルゴリズムではラベルごとに対応するアクションが存在する。そのアクションの実行とは、そのラベルから次のラベルまでのすべてのコードの実行で構成される。アクションは実行可能である場合にのみ有効化 (enabled) される。プロセス内の以下のコードについて考える:

a: y := 42;
   z := y + 1;
b: await x > self;
   x := x-1;
c: ...

アクション \(a\) の実行は \(y\) と \(z\) への割り当てを実行することで構成されている。このアクションはプロセスの制御が \(a\) にある場合にのみ有効化される。アクション \(b\) の実行は \(x\) を 1 ずつ減少させる。これは制御が \(b\) にあり \(x\) の値がプロセスの識別子 \({\it self}\) より大きい場合にのみ有効化される。

制御がそのラベルにある場合にのみ有効化される \(a\) のようなアクションはノンブロッキングと呼ばれる。ノンブロッキングではない \(b\) のようなアクションはブロッキングと呼ばれる。

ノンブロッキングアクションに対する公平性は、プロセスがそのアクションで停止できないことを意味している。したがって \(a\) での公平性とは、プロセスの制御が \(a\) にあるときにプロセスは最終的にアクション \(a\) を実行しなければならないことを意味している。

ブロッキングアクションに対する公平性の条件には 2 種類がある。アクション \(\alpha\) の弱い公平性 (weak fairness) は、\(\alpha\) が永遠に有効化されているなら \(\alpha\) を停止できないことを意味している。例えばアクション \(b\) が弱い公平性であるとは、プロセスが \(b\) にある間 \(x \gt {\it self}\) が true のままである場合、アクション \(b\) が最終的に実行されることを意味している。\(\alpha\) の強い公平性 (strong fairness) とは、\(\alpha\) が永遠に true のままであればプロセスは \(\alpha\) で停止できないことに加えて、\(\alpha\) が無効化され続けその後に有効化されても停止できないことを意味する。例えばアクション \(b\) の強い公平性は、\(x \gt {\it self}\) が true になり続ける限り、たとえ false になり続けたとしてもプロセス \({\it self}\) は \(b\) で停止できないことを意味する。

ノンブロッキングアクションの場合、弱い公平性と強い公平性は同等であるため公平性は 1 種類しかない。

ただの process ではなく fair process と書くことで、そのプロセスのすべてのアクションがデフォルトで弱い公平性であることを保証する。プロセスのアクションのデフォルトの公平性条件は、ラベルの後に + または - を追加することで変更できる。a:+ と書くことでアクション \(a\) が強い公平性であることを保証する。a:- と書くことで \(a\) が公平性条件を満たさないことを保証する。

fair+ process とプロセスを書くことで、そのプロセスのすべてのアクションがデフォルトで強い公平性であることを保証する。プロセスのラベルの後に - を追加することでアクションが公平性条件を満たさないことを保証する。fair+ プロセスでラベルの後に + を付けても効果はない。

fair または fair+ ではないプロセスは不公平プロセス (unfair process) と呼ばれ、そのアクションではなんの公平性仮定も持たない。そのようなプロセスのラベルの後に + や - を付けても効果はない。

以下の翻訳オプションは公平性の仮定に影響する。

-wf

任意の不公平プロセス (前に fair または fair+ が付かないもの) を fair プロセスとする。

-sf

任意の不公平プロセス (前に fair または fair+ が付かないもの) を fair+ プロセスとする。

-nof

すべてのプロセスを不公平プロセスとする。

アルゴリズムの個々のアクションの公平性に加えてアルゴリズム全体の公平性も存在する。この特性はプロセスが少なくとも 1 つの有効化されたアクションを持つならアルゴリズムは停止できないことを保証する。この特性はアルゴリズムを --fair algorithm で開始するか、または -wfNext 翻訳オプションによって保証される。

単一プロセスまたは逐次アルゴリズムの場合、--fair algorithm で開始したり -wfNext, -wf または -sf オプションを使用することは同等である (他のプロセスがなければ、有効化されていないアクション \(\alpha\) に制御がある場合、\(\alpha\) が有効化されることはない)。逐次アルゴリズムの弱い公平性はアルゴリズムの本体を開始する { の前に fair (または fair+) を書くkとによって指定することもできる。ラベルの後に + や - を付けても逐次アルゴリズムでは効果がない。

11 ページのセクション 2.5 で論議した -termination オプションは、上述の公平性オプションがどれも指定されていない場合、事実上 -wf を追加することになる。

アルゴリズムが満たすべき liveness プロパティは、公平性と liveness を表すために使われる TLA+ 時相演算子を使った時相式として記述することができる。これについては 51 ページのセクション 5.10 で詳述する。時相特性は繊細で理解が難しいかもしれない。TLA+ 本のチャプター 8 はこれらの特性をより詳しく説明している。ここでは、非常に便利なある一つの演算子 \(⤳\), タイプは ~>、発音 Leads to についてのみ説明する。

式 \(P ⤳ Q\) は、もし \(P\) が true となることがあれば \(Q\) はその時に true であるか、または後に true となることを保証する。例としてページ 13 の Figure 2 のアルゴリズム FastMutex を考えてみよう。プロセスが公平であると仮定して process の前にキーワード fair を追加する。我々はプロセスが非クリティカルセクションの中に永遠にとどまることを許している。そのためラベル ncs: と cs: の後に - を追加する。

このアルゴリズムが満たしている liveness 条件とは、あるプロセスがそのクリティカルセクションに入ろうとしているとき、あるプロセス (必ずしも同じプロセスではない) がそのクリティカルセクションに入っているか、または最終的に入るというものである。\({\it pc}[i]\) が集合 \(\{{\tt "start"},{\tt "l1"},\ldots,{\tt "l10"}\}\) の中にある場合、プロセス \(i\) はそのクリティカルセクションに入ろうとしている。\({\it pc}[i]\) が集合 \(\{{\tt "ncs"},{\tt "cs"},{\tt "l11"},{\tt "l12"}\}\) に入っていないとき、と表現するほうがわかりやすいかもしれない。それで、我々がチェックしたい特性は、この条件があるプロセスをそのクリティカルセクションに導くことである。この特性は \[ (\exists i \in 1 .. N : {\it pc}[i] \not\in \{{\tt "ncs"}, {\tt "cs"}, {\tt "l11"}, {\tt "l12"}\}) \\ ⤳ (\exists i \in 1 .. N : {\it pc}[i] = {\tt "cs"}) \] と書く。TLC は 3 つのプロセス (\(N=3\)) に対するこの特性を約 1 分でチェックすることができる。

ここで説明した言語構造と変換オプションにより、必要と考えられるアルゴリズムの公平性に関する仮定を全て表現することができるようになる。もしも他の種類の公平性仮定が必要となった場合は 51 ページのセクション 5.10 で説明している TLA+ 時相演算子を使用して自分で書くことができる。

liveness チェック (終了を含む) は不変性チェックよりも遅く、TLC は不変性チェックのような大きなモデルで liveness をチェックすることができない。

4.7 Additional TLC Features

4.7.1 Deadlock Checking

4.7.2 Multithreading

4.7.3 Symmetry

5 TLA+ Expressions and Definitions

5.1 Numbers

5.2 Strings

5.3 Boolean Operators

5.4 Sets

5.5 Functions

5.6 Records

5.7 The Except Construct

5.8 Tuples and Sequences

5.9 Miscellaneous Constructs

5.10 Temporal Operators

5.10.1 Fairness

5.10.2 Liveness

5.10.3 One Algorithm Implementing Another

TLA+ Definitions

References

A The Grammar

B The TLA+ Translation

C Translator Options

Useful Tables

Index

(省略)

翻訳抄

1. A PlusCal User's Manual