|
5
|
1 \section{ Socket Simulator}
|
|
|
2
|
|
|
3 Java Pathfinder による検証を行なうために、直接、Socketを経由せずに、
|
|
|
4 Thread を通して通信を行なうライブラリを作成した。
|
|
|
5
|
|
|
6 このライブラリは、最初、java.nio互換ではなく作成し、Merge Protocol
|
|
|
7 (A)及び(B)の動作をJava PathFinder で確認した。編集結果の同一性を
|
|
|
8 調べるために、Session 内の Editor のquit プロトコルを実装している。
|
|
|
9
|
|
|
10 まず、 {\tt quit } Command がSessin ring に送られ、各Editorは、
|
|
|
11 {\tt quit}を受け取ると、自分のユーザ編集コマンドを停止する。その編集を
|
|
|
12 終了した後、{\tt quit}を返す。{\tt quit}を受け取った後も、他の
|
|
|
13 Editor からのEditor Commandは来る可能性がある。{\tt quit}を最初に
|
|
|
14 送ったEditorに{\tt quit}が戻ると、今度は{\tt quit2}をSession Ring
|
|
|
15 に流す。これより後に、ユーザ編集コマンドが来ることはない。Editor は
|
|
|
16 自分の待っているEditor Commandのackがすべて来るのを確認してから、
|
|
|
17 {\tt quit2}を次へ渡す。{\tt quit2}を渡した後は、Editor Command は
|
|
|
18 来ないので、終了して良い。最初のEditorへ{\tt quit2}が戻った時点で、
|
|
|
19 すべての編集が終了する。
|
|
|
20
|
|
|
21 この時に、Editor のバッファを比較して、
|
|
|
22 すべてのEditorのバッファが同じならば、正しくプロトコルが動いた
|
|
|
23 ことになる。これをJava PathFinderで検証を行なう。
|
|
|
24
|
|
|
25
|
|
|
26 (C)の実装を、実際のSession Manager 上で検証するために、java.nio と
|
|
|
27 Thread による通信のシミュレーションを切替えることが可能なライブラリ
|
|
|
28 を作成した。実際のSession Manager に対する Java PathFinder での
|
|
|
29 実行確認は、計算時間の制約により、まだ、可能とはなっていない。
|
|
|
30
|
