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

付録A.5 の小さなケーススタディの鉄道のスイッチングです。

• A.5.2 (c), (d), (e), (f)

open util/ordering [TrainState]

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

sig Train {}

sig TrainState {
  on: Train -> one Segment,
  occupied: Train -> some Segment
} {
  all t: Train |{
    t.occupied = t.on.^overlaps
  }
  all disj t1, t2: Train |{
    no t1.occupied & t2.occupied
  }
}

sig GateState {
  closed: set Segment
}

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

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

pred transit (ts, ts': TrainState, g: GateState, t: some Train) {
  let m = { x: t | not ts.on[x].next in g.closed } {
    ts'.on = ts.on - (m -> ts.on[m]) + (m -> ts.on[m].next)
  }
}

run {
  #overlaps > #Segment
  all ts: TrainState - last {
    let ts' = ts.next {
      some t: Train | one g: GateState {
        transit [ts, ts', g, t]
      }
    }
  }
}

• • TrainState の制約として overlaps で重複している Segment のなかには1つしか Train が存在できないようにしています (f)
  • util/ordering を使って TrainState を時系列で並べるようにして、その間の Train の移動を記述するようにしています (c), (d)
  • GateStatus を導入して侵入できない Segment を指定するようにしています (e)

次はこの GateState を適切に指示するポリシーを作らないといけないのですが、なかなか難しいですね。