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 (((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 (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_speedButtonValidPressed = true & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL2)
G (spec_speedButtonValidPressed = true & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL3)
G (spec_speedButtonValidPressed = true & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL1)
G (spec_speedButtonValidPressed = false & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL1)
G (spec_speedButtonValidPressed = false & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL2)
G (spec_speedButtonValidPressed = false & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL3)
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 (spec_finished_cycle <-> ack_bot = SLEEP & PREV(spec_pausing = GO) & spec_stage = FROMANGLE & spec_pausing = GO)
G (ack_bot = SLEEP & PREV(spec_pausing = go) & spec_stage = FROMANGLE & spec_pausing = go -> spec_allsleep & next(spec_stage) = WAIT)
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL2)
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL3)
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL1)
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL1)
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL2)
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL3)
G (spec_dropping = next(spec_dropping) <-> verMot = SLEEP & !(PREV(botMot = RETURN) & ack_bot = SLEEP))
G (ack_ver = SLEEP & PREV(ack_ver = MOVE) & spec_dropping -> botMot = SEEK)
G (spec_dropping & detect = spec_currentColor & PREV(botMot != STOP) <-> horMot = MOVE)
G ((nonemove & spec_dropping) | (PREV(botMot = SEEK) & onlybotmoves & detect != spec_currentColor) -> botMot = SEEK)
G (spec_dropping & onlybotmoves & detect = spec_currentColor & PREV(botMot = SEEK) -> horMot = MOVE)
G(spec_prevBotMotReturn<->PREV(botMot = RETURN))
G ((nonemove & spec_dropping & PREV(ack_hor != MOVE)) | (PREV(botMot = SEEK) & onlybotmoves & detect != spec_currentColor) -> botMot = SEEK)
G (spec_dropping & onlybotmoves & detect = spec_currentColor & PREV(botMot = SEEK) <-> horMot = MOVE)
G (nonemove & PREV(ack_hor = MOVE) & spec_dropping -> botMot = RETURN)
G (spec_prevBotMotReturn<->PREV(botMot = RETURN))
G (spec_prevBotMotSeek<->PREV(botMot = SEEK))
G ((nonemove & spec_dropping & PREV(ack_hor != MOVE)) -> botMot = SEEK)
G (nonemove & spec_dropping & PREV(ack_hor != MOVE)-> botMot = SEEK)
G (nonemove & spec_dropping & PREV(ack_ver = MOVE)-> botMot = SEEK)
G (!spec_dropping & starting_pos = YES & PREV(botMot = RETURN) <-> reduce_num_of_cubes = REDUCE)
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 ((InputMoveMode = FWD & Y (InputMoveMode = TURN_LEFT_2)) -> (LeftMotor = CALIB_FWD & RightMotor = CALIB_FWD))
G ((InputMoveMode = FWD & Obstacle = CLEAR & Y (InputMoveMode != TURN_LEFT_2)) -> (LeftMotor = FWD & RightMotor = FWD))
G ((InputMoveMode = FWD & Button = FREE & Y (InputMoveMode = TURN_LEFT_2)) -> (LeftMotor = CALIB_FWD & RightMotor = CALIB_FWD))
G ((InputMoveMode = FWD & Obstacle = CLEAR & Button = FREE & Y (InputMoveMode != TURN_LEFT_2)) -> (LeftMotor = FWD & RightMotor = FWD))
G((Y(nextMoveMode = BWD) & (nextMoveMode = FWD)) <-> (LeftMotor = FWD & RightMotor = BWD))
G((Y(nextMoveMode = FWD) & (nextMoveMode = BWD)) <-> (LeftMotor = BWD & RightMotor = FWD))
G ((nextMoveMode = BWD) -> (Y(nextMoveMode = FWD) | Y(nextMoveMode = BWD)))
G (Y (nextMoveMode = TURN_LEFT_2) -> !(nextMoveMode = BWD))
G ((Y(nextMoveMode = FWD) & nextMoveMode = TURN_LEFT_1) <-> (LeftMotor = CALIB_TURN & RightMotor = CALIB_TURN))
G ( (Y(nextMoveMode = BWD)) -> (nextMoveMode != TURN_LEFT_1)) 
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(nextMoveMode = TURN_LEFT_1) -> (LeftMotor = FWD & RightMotor = TURN_FWD))
G (Y(nextMoveMode = TURN_LEFT_2) -> (LeftMotor = BWD & RightMotor = TURN_BWD))
G (!(Y(nextMoveMode = TURN_LEFT_1) | Y(nextMoveMode = TURN_LEFT_2)) -> !(LeftMotor = TURN_BWD | RightMotor = TURN_BWD | LeftMotor = TURN_FWD | RightMotor = TURN_FWD))
G(((Obstacle = BLOCKED) & !(Y(Y(spec_nextMoveMode = TURN_LEFT_2)))) -> (!(spec_nextMoveMode = FWD)))
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 ((spec_nextMoveMode = BWD) -> (Y(spec_nextMoveMode = FWD) | Y(spec_nextMoveMode = BWD)))
G (Y (spec_nextMoveMode = TURN_LEFT_2) -> !(spec_nextMoveMode = BWD))
G ((Y(spec_nextMoveMode = FWD) & spec_nextMoveMode = TURN_LEFT_1) <-> (LeftMotor = CALIB_TURN & RightMotor = CALIB_TURN))
G ( (Y(spec_nextMoveMode = BWD)) -> (spec_nextMoveMode != TURN_LEFT_1)) 
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 (Y(spec_nextMoveMode = TURN_LEFT_1) -> (LeftMotor = FWD & RightMotor = TURN_FWD))
G (Y(spec_nextMoveMode = TURN_LEFT_2) -> (LeftMotor = BWD & RightMotor = TURN_BWD))
G (!(Y(spec_nextMoveMode = TURN_LEFT_1) | Y(spec_nextMoveMode = TURN_LEFT_2)) -> !(LeftMotor = TURN_BWD | RightMotor = TURN_BWD | LeftMotor = TURN_FWD | RightMotor = TURN_FWD))
G ((Y(search = M0) & Noise = NOISE & Heading != next_head & Button != PRESSED) -> (search = M1))
G((Y(search = M1) & Heading = next_head) -> search = M0)
G((Y(search = M1) & Heading != next_head) -> search = M1)
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 ((turnState = T2 & Y(nextMoveMode = TURN_RIGHT)) <-> (LeftMotor = BWD & RightMotor = TURN_BWD))
G ((turnState = T2 & Y(nextMoveMode = TURN_LEFT)) <-> (LeftMotor = TURN_BWD & RightMotor = BWD))
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 & sideSense = CENTERED & (PREV(sideSense != CLOSE) & PREV(sideSense != FAR))) -> (steer=CENTER))
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=SEEKING & obstacle = CLEAR & PREV(obstacle = BLOCKED)) -> (steer=CENTER))
G((policy=SEEKING & obstacle = CLEAR & sideSense = CLOSE & PREV(obstacle = CLEAR)) -> (steer=EASY_LEFT))
G((policy=SEEKING & obstacle = CLEAR & sideSense = FAR & PREV(obstacle = CLEAR)) -> (steer=EASY_RIGHT))
G((policy=SEEKING & obstacle = CLEAR & sideSense = CENTERED & (PREV(sideSense = CENTERED)) & PREV(obstacle = CLEAR)) -> (steer=CENTER))
G((policy = SEEKING & obstacle = CLEAR & PREV(sideSense = FAR) & sideSense = CENTERED & PREV(obstacle = CLEAR)) -> (steer=EASY_LEFT))
G((policy = SEEKING & obstacle = CLEAR & PREV(sideSense = CLOSE) & sideSense = CENTERED & PREV(obstacle = CLEAR)) -> (steer=EASY_RIGHT))
G((policy=MEASURING & obstacle = CLEAR & sideSense = PARALLEL_PARKING & PREV(sideSense = PARALLEL_PARKING)) -> (steer=CENTER))
G((policy=MEASURING & obstacle = CLEAR & sideSense = PARALLEL_PARKING & PREV(sideSense = CLOSE_PARKING)) -> (steer=EASY_RIGHT))
G((policy=MEASURING & obstacle = CLEAR & sideSense = PARALLEL_PARKING & PREV(sideSense = PERPENDICULAR)) -> (steer=EASY_LEFT))
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=SEEKING & obstacle = CLEAR & sideSense = CENTERED & (PREV(sideSense = CENTERED))) -> (steer=CENTER))
G((spec_policy = SEEKING & obstacle = CLEAR & PREV(sideSense = FAR) & sideSense = CENTERED) -> (steer=EASY_LEFT))
G((spec_policy = SEEKING & obstacle = CLEAR & PREV(sideSense = CLOSE) & sideSense = CENTERED) -> (steer=EASY_RIGHT))
G((spec_policy=MEASURING & obstacle = CLEAR & sideSense = PARALLEL_PARKING & PREV(sideSense = PARALLEL_PARKING)) -> (steer=CENTER))
G((spec_policy=MEASURING & obstacle = CLEAR & sideSense = PARALLEL_PARKING & PREV(sideSense = CLOSE_PARKING)) -> (steer=EASY_RIGHT))
G((spec_policy=MEASURING & obstacle = CLEAR & sideSense = PARALLEL_PARKING & PREV(sideSense = PERPENDICULAR)) -> (steer=EASY_LEFT))
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=SEEKING & obstacle = CLEAR & PREV(obstacle = BLOCKED)) -> (steer=CENTER))
G((spec_policy=SEEKING & obstacle = CLEAR & sideSense = CLOSE & PREV(obstacle = CLEAR)) -> (steer=EASY_LEFT))
G((spec_policy=SEEKING & obstacle = CLEAR & sideSense = FAR & PREV(obstacle = CLEAR)) -> (steer=EASY_RIGHT))
G((spec_policy=SEEKING & obstacle = CLEAR & sideSense = CENTERED & (PREV(sideSense = CENTERED)) & PREV(obstacle = CLEAR)) -> (steer=CENTER))
G((spec_policy = SEEKING & obstacle = CLEAR & PREV(sideSense = FAR) & sideSense = CENTERED & PREV(obstacle = CLEAR)) -> (steer=EASY_LEFT))
G((spec_policy = SEEKING & obstacle = CLEAR & PREV(sideSense = CLOSE) & sideSense = CENTERED & PREV(obstacle = CLEAR)) -> (steer=EASY_RIGHT))
G((spec_policy=SEEKING & obstacle = CLEAR & PREV(obstacle = BLOCKED) & command=AUTO) -> (steer=CENTER))
G((spec_policy=SEEKING & obstacle = CLEAR & sideSense = CLOSE & command=AUTO & PREV(obstacle = CLEAR)) -> (steer=EASY_LEFT))
G((spec_policy=SEEKING & obstacle = CLEAR & sideSense = FAR & command=AUTO & PREV(obstacle = CLEAR)) -> (steer=EASY_RIGHT))
G((spec_policy=SEEKING & obstacle = CLEAR & sideSense = CENTERED & (PREV(sideSense = CENTERED)) & command=AUTO & PREV(obstacle = CLEAR)) -> (steer=CENTER))
G((spec_policy = SEEKING & obstacle = CLEAR & PREV(sideSense = FAR) & sideSense = CENTERED & command=AUTO & PREV(obstacle = CLEAR)) -> (steer=EASY_LEFT))
G((spec_policy = SEEKING & obstacle = CLEAR & PREV(sideSense = CLOSE) & sideSense = CENTERED & command=AUTO & PREV(obstacle = CLEAR)) -> (steer=EASY_RIGHT))
G((spec_policy=MEASURING & obstacle = CLEAR & sideSense = PARALLEL_PARKING & PREV(sideSense = PARALLEL_PARKING) & command=AUTO) -> (steer=CENTER))
G((spec_policy=MEASURING & obstacle = CLEAR & sideSense = PARALLEL_PARKING & PREV(sideSense = CLOSE_PARKING) & command=AUTO) -> (steer=EASY_RIGHT))
G((spec_policy=MEASURING & obstacle = CLEAR & sideSense = PARALLEL_PARKING & PREV(sideSense = PERPENDICULAR) & command=AUTO) -> (steer=EASY_LEFT))
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((obstacle = BLOCKED & carStatus = PARALLEL & (PREV(sensorMot = BWD) & !movingFwd) ) -> (sensorMot = BWD))
G((obstacle = BLOCKED & (carStatus = PARALLEL | carStatus = ALIGN_BEFORE_PARKING) & (PREV(sensorMot = BWD) & !movingFwd) ) -> (sensorMot = BWD))
G((carStatus != BYPASSING & PREV(obstacle = CLEAR) & obstacle = BLOCKED ) -> (spec_obstacleCounter = 0))
G((obstacle = BLOCKED & carStatus != BYPASSING & (PREV(sensorMot = BWD) & !movingFwd) ) -> (sensorMot = BWD))
G((obstacle = BLOCKED & carStatus = BYPASSING & (spec_counter = 1 | spec_counter = 2 | spec_counter = 11) & (PREV(sensorMot = BWD) & !movingFwd) ) -> (sensorMot = BWD))
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 ((atEmgState & PREV(willEnterStation))|(atStation & readyToEmgBeep & atEmgState)) <-> emgBeepProcessReq
G (PREV(!techGuyInAction) & techGuyInAction <-> startTechnicalJob )
G (onlyDownCalls&PREV(stayInPlace))->(goingDown|atEmergencyFloor)
G (onlyUpCalls&PREV(stayInPlace))->(goingUp|atEmergencyFloor)
G(fullyOpenedStateAtDesignatedFloor&(noSeconds|seconds3|seconds5)&!memEmergency&sabbathMode&PREV(keepDoorsState))->(keepDoorsState)
G (onlyDownCalls&PREV(stayInPlace))->(!goingUp)
G (onlyUpCalls&PREV(stayInPlace))->(!goingDown)
G (PREV(sideSense <= 1)) -> (!right)
G (driveMotor = BWD) -> PREV(senseMotor = REVERSE)
G backSense = 0 & PREV(senseMotor = REVERSE) -> driveMotor != BWD
G reversing -> PREV(senseMotor = REVERSE) & velocity = 1
G (mode = SCANNING) -> PREV(mode != PARKED)
G (mode = SCANNING) -> PREV(mode != PARKING)
G (mode = PARKING) -> PREV(mode != SEARCHING)
G (mode = PARKING) -> PREV(mode != PARKED)
G (mode = PARKING) -> PREV(mode != EXIT)
G (mode = PARKED) -> PREV(mode != SEARCHING)
G (mode = PARKED) -> PREV(mode != SCANNING)
G (mode = PARKED) -> PREV(mode != EXIT)
G (mode = EXIT) -> PREV(mode != SEARCHING)
G (mode = EXIT) -> PREV(mode != SCANNING)
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
G backSense = 0 & PREV(senseMotor = BACK) -> driveMotor = FWD
G reversing -> PREV(senseMotor = BACK) & velocity = 1
G (PREV(mode = SCANNING) & status = PARALLEL) -> (mode = PARKING)
G driveMotor = BWD -> backSense > 0 & PREV(senseMotor = BACK)
G (PREV(senseMotor = BACK) & backSense <= 1) -> (driveMotor != BWD)
G (PREV(senseMotor = SIDE) & sideSense <= 1) -> (steeringMotor = STRAIGHT)
G (driveMotor = FWD) -> (PREV(senseMotor = SIDE))
G(driveMotor = BWD) -> ((PREV(senseMotor = SIDE)) & (PREV(backSense > 0 & stopping) & PREV(PREV(senseMotor = BACK))))
