G (speedButton = PRESS & PREV(speedButton = RELEASE) <-> spec_speedButtonValidPressed)
G (haltButton = PRESS & PREV(haltButton = RELEASE) <-> spec_pauseButtonValidPressed)
G (haltButton = PRESS & PREV(haltButton = RELEASE) <-> spec_haltButtonValidPressed = true)
G (spec_finished_cycle <-> ack_bot = SLEEP & PREV(spec_pausing = go) & spec_stage = FROMANGLE & spec_pausing = go)
G (speedButton = PRESS & PREV(speedButton = RELEASE) <-> spec_speedButtonValidPressed = true)
G (spec_finished_cycle <-> ack_bot = SLEEP & PREV(spec_pausing = GO) & spec_stage = FROMANGLE & spec_pausing = GO)
G (spec_dropping & detect = spec_currentColor & PREV(botMot != STOP) <-> horMot = MOVE)
G(spec_prevBotMotReturn<->PREV(botMot = RETURN))
G (spec_dropping & onlybotmoves & detect = spec_currentColor & PREV(botMot = SEEK) <-> horMot = MOVE)
G (spec_prevBotMotReturn<->PREV(botMot = RETURN))
G (spec_prevBotMotSeek<->PREV(botMot = SEEK))
G (!spec_dropping & starting_pos = YES & PREV(botMot = RETURN) <-> reduce_num_of_cubes = REDUCE)
G((Y(nextMoveMode = BWD) & (nextMoveMode = FWD)) <-> (LeftMotor = FWD & RightMotor = BWD))
G((Y(nextMoveMode = FWD) & (nextMoveMode = BWD)) <-> (LeftMotor = BWD & RightMotor = FWD))
G ((Y(nextMoveMode = FWD) & nextMoveMode = TURN_LEFT_1) <-> (LeftMotor = CALIB_TURN & RightMotor = CALIB_TURN))
G ((Y(nextMoveMode = FWD) & Y(Y(nextMoveMode = TURN_LEFT_2))) <-> (LeftMotor = CALIB_FWD & RightMotor = CALIB_FWD))
G (Y(nextMoveMode = TURN_LEFT_1) <-> nextMoveMode = TURN_LEFT_2)
G((Y(spec_nextMoveMode = BWD) & (spec_nextMoveMode = FWD)) <-> (LeftMotor = FWD & RightMotor = BWD))
G((Y(spec_nextMoveMode = FWD) & (spec_nextMoveMode = BWD)) <-> (LeftMotor = BWD & RightMotor = FWD))
G ((Y(spec_nextMoveMode = FWD) & spec_nextMoveMode = TURN_LEFT_1) <-> (LeftMotor = CALIB_TURN & RightMotor = CALIB_TURN))
G ((Y(spec_nextMoveMode = FWD) & Y(Y(spec_nextMoveMode = TURN_LEFT_2))) <-> (LeftMotor = CALIB_FWD & RightMotor = CALIB_FWD))
G (Y(spec_nextMoveMode = TURN_LEFT_1) <-> spec_nextMoveMode = TURN_LEFT_2)
G ((turnState = T2 & Y(nextMoveMode = TURN_RIGHT)) <-> (LeftMotor = BWD & RightMotor = TURN_BWD))
G ((turnState = T2 & Y(nextMoveMode = TURN_LEFT)) <-> (LeftMotor = TURN_BWD & RightMotor = BWD))
G ((atEmgState & PREV(willEnterStation))|(atStation & readyToEmgBeep & atEmgState)) <-> emgBeepProcessReq
G (PREV(!techGuyInAction) & techGuyInAction <-> startTechnicalJob )
