G (spec_dropping = next(spec_dropping) <-> verMot = SLEEP & horMot = SLEEP)
G (edge = YES <-> direction != next(direction))
G (spec_dropping = next(spec_dropping) <-> verMot = SLEEP )
G (spec_dropping = next(spec_dropping) <-> verMot = SLEEP & !(spec_prevBotMotReturn & nonemove))
G (spec_dropping = next(spec_dropping) <-> verMot = SLEEP & !(spec_prevBotMotReturn & ack_bot = SLEEP))
G(((spec_nextMoveMode = BWD) & next(spec_nextMoveMode = FWD)) <-> next(LeftMotor = FWD & RightMotor = BWD))
G(((spec_nextMoveMode = FWD) & next(spec_nextMoveMode = BWD)) <-> next(LeftMotor = BWD & RightMotor = FWD))
G ((spec_turnState = T0 & next(spec_turnState) = T1 & spec_nextMoveMode = TURN_RIGHT) <-> (LeftMotor = CALIB_TURN_RIGHT & RightMotor = CALIB_TURN_RIGHT))
G ((spec_turnState = T0 & next(spec_turnState) = T1 & spec_nextMoveMode = TURN_LEFT) <-> (LeftMotor = CALIB_TURN_LEFT & RightMotor = CALIB_TURN_LEFT))
G ((next(spec_turnState) = T2) <-> (LeftMotor = FWD & RightMotor = TURN_FWD))
G ((spec_nextMoveMode = TURN_LEFT_1) <-> next(spec_nextMoveMode = TURN_LEFT_2))
G (((spec_nextMoveMode = FWD) & next(spec_nextMoveMode = TURN_LEFT_1)) <-> next(LeftMotor = CALIB_TURN & RightMotor = CALIB_TURN))
G ((spec_turnState = T0 & next(spec_turnState) = T1) <-> (LeftMotor = CALIB_TURN & RightMotor = CALIB_TURN))
G (next(spec_turnState) = T2 <-> (LeftMotor = FWD & RightMotor = TURN_FWD))
G ((spec_turnState = T3 & next(spec_turnState = T0)) <-> (LeftMotor = CALIB_FWD & RightMotor = CALIB_FWD))
G(((nextMoveMode = BWD) & next(nextMoveMode = FWD)) <-> next(LeftMotor = FWD & RightMotor = BWD))
G(((nextMoveMode = FWD) & next(nextMoveMode = BWD)) <-> next(LeftMotor = BWD & RightMotor = FWD))
G ((turnState = T0 & next(turnState) = T1) <-> (LeftMotor = CALIB_TURN & RightMotor = CALIB_TURN))
G ((next(turnState) = T2 & nextMoveMode = TURN_RIGHT) <-> (LeftMotor = FWD & RightMotor = TURN_FWD))
G ((next(turnState) = T2 & nextMoveMode = TURN_LEFT) <-> (LeftMotor = TURN_FWD & RightMotor = FWD))
G ((turnState = T3 & next(turnState = T0)) <-> (LeftMotor = CALIB_FWD & RightMotor = CALIB_FWD))
G !techGuyInAction & next(techGuyInAction) <-> next(startTechnicalJob)
G(valid_parking_spot <-> next(mode = PARKED))
G(mode = PARKING & valid_parking_spot) <-> (next(mode) = PARKED)
G (status = PARALLEL & mode = PARKING & sideSense <= 1 & steeringMotor = STRAIGHT & driveMotor = STOP) <-> (next(mode) = PARKED)
G (mode = PARKING & stopping) <-> (next(mode) = PARKED)
G (manual = true) <-> (next(mode) = MANUAL)
