「SPINモデル検査」第20回(7月19日)

Posted on by 0 comment

参加者 今井(読み手)、青木(記)
範囲 pp. 195 – 204

第9章 ケーススタディ(4) 検査対象の大きさを適切に保つ — 抽象化の方法

  • 9.3 制御の流れに着目した抽象化
    • 9.3.3 関連する話題 (p.195 9行目から)
  • 9.4 連続時間の抽象化
    • 9.4.1 時間オートマトン
    • 9.4.2 リージョン・オートマトンの解析
      p.201 l.2 「図9.16の状態S0からの3つの遷移は」は「図.9.18の状態S0からの3つの遷移は」の誤りではないでしょうか。
      p.201 の「図9.20遷移(その1)」のifブロックのs.regionが非決定的に選択される箇所の「::s.region=R01」は「::s.region=R10」の誤りではないでしょうか。

コメントを残す

メールアドレスが公開されることはありません。 * が付いている欄は必須項目です

CAPTCHA