PlusCal構文 - TLA+メモ@ウィキ

PlusCal構文

素のTLA+の記述はプログラマにとっては馴染みのないもののため、プログラマでも分かりやすく、記述しやすいPlusCal記法が用意されている。
PlusCalはTLA＋に変換され、記述された仕様がある条件(不変条件やアサーション)を満たすかTLAのモデルチェッカ(TLC)が検証する。
PlusCalによる記述は必ず必要というわけではない。TLA+のみで記述しても検証はできる。

---- MODULE HelloWorld ----
EXTENDS TLC
(* --algorithm HelloWorld {
  {
    Greeting:
      print "hello, world";
  }
} *)
 

PlusCal の構文は(* *)で囲まれた部分、”--algorithm [モジュール名] から end algorithm;” までの間で、それより外は TLA+ の構文である。
PlusCalの構文は最終的にTLA+に翻訳される。PlusCal構文の構造は決まっていて、以下のように正しく並んでいることが求められる。

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

p-構文とc-構文

PlusCalには、p-構文とよりコンパクトなc-構文の2つの別々の構文がある。2つの構文で記述されたコードのスニペットを次に示す。

p-構文

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

c-構文

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

p-構文はPascal風に”begin”, “end”等を使ってコードの開始、終了を明記する。c-構文はより簡潔に”{ }”でくくることで表現する。
C++、C#、Java などの C から派生した言語でのプログラミングに慣れている場合は、c-構文がおすすめ。

変数宣言

PlusCalでは以下のように変数を宣言する。

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

初期化は必須ではない。宣言時に型は明示しない。文末にセミコロンをつける。

\inによる初期化

変数は”=”だけでなく、”\in”で初期化することができ、値のとりうる範囲を指定することができる。
以下のような場合、yは1から10のいずれかの要素になることを示す。この場合、TLCはy=1のケースで検証を行い、次にy=2のケースを検証し、y=3,4,5..10のケースを検証する。

variables x =1, y \in 1..10;
 

PlusCalにおける“=”と“:=”およびTLA+における” x ”と“ ｘ’ ”について

PlusCalでは “=” が等価記号で “:=” が代入となる。しかし、初期化のときだけは “x = 1” と記述する。
原則として、変数を最初に扱う場合のみ、“=” は初期化として扱う。

これは変換先にあたるTLA＋自体には代入というものが存在しないため。TLA＋ではxを初期化した場合は”x = 1” と記述する。
xが初期化されていて、2を割り当てたい場合は、“x’ = 2”と記述する。xと1を比較したい場合は“x = 1”と記述する。
TLA+では代入という概念自体がなく、xの次の状態をx’で表す。”x’ = 2” はxの次の状態が2になるということを示す。

変数に対する操作を整理すると以下のようになる。

言語	宣言	初期化	更新	比較演算子
TLA+	VARIABLES x	x = 1	x’ = x + 1	x = y
PlusCal	variables x	x = 1	x := x + 1	x = y

define宣言

