学生課から、製本論文の提出への案内があった、しかしまだ指導教官のＤ論修正指摘事項が反映できてない。 (1)関連研究の記述の補充、それに伴う文献リストの充実 (2)2章eMSCシステムから、3章プロセス代数(形式化)への橋渡 形式化を行う必要のある部分を限定…

2時間前にはいって、D論の修正原稿を審査委員の先生分印刷をしようとしますが、ここでコピー機が壊れてしまい、kinkosに飛んだりしてバタバタします。審査会本体は、もうぼろぼろ、まあD論をそのまま発表しているからしょうがないですね。とはいっても縦・横…

結局、家族の用事があって、修正する時間が夜中しかとれません。 充足性演算における非決定性の取り扱い タイポ等 は修正しましたが、 連動性の計算のところのロジックの不全 は厄介です。この日記をたどる（といっても９月）と、弱双模倣性は＋結合のところ…

縮めても64page。もうどうしようもありません。というところで、外部審査委員の先生よりコメントがかえってくる。なんて律儀な。 充足性演算における非決定性の取り扱い 連動性の計算のところのロジックの不全 タイポ等 の指摘。ありがたい、最初の非決定性…

マテリアルの取捨選択と、構造調整で80pageを65pageにできた。しかし目標は50毎強。 まだ10pageを消滅させるには、いろいろ削らないといけないし、Result, Discussionは補強は必要だ。というところで時間切れ。

スライドの修正は終了、といっても予備審査のものをupdateしただけ。IMRAD(Intro,Method,Result,and,Discussion)に従って見直すと、構造になってません。ただD論に書いてあることを書き並べただけ。課題(I)に対して、Methodを使い、必要ならば創造して(M)、…

予備審査から進んだところは制約の精査だったので考察と修正 nを決めるのが重要 検証の手間や実装でバッファ長をどれだけにすればよいかを考えるため nは他の制約とからめると決まる場合がある（横、縦チェーン） 具体的にnを追い詰めることを横・縦チェーン…

今日も時間を縫って、土曜朝マック。壁は"Softeware Abstraction"の本の絵柄と同じ絵の内装なのがご愛嬌。 縦チェーン・横チェーンの修正をあわせた 性質の考察の追加 後者は予備審査のときからの進捗したものであり、これに基づいて、縦横チェーンの検証も…

仕事がらみで参加した学会（この発表の準備もあった）で、副主査の先生（田中先生）にお会いできた。懇親会でいろいろ伺うと、７日の公聴会の話になって、「いやああなたのは難しいねエー」ということで、読み手にわかりやすくないことが判明。また指導教官…

beamerでverbatim環境をつかうのにfragileをつかっていたのだが、どうも[containsverbatim] を使うのが正しいらしい。はまる。２項目前進

Beamerでしおりが文字化けを起こさないようにするには以下をプリアンブルへ \AtBeginDvi{\special{pdf:tounicode 90ms-RKSJ-UCS2}} Beamerでは\verb+hoge+はうまくきかない というわけで2/12まで進んだかな。。。

直さなければ行けない項目 ACP,CCS,ACP_drtの絵と関係の説明 Acp_drtのチャネルのルールと例の修正 COMの導入 の詳しい説明 との修正 のルール CWBによる充足性検証 CWBによる連動性の検証(can_livelock)の説明 横チェーン検証の修正 縦チェーン検証の修正 I…

指導教官の指摘事項31件を全てクリア、タイポ、説明の足らないところ、章立ての修正等の、振り返れば見栄えに関するところかなあ。というわけで来月7日に決まった公聴会向けにスライドを作りなおさねば。ちょうど１年前は予備審査したスライドがありますが、…

先生の指摘事項の修正中、進みません。今日は24/31まで進行。

校正を合間をぬって行う。いろいろ学会の流儀があるんだなあー。 「同士」→「どうし」 「一旦」→「いったん」 「全て」→「すべて」 「A.Tarski」→「Tarski, A.」 言い回しが変だだったり、表の説明が本文に内のもあったりして冷や汗もの。得意のEXPACKにして…

