CONTROLLER = (near.ind -> down.command -> confirm ->CONTROLLER | out.ind -> up.command -> confirm -> CONTROLLER).
GATE = (down.command -> down -> confirm -> GATE | up.command -> up -> confirm -> GATE).
||CROSSING = (CONTROLLER || GATE).
TRAIN = (train.near -> near.ind -> enter.crossing -> leave.crossing -> out.ind -> TRAIN).
||SYSTEM = (TRAIN || CROSSING).
//SAfety Properties
property SAFETY_1 = (down -> enter.crossing -> SAFETY_1).
property SAFETY_3 = (leave.crossing -> up -> SAFETY_3).
||CHECK_1 = (SYSTEM || SAFETY_1).
||CHECK_3 = (SYSTEM || SAFETY_3).