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

付録A.5 の小さなケーススタディから

A.5.1 の Unix ファイルシステムは 10個のアドレスを扱うというのが Alloy の設定でデフォルト 4bit までしか扱えないので断念(設定で増やせると思いますが)。
A.5.2 の鉄道のスイッチングをやってみます。

• A.5.2 (a), (b)
  • next は lone にしてみましたが set でよかったかも
  • next が自分自身に連結するのはなしに
  • overlaps は反射的、対称的としましたが推移的ではないとしています。並行して3つの区間があったとして真ん中と両隣は近接していて(接触の危険があって)も端同士は安全でありうるので

sig Segment {
  next: lone Segment,
  overlaps: some Segment
}

fact {
  all s: Segment {
    s != s.next
  }
}

fact {
  (Segment <: iden) in overlaps // 反射的
  ~overlaps in overlaps  // 対称的
}

run {} for exactly 4 Segment