G (((ack_ver_hor = SLEEP & spec_stage = DROP) | ((ack_bot = MOVE | (ack_bot = SLEEP & PREV(spec_pausing = pause))) & spec_stage = FROMANGLE)) & spec_pausing = go -> botMot = INITPOS & next(spec_stage) = FROMANGLE)
G (((ack_ver_hor = SLEEP & spec_stage = DROP) | ((ack_bot = MOVE | (ack_bot = SLEEP & PREV(spec_pausing = PAUSE))) & spec_stage = FROMANGLE)) & spec_pausing = GO -> botMot = INITPOS & next(spec_stage) = FROMANGLE)
G (ack_bot = SLEEP & PREV(spec_pausing = go) & spec_stage = FROMANGLE & spec_pausing = go -> spec_allsleep & next(spec_stage) = WAIT)
G (spec_dropping = next(spec_dropping) <-> verMot = SLEEP & !(PREV(botMot = RETURN) & ack_bot = SLEEP))
G ((spec_mode=MANUAL) -> ((!bluetoothDrivingCmd) -> ( (PREV(spec_manualCmd=STP) -> spec_manualCmd=STP) & (PREV(spec_manualCmd=FWD) -> spec_manualCmd=FWD) & (PREV(spec_manualCmd=BWD) -> spec_manualCmd=BWD) & (PREV(spec_manualCmd=TURN_LEFT) -> spec_manualCmd=TURN_LEFT) & (PREV(spec_manualCmd=TURN_RIGHT) -> spec_manualCmd=TURN_RIGHT) )))
G (((spec_nextMoveMode = TURN_RIGHT | spec_nextMoveMode = TURN_LEFT) & Y(spec_nextMoveMode = FWD) & spec_turnState = T0) -> next(spec_turnState) = T1)
G ((spec_turnState = T3 & next(spec_turnState = T0) & Y(Y(spec_nextMoveMode = TURN_RIGHT))) <-> (LeftMotor = CALIB_FWD_RIGHT & RightMotor = CALIB_FWD_RIGHT))
G ((spec_turnState = T3 & next(spec_turnState = T0) & Y(Y(spec_nextMoveMode = TURN_LEFT))) <-> (LeftMotor = CALIB_FWD_LEFT & RightMotor = CALIB_FWD_LEFT))
G ((Button = PRESSED & Y(search = M0)) -> (next(next_head) = Heading))
G ((Button = FREE | Y(search = M1)) -> (next(next_head) = next_head))
G((next(Obstacle = BLOCKED) & !((Y(spec_nextMoveMode = TURN_LEFT_2)))) -> next(!(spec_nextMoveMode = FWD)))
G (((spec_nextMoveMode = FWD) & (Y(spec_nextMoveMode = TURN_LEFT_2))) <-> next(LeftMotor = CALIB_FWD & RightMotor = CALIB_FWD))
G ((spec_nextMoveMode = TURN_LEFT & Y(spec_nextMoveMode = FWD) & spec_turnState = T0) -> next(spec_turnState) = T1)
G (((nextMoveMode = TURN_RIGHT | nextMoveMode = TURN_LEFT) & Y(nextMoveMode = FWD) & turnState = T0) -> next(turnState) = T1)
G (((((spec_policy = MEASURING)|(spec_policy=SEEKING & PREV(spec_policy=MEASURING)))) & (obstacle = CLEAR) &(parkResult =PARALLEL)) -> (next(spec_policy) = PARKING_0) & (throttle = STOP) & (parkCommand = STOP) & steer = RIGHT)
G((policy = SEEKING & obstacle = CLEAR & PREV(sideSense = FAR) & sideSense = CENTERED) -> (steer=EASY_LEFT & next(steer)=CENTER))
G((policy = SEEKING & obstacle = CLEAR & PREV(sideSense = CLOSE) & sideSense = CENTERED) -> (steer=EASY_RIGHT & next(steer)=CENTER))
G (((((policy = MEASURING & sideSense = PARALLEL_PARKING)|(policy=SEEKING & PREV(sideSense = PARALLEL_PARKING) & PREV(policy=MEASURING)))) & (obstacle = CLEAR) &(parkResult =PARALLEL)) -> (next(policy) = PARKING_0) & (throttle = BLOCKING_FWD) & (parkCommand = STOP) )
G (((((policy = MEASURING & sideSense = PARALLEL_PARKING)|(policy=SEEKING & PREV(sideSense = PARALLEL_PARKING) & PREV(policy=MEASURING)))) & (obstacle = CLEAR) &(parkResult =PARALLEL)) -> (next(policy) = PARKING_0) & (throttle = STOP) & (parkCommand = STOP) )
G (((((spec_policy = MEASURING & sideSense = PARALLEL_PARKING)|(spec_policy=SEEKING & PREV(sideSense = PARALLEL_PARKING) & PREV(spec_policy=MEASURING)))) & (obstacle = CLEAR) &(parkResult =PARALLEL)) -> (next(spec_policy) = PARKING_0) & (throttle = STOP) & (parkCommand = STOP) )
G ((((spec_policy = MEASURING & sideSense = PARALLEL_PARKING)|(spec_policy=SEEKING & PREV(sideSense = PARALLEL_PARKING) & PREV(spec_policy=MEASURING))) & (obstacle = CLEAR) &(parkResult =PARALLEL)) -> (next(spec_policy) = PARKING_0) & (throttle = STOP) & (parkCommand = STOP) )
G (((((spec_policy = MEASURING & sideSense = PARALLEL_PARKING)|(spec_policy=SEEKING & PREV(sideSense = PARALLEL_PARKING) & PREV(spec_policy=MEASURING)))) & (obstacle = CLEAR) &(parkResult =PARALLEL) & command=AUTO) -> (next(spec_policy) = PARKING_0) & (throttle = STOP) & (parkCommand = STOP) )
G(((carStatus = SEEKING_FOR_PS | carStatus = MEASURE_PARKING) & spec_obstacleCounter = 2 & obstacle = BLOCKED & PREV(obstacle = BLOCKED) ) -> (Stop & next(carStatus = BYPASSING) & next(spec_counter = 0) ) )
G mode = PARKING & status = PARALLEL & backSense > 2 -> PREV(senseMotor = BACK) & driveMotor = BWD & next(mode) = PARKING & steeringMotor = HARD_RIGHT
G mode = PARKING & status = PARALLEL & backSense <= 2 & backSense > 1 -> PREV(senseMotor = BACK) & driveMotor = BWD & next(mode) = PARKING & steeringMotor = HARD_LEFT
G mode = PARKING & status = PARALLEL & backSense <= 1 -> PREV(senseMotor = BACK) & driveMotor = STOP & next(mode) = PARKED & steeringMotor = STRAIGHT
