A safety condition
	• Every segment has at most one train on it and its overlapping segments – Could check by theorem proving…or by counterexample checking cond Safety {   all s | sole(s + s.overlaps).~on }