pan.c -> pan (PAN: Process ANalyzer) と進む前に、channel について。
channel は、プロセス間のデータのやりとりを抽象化したものとなる。
/* ex04.pml */
mtype = {ping, pong};
proctype A(chan ch)
{
ch!ping; /* (a) */
ch?pong; /* (b) */
}
proctype B(chan ch)
{
ch?ping;
ch!pong;
}
init {
chan ch = [1] of {mtype}; /* (c) */
run A(ch);
run B(ch);
}
上のコードの (a) がデータの送信、(b) がデータの受信を表す。 受信の引数で定数((b) では pong)を指定した場合、その定数が受信できるまでプロセスの実行はブロックされる。
channel の生成は (c) で行っている。ここでは、channel ch が mtype (整数をシンボルで定義した、Cで言う enum のようなもの) をやりとりする、キューのサイズが 1 の channel であることを示している。
これを実行すると、process A() は ping を送信して pong 受信を待ち、process B() は ping 受信を待って pong を送信する動作を行う。
channel のやり取りを見るために spin には -r , -s , -c , -C といったオプションがある。-r , -s はそれぞれ channel の受信／送信したデータを表示する。
spin -r ex04.pml
を実行すると、
4: proc 2 (B) line 12 "ex04.pml" Recv ping <- queue 1 (ch) 6: proc 1 (A) line 7 "ex04.pml" Recv pong <- queue 1 (ch)
と表示され、
spin -s ex04.pml
を実行すると、
3: proc 1 (A) line 6 "ex04.pml" Send ping -> queue 1 (ch) 5: proc 2 (B) line 13 "ex04.pml" Send pong -> queue 1 (ch)
と表示される。また、
spin -r -s ex04.pml
のように同時に指定することも出来、この時は、
3: proc 1 (A) line 6 "ex04.pml" Send ping -> queue 1 (ch) 4: proc 2 (B) line 12 "ex04.pml" Recv ping <- queue 1 (ch) 5: proc 2 (B) line 13 "ex04.pml" Send pong -> queue 1 (ch) 6: proc 1 (A) line 7 "ex04.pml" Recv pong <- queue 1 (ch)
というように受信、送信を合わせて表示する形となる。(表示される先頭の数字は、実行するごとに異なる)
別形式で整形した表示を、-c を指定する事で行うことができる。
spin -c ex04.pml
で、
proc 0 = :init: proc 1 = A proc 2 = B q\p 0 1 2 1 . ch!ping 1 . . ch?ping 1 . . ch!pong 1 . ch?pong ------------- final state: ------------- 3 processes created
といった表示になる。
使用している channel のデータは、-C と -g を組み合わせて表示する。
spin -C -g ex04.pml
で、
chan A-ch
imported as proctype parameter by: A par 1
received from by: A
sent to by: A
chan B-ch
imported as proctype parameter by: B par 1
received from by: B
sent to by: B
chan :init:-ch
exported as run parameter by: :init: to B par 1, :init: to A par 1
と言うように、channel の名前(プロセス名-チャンネル名)、どこから指定されたものか、送受信はどこで行うかといった情報が表示される。
4月に買った SPIN の本が、引越しの荷物に紛れて見つからない。英語版は発掘済みなのに。