------------------------------------------------------------------
第 354 回 PTT のお知らせ
--- Programming Tools and Techniques ---
------------------------------------------------------------------
■日時: 2009年4月23日(木) 18時30分から
■場所: 情報理工学科会議室
（早稲田大学西早稲田キャンパス６３号館５階０５−０６号室）
http://www.ueda.info.waseda.ac.jp/location_j.html
＊なお、この４月から理工は「大久保キャンパス」から「西早稲田キャンパス」
に呼称変更しています（以前は、「西早稲田キャンパス」は本部や大隈講堂な
どのあるキャンパスを指していたのですが、副都心線の西早稲田駅が理工の
キャンパスと直結したため）。ご注意下さい。
■話者: 綾野 貴之 (早稲田大学上田研究室修士1年)
■題目: 統合開発環境によるLMNtalモデル検査
■概要:
階層グラフ書換えに基づく並行計算モデルLMNtalの新たな応用の開
拓を目指して，LMNtalをモデリング言語とするモデル検査器を構築
し，記述実験と改良を重ねている．新たに構築した統合開発環境
LMNtalEditorは，LMNtal処理系やモデル検査器の操作を容易にする
だけでなく全実行経路の可視化機能や重要な状態の発見に役立つ機
能，実行経路を解析し動作の特徴を捉える描画機能などを備えてい
る．モデル検査，探索問題，非決定的計算を含む多様な例題を
LMNtalEditor上で実行することで，本統合環境がモデルの挙動や性
質，反例の理解に役立ち，また検証作業の効率を大幅に高めること
が確認できた．本発表では，LMNtalEditorを利用したLMNtalプログ
ラムの記述例，動作例，可視化例などを紹介する．
----------------------------------------------------------
第354回 PTT report
出席者：和田英一（IIJ）、寺田実（電通大）、後町将人、岩澤宏希、上田和紀、
馬場裕太（早大）、伊知地宏（ラムダ数教研）、小林弘明（元電通大）、丸山一
貴（東大）（以上10名）
質疑応答：
Q.水差しの問題では水は大量にあると仮定？
A.はい。水は無限にあると仮定します。
Q.『リンク』はそのアトム間の棒のことを示すか？『2』というデータもアトムか？
A.両方ともそうです。
Q.リンクは膜を突き破ることはできるか？
A.膜を突き破るリンクも接続できます。
Q.どっちの『450』が最大容量で、どっちの『450』が現在容量か？
A.リンク番号が振られているのでそれで判別することができます。
Q.プログラム可視化ツールで柔軟に動いているのはなぜか？
A.力学の計算を使って位置を求めています。サッカーボールみたいな図形も綺麗に表示できます。
C.柔軟だから複雑なものも自動的に位置を求めることができるのですね
Q.10個の要素のバブルソートで5700状態もなる？
A.書き方によって多くの非決定性があります
Q.状態遷移の可視化で戻る遷移は禁止している？
A.バックエッジも描画しています
Q.横軸は時間軸なの？
A.時間軸では無いですが、最小ステップ数を表しています。
Q.水差しの問題の状態遷移でいきなり最初に戻るのがあるけどそれはなぜか？
A.例えば操作を繰り返して片方の水差しに100を作って、それを捨てると初期状態になる場合があります。
Q.500と700の水差しでは100刻みでしか作れないということか？
A.そのようになります。水差しの数や容量を変えると作れる水の量が変わります。
Q.縦に並んでいる状態は何を表しているか？
A.同じステップ数で遷移できる状態同士が縦に並んでいます。
Q.状態遷移を示す線を重ねないようにする工夫はしているか？
A.状態を再配置するアルゴリズムを実装しています。
Q.状態を再配置するプログラムはLMNtalで書いている？
A.現在はJavaで書いています。
Q.食事する哲学者の問題で最初のステップで一遷移になっているのはなぜか？
A.書き換える箇所が異なっても、LMNtalにおいてグラフ構造が等しいためです。
C.それぞれの哲学者にIDがないということですね。
C.食事する哲学者では天邪鬼が大事ですね。
Q.天邪鬼が二人いるとどうなるか？
A.デッドロックは起きません。
Q.膜の中にcアトムがあっても差分管理できるのか？
A.上手く差分を管理すれば可能です。
Q.メモリを増やすことによってスケーラビリティを増やすという手は？
A.やっていないですが検討してみます。
Q.LMNtalは予約語がほとんどないのか？
A.基本的にありません。
Q.LMNtal処理系は大体何行くらいコードを書いているか？
A.統合開発環境が約10,000行、モデル検査器(C言語で書かれたランタイム)が約15,000行
コンパイラが約25,000行、Javaで書かれたランタイムも約25,000行程度です。
Q.膜を使ったプログラムの話があまりなかった様に感じられたが、使っているのか？
A.ビザンチン将軍問題では膜を使っています。哲学者の問題でも使っています。
哲学者の問題では使用される順序を意識しないためフォークをアトムでは無く膜で表現しています。
Q.LMNtalにおけるリストのappendのプログラムはある？
A.あります。
Q.統合環境のユーザビリティの向上を今後の目標としていたが、具体的にはどのようなことを考えているか？
A.プログラムのエディタで繋がっているX同士は同じ色になったりを予定です。
Q.エディタ上に様々な色が出てくると見づらくなるのではないか？
A.その可能性もあります。ハイライティングなども考えています。
Q.状態遷移の可視化はプログラムのデバッグに使えるか？無限状態ではだめではないか？
A.確かにバグで無限状態になってしまうと状態遷移の可視化はできないのですが
バグで状態遷移が少なくなる場合はデバッグに役立ちます。
Q.状態数が同じくらいになってしまうバグだと分かりにくいかも
A.その場合は状態の遷移をよく見てもらうことになります。
Q.無限状態になる場合、止めることはできるか？
A.状態数などの上限値の設定はできませんが、ユーザーが任意のタイミングでモデル検査器を止めることができます。