PluaCal構文にて宣言した変数は”BEGIN TRANSLATION”の行に続いて、TLA+で定義される。
そのため、“(* --algorithm “より前では演算子の定義などにPluaCal構文にて定義した変数を使用することができない。
この問題に対応するため、variables宣言の後に続いてdefine宣言を行い。define宣言内でPlusCal構文にて宣言した変数を使用して、グローバルに使用できる演算子を定義することができる。

マクロ

Pluscalではマクロを定義することができる。

macro Name(var1, ...)
{
   \* body
};
 

• マクロはTLA＋に翻訳される際にインライン展開される。そのため、ラベル、変数の割り当て、whileループを定義することはできない。
• マクロ呼び出しには”call”は不要。returnはない。

プロシジャ

プロシジャはマクロと似ているが、ローカル変数を宣言することができる。

procedure Name(arg1, ...)
variables var1 = ... \* This cannot be \in, only =
{
    Label:
    \* body
    return;
};
 

プロシジャの制約は以下のようなものがある。

• PlusCalのプロシジャを使用する場合は標準モジュールSequencesをEXTENDSに含む必要がある。

これはTLA+に翻訳される際、プロシジャを処理するためにスタックが導入されるため。

• プロシジャのreturnは呼び出し元に値を返さない。
• プロシジャはマクロの後、プロセスの前に定義する必要がある。
• プロシジャはマクロを呼び出せるがマクロはプロシジャを呼び出すことはできない。
• プロシジャからプロシジャを呼び出すことができる。再帰的に自身を呼び出すこともできる。
• プロシジャでプロセスを使うことはできない。
• プロセスはマクロ、プロシジャを呼び出すことができる。
• プロセス内でプロシジャを呼び出すときは、プロシジャの名前の前に”call”をつける必要がある。プロセスから呼ばれるプロシジャにはラベルが定義されていなければならない。
• プロシジャはローカル変数を定義することができる。ただし等式(=)のみで集合(\in)にすることはできない。

Init, Next, Spec演算子

PlusCal記法で記述された内容はTLA＋に変換される。TLA+に変換される際にはかならず(?)、Init, Terminating, Next, Specという演算子が定義される。

Init演算子

初期状態を表す。通常、システムの状態変数に対する初期値の条件が含まれる。宣言した変数はInit中で必ず全て初期化される。

Terminating演算子

終了条件が定義されている。pc[]が”Done”となり、かつ、すべての変数がUNCANGEDとなる（つまり、変化がなくなる）ことが定義される。

Next演算子

PlusCalから変換された場合は状態遷移の分岐が定義される。

• Nextから先の状態遷移ではすべての変数の新しい値を設定する必要がある(PlusCalから変換された場合は自動的にすべての変数の新しい値が設定されている)。
• 全ての変数に新しい値を設定するのは煩雑なためEXCEPT構文がある。

Spec演算子

以下のような記載がされているはず。

Spec == Init /\ [][Next]_vars
 

このTLA+の文は、システムの仕様（Spec）を定義している。ここで、2つの主要な要素が含まれている。
“[][Next]_vars”の部分は、システムの状態遷移に関する性質を表している。[]はTLA+の「常に（always）」という時相論理演算子で、Nextは状態遷移を表すアクションである。_varsは、システムの変数のタプルを指している。
ボックス演算子:[P]_xは特殊な糖衣構文で“[](P \/ UNCHANGED x)” という意味となる。つまり、”Spec == Init /\ [](NEXT \/ UNCHAGED vars)”となる。
システムの仕様Specは、初期状態Initと状態遷移[][Next]_varsの論理積（/\）で定義され、時相論理式の慣例として時相論理式([]または<>)の外側は初期状態で真として扱われる。
つまり、Specは、システムは初期状態Initが真で始まり、その後のすべての状態遷移がNextの定義に従って行われるか、変化しないことを意味している。
この定義により、システムの振る舞いに関する性質や制約が表現される。

制御構文

PlusCal で制御を記述するための構文のうち if-else, while, goto の 3 つはすべて一般的なプログラミング言語と同じ機能である。

if-else文

If( condition ){ statements }else if( condition ){ statements }else{ statements }
 

while文

for文に相当する構文はPlusCalには存在せず、whileとループカウンターを組み合わせて実装しなければならない。
while文の前にはラベルを記述しなくてはいけない。

label：while( condition ) { statements };
 

call文

プロシジャ呼び出しの前にはキーワード call を付け、その後にラベルを付ける必要がある。

call proc( );
label :
 

goto文

ラベルの処理へジャンプする。

goto label;
 

非決定性挙動を記述する制御構文

非決定性挙動を記述する構文について

either

either構文は、複数のアクションのうち1つを非決定的に選択して実行する。
either構文内には、それぞれのアクションが別々のブロックで記述され、実行時にランダムに1つが選択される。
これにより、アルゴリズムの並行性や非決定性をモデル化する。

either{ statements }or{ statements }or{...}
 

例えば以下では1つ目のアクションでは、変数xの値が1増加し、2つ目のアクションでは、変数yの値が1増加する。
実行時に、これらのアクションのうちどちらか1つがランダムに選択され、実行される。

variables x = 0, y = 0;
  {
    either {
      x := x + 1;
    }
    or {
      y := y + 1;
    }
  }
 

either-or の本体が await を含む場合、有効化されていない選択肢に制御が移ることはない。
これはしばしばマルチプロセス環境で複数の await 待機から有効化された処理のみを実行する目的で使用される。

with

集合Sの中からランダムに要素を選択し、body部分を実行する。Sが空集合の場合、実行されない。(ノンブロックであることに注意)

with (id \in S ) { body }
 

例えば以下では、一時変数iに1から3の範囲の値が非決定的に割り当てられる。
その後、x := x + iというアクションが実行され、変数xの値がiだけ増加する。実行時に、iにどの値が割り当てられるかは非決定的となる。

variables x = 0;
{
    with (i \in 1..3) {
        x := x + i;
    }
}
 

with ステートメントの中はラベルを設置することができない。
この制約からラベルを必須とする while などのいくつかの機能は with 内では使用することができない。
使い方によってはfor文の代わりにできるかも？

並行処理に関する制御構文

並行処理について説明する。

プロセス

プロセステンプレートを宣言し、複数のインスタンスをもつことができる。
PlusCalでは実行中に動的にプロセスを生成することはサポートされていない。

( fair | fair+ ) process (ProcessName \in {Set})
variables anyname = anyvalues;
{
\*body
}
 
\* single procee
 
( fair | fair+ ) (process ProcessName = "p1")
variables anyname = anyvalues;
{
\*body
}
 
 

プロセス内からプロセス番号にアクセスする場合は、selfでアクセスする。

ラベル

ラベルの有効範囲はラベルを定義してから次のラベルが現れるまでの間となる。

原子性の粒度

ラベルは原子性の粒度を決定する。TLCはラベル内のものを1つのステップとして実行するもの(アトミック操作)とみなす。これは並行処理の検証において重要である。
ラベル内の全操作が完了するまで、他のプロセスはその途中の状態を観測できない、不可分な操作となる。
PlusCalをTLA+に変換すると現在のラベルを追跡する変数pcが定義される。(pcは「program counter」の略)

ラベルを配置するルール

ラベルは以下のルールに従って配置しなければならない。

• 各プロセスの開始と各while文の前にラベルを配置しなければならない。
• マクロやwith文の中にラベルを配置してはならない。
• goto文の後に必ずラベルを配置しなければならない。
• eitherまたはifを使っていて、その中にラベルを含んでいる分岐がある場合は、制御構造が終わった後にラベルを配置しなければならない。
• ラベル内で同じ変数に2回代入を行ってはならない。

補足：各プロセスの最後に暗黙のラベルDoneがある。Doneを自分で定義することはできないがgoto文でジャンプすることは可能。

ラベル内の変数への代入

ラベル内での変数の代入は1回しかできないという制約がある。そして以下のような場合、2回代入と判定されてしまう。

Struct.key1 = 1;
Struct.key2 = 2;
 

このような場合、”||”でつなぐことで1回の代入とみなされる。

Struct.key1 = 1 || Struct.key2 = 2;
 

await 文

await condition
 

ラベル付けされたステップ中に await 文が含まれているとき、TLC はその条件式が true となるまでそのステップを実行対象から除外する (await の位置で停止するわけではない点に注意)。
これは別のプロセスが条件式を true とするような作用を起こすことを暗に期待しており、プロセス間の同期ポイントと考えることができる。
await 文はステップ中のどこでも配置することができるが、そのステップに入る前に条件式が false であった場合、同一ステップ内で await より前に配置されている別の処理を実行しないまま停止する。
この直観的ではない挙動がしばしば混乱を引き起こすため、可能な限りラベルの直後に await 文を配置することを推奨する。

その他

assert文

exprがFALSEなら中断し、エラーメッセージが表示される。TLCモジュールをEXTENDSする必要がある。

assert expr;
 

補足：TLA+にもAssertがある(頭文字が大文字)。 expr が falseならmessageが表示される

Assert(expr, message) 
 

print文

exprの内容を表示する。

print expr;
 

skip文

何もしない。