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 (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 (ack_ver = SLEEP & PREV(ack_ver = MOVE) & spec_dropping -> botMot = SEEK)
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 ((nonemove & spec_dropping & PREV(ack_hor != MOVE)) | (PREV(botMot = SEEK) & onlybotmoves & detect != spec_currentColor) -> botMot = SEEK)
G (nonemove & PREV(ack_hor = MOVE) & spec_dropping -> botMot = RETURN)
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 ((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 ((nextMoveMode = BWD) -> (Y(nextMoveMode = FWD) | Y(nextMoveMode = BWD)))
G (Y (nextMoveMode = TURN_LEFT_2) -> !(nextMoveMode = BWD))
G ( (Y(nextMoveMode = BWD)) -> (nextMoveMode != TURN_LEFT_1)) 
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 ((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 = BWD)) -> (spec_nextMoveMode != TURN_LEFT_1)) 
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((policy=SEEKING & obstacle = CLEAR & sideSense = CENTERED & (PREV(sideSense != CLOSE) & PREV(sideSense != FAR))) -> (steer=CENTER))
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((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=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((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 (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 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))))
