参加者 青木(読み手)、沼田、今井(記)
範囲 pp. 63 – 78
第4章 対象を広げる — Promelaの実行規則
- 4.2 Promela言語の基本
- 4.2.1 主な構成要素
- 4.2.2 通信チャネル
- 4.2.3 プロセス・テンプレート定義
- 4.2.4 その他の重要な言語要素
第5章 仕組みを理解する — SPINの検査法
- 5.1 SPINのツール概要
- p.74 図5.1
「ANCI Cコンパイラ」と「検証器の実行」についている†(ダガー)は、どこかで参照してる? - p.75 下方のコード
なぜ、p には二つも括弧 ((p)) がついているのだろう? 自動生成時に何か都合が良い?
- p.74 図5.1
- 5.2 オートマトンによる形式化
- 5.2.1 システム・オートマトンの合成