|
⇤ ← 2014-01-20 12:33:16時点のリビジョン1
サイズ: 783
コメント:
|
← 2014-01-20 12:37:26時点のリビジョン2 ⇥
サイズ: 775
コメント:
|
| 削除された箇所はこのように表示されます。 | 追加された箇所はこのように表示されます。 |
| 行 19: | 行 19: |
| Part 2（Artho先生パート）で使用したDining philosophersのコードを上のプリントの通り改変し、LTL式G F eat0で表わされる性質をJPFで検証。 | Part 2（Artho先生パート）で使用したDining philosophersのコードを上のプリントの通り改変し、LTL式で表わされる性質をJPFで検証。 |
計算システム検証論
開講時限・場所
- 月曜 2限 理学部7号館102教室
担当教員
- 萩谷 昌己
- Cyriille Artho
- 田辺 良則
- (Yusuke Kawamoto)
課題
萩谷先生のLTL+JPF課題(1/26〆)
Part 2（Artho先生パート）で使用したDining philosophersのコードを上のプリントの通り改変し、LTL式で表わされる性質をJPFで検証。
JPFでLTL式を扱う方法は 田辺先生のプリント配布ページ に上げられている。