情報処理学会の投稿論文の著者校正が来た。いろいろ直すプロというのがいるものだなあ。１３日までに直して送らないといけない。またD論をやっと担当先生が見てくれて、いろいろ間違え（ミスプリレベル）の指摘が来る。 とりあえず直しますが、これを直して…

D論は無事２日の11時AMに到着した（EXPACKはいいな）ところが、どうも論文は、簡易製本してあることが必要だそうで（閲覧に供するため）、簡易製本のファイルを遅れとの連絡が教務係からきた。いそいでファイルを準備し、会社の帰りにEXPACKで送った。製本し…

チャネル周りの意味論を見直してなんとか、それ以降の展開式が説明できるのでまあいいか。というところでやめた。よくよく調べると、２日が締め切りというのは２日に石川に物理的についてないといけないらしい。。。。家に帰って、最終修正して、必要書類を…

チャネルの導入とその動作の操作的な意味定義がおかしい、いい加減だというわけで急遽見直ししている。どんなにダサくても、ちゃんと動作が復元できる、操作的意味をつくるしかない。もう明後日提出だし。。

先生との打合せ 「はじめに」の最初で各章で何が語られるか照会する 「おわりに」で各章で何が語られたかをサマリする 「まとめ」に設計問題からみた課題（制約をあたえて合成する＋αの話）を追加すること とくにパラメータ？に対するsensitivity?の話 「関…

家族が帰ってくるので、実質の最終日でした昨日は、朝から千葉方面に 遠征。227km走って17.4km/lの燃費、なかなかよい。ではなくて昼過ぎには 帰って、後半の補強２ やったこと 様相論理(HMLでいいから)の説明をどこかに 特に最大、最小不動点のところは補強…

ぐるぐるまわってましたが、とりあえず。形にしました。モザイク模様なのは、D論らしい。 つかれたので、今日は外の空気を吸ってきます。 やったこと ACPとCCSの関係を、前段に移動 実装のところを、うまく整理、 シナリオ合成、シナリオマージ（いわゆる後…

どうもACPとCCSの続きのところをやってると、ルールが足らなかったり、上書きの場合()の場合どするとか、いろいろ決めないといけないことが抜けてます。それにACPとCCSの関係を、「プロセス代数による形式化」の章の後でこそっと入れるのはいかにも罰がわる…

連休で家族を送り出し、ぼちぼちやってます。それにしても、この日記は Chrome+モバイル環境では、なぜかまともに記事を書くことができません、しょうがないからFireFox復活。IE8いれたろか。 やったこと ACPでの順序制約や演算について、CCSのそれを補足す…

またまた土曜は朝からMacで活動いろいろボロが見えてきましたが27日に指導教官との打ち合わせを設定して、それまでにD論をがんばって書かねば、実装ACP_drtへの展開を考えるとCCSで書かれたLTSでいろいろ検証とかするのは都合が悪いことが判明。といってもCC…

ACPもCCSもプロセス代数の一派で、どちらがどちらというわけではないのですが通信を伴わない動機並行動作を表現しようとするとACPの方が優れていて、そこからACP_drtなる離散時間版を展開したりしています。どうもD論では、CCS,ACP,ACP_drtが入り乱れていて…

いろいろ考えたら無限の内部遷移()のループに陥る可能性があることを プロパティでかけばよいではないか。 prop can_livelock = min X = livelock_now \/ <->X prop livelock_now = max X = <t>X最大不動点と最小不動点の組み合わせたプロパティになる。 proc X</t>…

Ｄ論みなおしていて、連動性の検証をCWBでやっていたのだがどうも変だ X=a.b.X, Y=c.d.Yのとき Z=X|Yに対して ZはXあるいはYに対する連動性がありません ずっとX(Y)が占有する可能性があるから というのをCWBで占めそうとおもったのですが obseqオプションは…

順序制約に関する正しい分解法則を整理して、横チェーンの見直しと縦チェーンの見直しをほぼ終了。ふと振り返って、それ以前の充足性の判定とか演算の導入とかみると、いまやったところと温度差がありすぎ、記法もバラバラ、n巡目を区別するといっていてもな…

最近の考察に従い横チェーンの検証の節を少し修正、１時間３０分で少しすすんだ、毎日やらないとだめだ。。