抽象によるソフトウェア設計 付録A 練習問題 その19

付録A.4 のメタモデル続き。

• A.4.2 状態機械の模倣関係
  • 状態機械の遷移にラベルをつけて、遷移経路をラベルの配列の「トレース」で表現する

sig Label { trans: State-> State } { one trans }
sig State {}
sig StateMachine {
  states: some State,
  first: some State,
  labels: some Label
} {
  first in states
  labels.trans.State in states
  labels.trans[State] in states
}

run { one StateMachine }

• • • 「トレース」を pred か fun で定義しようと思ったのですが、「可変長のラベルの配列(リスト)の集合」のようなものを作らないといけなくて、そうすると型がトレースの長さで変化することになるので、どう定義すればいいのかわからずギブアップです。
    • ぱっと考えるとトレースは無限列になりうる(ループする)と思うのですが、定義には「有限列」と書かれているので、まずトレースの理解が誤っているのかもしれませんが……

というわけで A.4.2 はこれでおわりにします。4.3, 4.4 は Alloy と Java のメタモデルということで強烈そうなのでこれもスキップして次は A.5 からできそうなものを選んでやりたいと思います。

付録 A が終わるとあとはリファレンスや Alloy 以外の証明ツールの話なので、そろそろ読み終えることにして、次の本を考えないといけませんね。次は何にしようかな。