C Manual (PlusCAL) つづき。３章。
Cマニュアル、意外によみやすいのでこのまま続けて読むことにした。
3は言語仕様。
3.2.1 Assignment
:= はわかる。けど、-> と |-> の違いがいまいちわかってない。S->Tは写像（集合と集合のマッピング）と理解できそうだけど、それだけだとしっくりこない使い方もされている。
| はPlusCALの特殊表記。同じ変数への複数の代入をアトミックに行うときに使う。主に arrayなどに使うことになりそう。 |
3.2.2 If
If (test) hogehoge else boroboro
TLA+の場合は IF THEN ELSEだったと思うので、ちょっと違う。
3.2.3 Either
etiher A or B or C
と使う。TLC(TLAのモデルチェッカー）にどれか選ばせる（というか全通り組み合わせを調べさせる）ための分岐。
なので、switch文とは違う。
3.2.4 While
label_1: while (test) body
まあ、普通だ。なんでわざわざlabel_1: とラベルがついてるかというと、while文にはかならずラベルがつくという鉄の掟があるから。もちろん、translatorが必要に応じてつけてくれるんだけど、鉄の掟を忘れぬようにとのLamport先生がおっしゃっております。
3.2.5 Await (When)
条件がTrueになったときだけ実行される。主にマルチプロセッシングのblockingを表現するのに使う。同じラベルの中であれば、どこにあろうとその条件を満たさなければそのラベルは実行されない。
3.2.6 With
with (id \in S) body
Sが空じゃない時は、idはSからランダムに選ばれる。これまたTLCに分岐させるために使われるってことだな。
Sが空の時は待つ。つまりblock。
3.2.7 Skip
なにもしない。
3.2.8 Print
何かを表示。モデルチェック的には何の影響もないのでskipと同じ。
3.2.9 Assert
TLCモジュールが必要。 モデルチェック的にはなんの影響もないが、assertがFalseになればそこでエラーとなる。
3.2.11 Goto
どこかのラベルに飛ぶ
3.3 Process
process (ProcName \in IdSet) と複数プロセスを定義するか、process (ProcName = Id) と一つのプロセスを定義するか。
宣言の次に local variableを持つことができて、その後に bodyがくる。
3.4~3.6 Procedure, Macro, Definition
Procedureはさっき飛ばした3.10のcall, returnを使う。正直、この後の Macro, Definitionと合わせて理解が充分でない。今後復習したい。
3.7 Label
何度も出ているラベル。いつものラベルを置けるところ、置かないといけないところのルール。
