R41 - woven-planet/opensafety-mbse GitHub Wiki

R41 / 1:1c

Lane Division marks zero or one Road Edge

Road Edge is marked by one Lane Division

---

On any given Road Segment, there will be two Lane Divisions that each mark a Road Edge. Since there are always two Road Edges, there must always be two such Lane Divisions in the Road Segment.

Formalization

Road Edge.(Lane division, Road segment) -> Lane Division.(ID, Road segment)