ライントレーサー

"Interface" Jan.2010
「外部センサのデータにより、モータの回転を自律制御するアルゴリズムを考えよう！（間瀬順一、吉村悠）」より。
さっと作ると、かなり落とし穴のある制御のモデルになってしまった。
上手いこと制御のアルゴリズムを考えて私に教えてください。

/*
ライントレーサーの制御

ライントレーサーは、光センサーから入ってくる情報を元に、黒のラインの上を走る。
ライントレーサーは3つの光センサーと２つの車輪用モータを持つ
3つの光センサーは、左、中央、右の順に並ぶ。
2つの車輪用モーターは、それぞれ、左の車輪と右の車輪を回す。

*/

abstract sig LightState {}
one sig White, Black extends LightState {}

abstract sig MotorState {}
one sig High,Low extends MotorState {}

sig LineTracer {
	leftLS,centerLS,rightLS:one LightState,
	leftM,rightM: MotorState
}

pred handle[lt,lt':LineTracer] {
	lt.centerLS = Black => lt'.leftM = High and lt'.rightM = High else
	lt.leftLS = Black => lt'.leftM = Low and lt'.rightM = High else
	lt.rightLS = Black => lt'.leftM = High and lt'.rightM = Low
}

run {
	some disj lt,lt':LineTracer | lt.leftLS = Black and lt.centerLS = White and handle[lt,lt']
} for 4 but
	exactly 2 LineTracer