An operation
	• In any step, any number of trains can move; no train goes through a closed gate    op TrainsMove(ts: Train) {   all t: ts | t.on’ in t.on.succ   no (ts.on.gate & Closed)   all t: Train – ts | t.on = t.on’ }