G (verMot = SLEEP -> spec_currentColor = next(spec_currentColor))
G (verMot = MOVE -> color = next(spec_currentColor))
G (spec_speedButtonValidPressed & motSpeed = LEVEL1 -> next(motSpeed = LEVEL2))
G (spec_speedButtonValidPressed & motSpeed = LEVEL2 -> next(motSpeed = LEVEL3))
G (spec_speedButtonValidPressed & motSpeed = LEVEL3 -> next(motSpeed = LEVEL1))
G (!spec_speedButtonValidPressed -> motSpeed = next(motSpeed))
G ((spec_pauseButtonValidPressed & spec_pausing = GO) | (!spec_pauseButtonValidPressed & spec_pausing = PAUSE) -> next(spec_pausing) = PAUSE)
G ((!spec_pauseButtonValidPressed & spec_pausing = GO) | (spec_pauseButtonValidPressed & spec_pausing = PAUSE) -> next(spec_pausing) = GO)
G(!spec_waiting_ack_ver_mot & verMot!=MOVE -> next(!spec_waiting_ack_ver_mot))
G (!spec_waiting_ack_ver_mot & verMot=MOVE -> next(spec_waiting_ack_ver_mot))
G (spec_waiting_ack_ver_mot & ack_ver=SLEEP -> next(!spec_waiting_ack_ver_mot))
G (spec_waiting_ack_ver_mot & ack_ver!=SLEEP -> next(spec_waiting_ack_ver_mot))
G(!spec_waiting_ack_hor_mot & horMot!=MOVE -> next(!spec_waiting_ack_hor_mot))
G (!spec_waiting_ack_hor_mot & horMot=MOVE -> next(spec_waiting_ack_hor_mot))
G (spec_waiting_ack_hor_mot & ack_hor=SLEEP -> next(!spec_waiting_ack_hor_mot))
G (spec_waiting_ack_hor_mot & ack_hor!=SLEEP -> next(spec_waiting_ack_hor_mot))
G ((spec_haltButtonValidPressed = true & spec_pausing = go) | (spec_haltButtonValidPressed = false & spec_pausing = pause) -> next(spec_pausing) = pause)
G ((spec_haltButtonValidPressed = false & spec_pausing = go) | (spec_haltButtonValidPressed = true & spec_pausing = pause) -> next(spec_pausing) = go)
G (spec_pausing = pause | ack_ver_hor = MOVE -> spec_allsleep = true & next(spec_stage) = spec_stage)
G (spec_stage != WAIT -> next(spec_currentColor) = spec_currentColor)
G ((color = BLACK | num_of_cubes = ZERO) & spec_stage = WAIT -> spec_allsleep = true & next(spec_stage) = WAIT)
G (color != BLACK & num_of_cubes != ZERO & spec_stage = WAIT & spec_pausing = go -> verMot = MOVE & color = next(spec_currentColor) & next(spec_stage) = KICK)
G (ack_ver_hor = SLEEP & spec_stage = KICK & spec_pausing = go -> botMot = RIGHT & next(spec_stage) = TOANGLERIGHT)
G (atEdge != EDGE & spec_stage = TOANGLERIGHT & detect != spec_currentColor & spec_pausing = go -> botMot = RIGHT & next(spec_stage) = TOANGLERIGHT)
G (atEdge = EDGE & spec_stage = TOANGLERIGHT & spec_pausing = go & detect != spec_currentColor -> botMot = LEFT & next(spec_stage) = TOANGLELEFT)
G (spec_stage = TOANGLELEFT & spec_pausing = go & detect != spec_currentColor -> botMot = LEFT & next(spec_stage) = TOANGLELEFT)
G ((spec_stage = TOANGLERIGHT | spec_stage = TOANGLELEFT) & spec_pausing = go & detect = spec_currentColor -> verMot = SLEEP & horMot = MOVE & botMot = STOP & next(spec_stage) = DROP )
G (spec_finished_cycle -> spec_allsleep = true & next(spec_stage) = WAIT)
G ((spec_haltButtonValidPressed = true & spec_pausing = GO) | (spec_haltButtonValidPressed = false & spec_pausing = PAUSE) -> next(spec_pausing) = PAUSE)
G ((spec_haltButtonValidPressed = false & spec_pausing = GO) | (spec_haltButtonValidPressed = true & spec_pausing = PAUSE) -> next(spec_pausing) = GO)
G (spec_pausing = PAUSE | ack_ver_hor = MOVE -> spec_allsleep = true & next(spec_stage) = spec_stage)
G (color != BLACK & num_of_cubes != ZERO & spec_stage = WAIT & spec_pausing = GO -> verMot = MOVE & color = next(spec_currentColor) & next(spec_stage) = KICK)
G (ack_ver_hor = SLEEP & spec_stage = KICK & spec_pausing = GO -> botMot = RIGHT & next(spec_stage) = TOANGLERIGHT)
G ((spec_stage = TOANGLERIGHT | spec_stage = TOANGLELEFT) & spec_pausing = GO & detect = spec_currentColor -> verMot = SLEEP & horMot = MOVE & botMot = STOP & next(spec_stage) = DROP )
G (spec_stage != WAIT -> next(botMotColor) = botMotColor)
G (color = BLACK & spec_stage = WAIT -> spec_allsleep = true & next(spec_stage) = WAIT)
G (color != BLACK & spec_stage = WAIT & spec_pausing = go -> verMot = MOVE & color = next(botMotColor) & next(spec_stage) = KICK)
G (ack_bot = MOVE & spec_stage = TOANGLEPLACE & spec_pausing = go -> botMot = PLACE & next(spec_stage) = TOANGLERIGHT)
G (ack_bot = SLEEP & spec_stage = TOANGLEPLACE & spec_pausing = go -> horMot = MOVE & next(spec_stage) = DROP)
G (atEdge != EDGE & spec_stage = TOANGLERIGHT & detect != botMotColor & spec_pausing = go -> botMot = RIGHT & next(spec_stage) = TOANGLERIGHT)
G (atEdge = EDGE & spec_stage = TOANGLERIGHT & spec_pausing = go & detect != botMotColor -> botMot = LEFT & next(spec_stage) = TOANGLELEFT)
G (spec_stage = TOANGLELEFT & spec_pausing = go & detect != botMotColor -> botMot = LEFT & next(spec_stage) = TOANGLELEFT)
G ((spec_stage = TOANGLERIGHT | spec_stage = TOANGLELEFT) & spec_pausing = go & detect = botMotColor -> horMot = MOVE & next(spec_stage) = DROP)
G (verMot = SLEEP -> spec_currentColor = next(spec_currentColor) & spec_dropping = next(spec_dropping))
G (color != BLACK & !spec_dropping -> verMot = MOVE & next(spec_currentColor) = color & next(spec_dropping))
G (color != BLACK & !spec_dropping -> verMot = MOVE & next(spec_currentColor) = color)
G ((spec_mode=AUTO & isReady) -> ((spec_blockedState=S0 & ((!(frontDistSense=BLOCKED) & !(frontDistSense=CLEAR)) | (frontDistSense=CLEAR)) & next(spec_blockedState=S0)) | (spec_blockedState=S0 & (frontDistSense=BLOCKED & !turningOp & !(frontDistSense=CLEAR)) & next(spec_blockedState=S1)) | (spec_blockedState=S0 & (frontDistSense=BLOCKED & turningOp & !(frontDistSense=CLEAR)) & next(spec_blockedState=S2)) | (spec_blockedState=S1 & next(spec_blockedState=S1)) | (spec_blockedState=S2 & (frontDistSense=CLEAR) & next(spec_blockedState=S0)) | (spec_blockedState=S2 & (!turningOp & !(frontDistSense=CLEAR)) & next(spec_blockedState=S1)) | (spec_blockedState=S2 & (turningOp & !(frontDistSense=CLEAR)) & next(spec_blockedState=S2))))
G ((balancer=FWD) -> next(!(balancer=TURN_RIGHT | balancer=TURN_LEFT)))
G ((distSense=BLOCKED & balancer=STP & isReady) -> next(!(balancer=STP)))
G ((bluetoothCmd=AUTO & isReady) -> ((spec_blockedState=S0 & ((!(frontDistSense=BLOCKED) & !(frontDistSense=CLEAR)) | (frontDistSense=CLEAR)) & next(spec_blockedState=S0)) | (spec_blockedState=S0 & (frontDistSense=BLOCKED & !turningOp & !(frontDistSense=CLEAR)) & next(spec_blockedState=S1)) | (spec_blockedState=S0 & (frontDistSense=BLOCKED & turningOp & !(frontDistSense=CLEAR)) & next(spec_blockedState=S2)) | (spec_blockedState=S1 & next(spec_blockedState=S1)) | (spec_blockedState=S2 & (frontDistSense=CLEAR) & next(spec_blockedState=S0)) | (spec_blockedState=S2 & (!turningOp & !(frontDistSense=CLEAR)) & next(spec_blockedState=S1)) | (spec_blockedState=S2 & (turningOp & !(frontDistSense=CLEAR)) & next(spec_blockedState=S2))))
G (next(spec_nextMoveMode = BWD) -> ((spec_nextMoveMode = FWD) | (spec_nextMoveMode = BWD)))
G (spec_nextMoveMode = BWD -> next((spec_nextMoveMode = FWD) | (spec_nextMoveMode = BWD)))
G (next(spec_nextMoveMode = TURN_RIGHT) -> (spec_nextMoveMode = FWD) | (spec_nextMoveMode = TURN_RIGHT))
G (next(spec_nextMoveMode = TURN_LEFT) -> (spec_nextMoveMode = FWD) | (spec_nextMoveMode = TURN_LEFT))
G((spec_specState = Q0 & spec_nextMoveMode = FWD & next(spec_nextMoveMode = BWD)) -> next(spec_specState = Q1))
G((spec_specState = Q1 & spec_nextMoveMode = BWD & next(spec_nextMoveMode = FWD)) -> next(spec_specState = Q2))
G((spec_specState = Q1 & next(spec_nextMoveMode = BWD)) -> next(spec_specState = Q1))
G((spec_specState = Q2 & next(spec_nextMoveMode = FWD)) -> next(spec_specState) = Q2)
G((spec_nextMoveMode = TURN_RIGHT | spec_nextMoveMode = TURN_LEFT) -> next(spec_specState = Q0))
G (next(spec_turnState) = T0 -> (spec_turnState = T0 | spec_turnState = T3))
G ((spec_turnState = T0 & !(spec_nextMoveMode = TURN_RIGHT | spec_nextMoveMode = TURN_LEFT)) -> next(spec_turnState) = T0)
G (spec_turnState = T1 -> (next(spec_turnState) = T2 & (spec_nextMoveMode = TURN_RIGHT | spec_nextMoveMode = TURN_LEFT)))
G ((spec_turnState = T2 & (spec_nextMoveMode = TURN_RIGHT | spec_nextMoveMode = TURN_LEFT)) -> next(spec_turnState) = T1)
G ((spec_turnState = T2 & spec_nextMoveMode = FWD) -> next(spec_turnState) = T3)
G ((spec_turnState = T3) -> next(spec_turnState = T0))
G((state = Q0 & nextMoveMode = FWD & next(nextMoveMode = BWD)) -> next(state = Q1))
G((state = Q1 & nextMoveMode = BWD & next(nextMoveMode = FWD)) -> next(state = Q2))
G((state = Q2 & nextMoveMode = FWD & next(nextMoveMode = BWD)) -> next(state = Q3))
G((state = Q1 & next(nextMoveMode = BWD)) -> (next(state = Q1)))
G((state = Q2 & next(nextMoveMode = FWD)) -> (next(state = Q2)))
G(( (nextMoveMode = TURN_LEFT_1) | (nextMoveMode = TURN_LEFT_1)) -> next(state = Q0))
G((spec_state = Q0 & spec_nextMoveMode = FWD & next(spec_nextMoveMode = BWD)) -> next(spec_state = Q1))
G((spec_state = Q1 & spec_nextMoveMode = BWD & next(spec_nextMoveMode = FWD)) -> next(spec_state = Q2))
G((spec_state = Q2 & spec_nextMoveMode = FWD & next(spec_nextMoveMode = BWD)) -> next(spec_state = Q3))
G((spec_state = Q1 & next(spec_nextMoveMode = BWD)) -> (next(spec_state = Q1)))
G((spec_state = Q2 & next(spec_nextMoveMode = FWD)) -> (next(spec_state = Q2)))
G(( (spec_nextMoveMode = TURN_LEFT_1) | (spec_nextMoveMode = TURN_LEFT_1)) -> next(spec_state = Q0))
G ((spec_search = M0 & spec_nextMoveMode = FWD & Noise = NOISE & Heading = LOST) -> (next(spec_search = M1) & next(spec_nextMoveMode = FWD)))
G((spec_search = M1) -> next(spec_search = M2) & next(spec_nextMoveMode = TURN_LEFT_1))
G((spec_search = M2 & Heading = LOST) -> (next(spec_search = M2) & (spec_nextMoveMode = TURN_LEFT_1 | spec_nextMoveMode = TURN_LEFT_2)))
G((spec_search = M2 & Heading = ONTRACK) -> next(spec_search = M0))
G(((spec_nextMoveMode = TURN_LEFT_1) | (spec_nextMoveMode = TURN_LEFT_2)) -> next(spec_state = Q0))
G ((spec_nextMoveMode = TURN_LEFT_1) -> next(LeftMotor = FWD & RightMotor = TURN_FWD))
G ((spec_nextMoveMode = TURN_LEFT_2) -> next(LeftMotor = BWD & RightMotor = TURN_BWD))
G (!((spec_nextMoveMode = TURN_LEFT_1) | (spec_nextMoveMode = TURN_LEFT_2)) -> next(!(LeftMotor = TURN_BWD | RightMotor = TURN_BWD | LeftMotor = TURN_FWD | RightMotor = TURN_FWD)))
G ( ((spec_nextMoveMode = BWD)) -> next(spec_nextMoveMode != TURN_LEFT_1))
G(spec_nextMoveMode = TURN_LEFT -> next(spec_specState = Q0))
G ((Button = PRESSED) -> next(spec_nextHead = Heading))
G ((Button = FREE) -> (next(spec_nextHead) = spec_nextHead))
G ((spec_turnState = T0 & !(spec_nextMoveMode = TURN_LEFT)) -> next(spec_turnState) = T0)
G (spec_turnState = T1 -> (next(spec_turnState) = T2 & spec_nextMoveMode = TURN_LEFT))
G ((spec_turnState = T2 & spec_nextMoveMode = TURN_LEFT) -> next(spec_turnState) = T1)
G ((spec_turnState = T3 & spec_nextMoveMode = FWD) -> next(spec_turnState = T0))
G ((spec_turnState = T3 & spec_nextMoveMode != FWD) -> next(spec_turnState = T2))
G (next(nextMoveMode = BWD) -> ((nextMoveMode = FWD) | (nextMoveMode = BWD)))
G (nextMoveMode = BWD -> next((nextMoveMode = FWD) | (nextMoveMode = BWD)))
G (next(nextMoveMode = TURN_RIGHT) -> (nextMoveMode = FWD) | (nextMoveMode = TURN_RIGHT))
G (next(nextMoveMode = TURN_LEFT) -> (nextMoveMode = FWD) | (nextMoveMode = TURN_LEFT))
G((specState = Q0 & nextMoveMode = FWD & next(nextMoveMode = BWD)) -> next(specState = Q1))
G((specState = Q1 & nextMoveMode = BWD & next(nextMoveMode = FWD)) -> next(specState = Q2))
G((specState = Q1 & next(nextMoveMode = BWD)) -> next(specState = Q1))
G((specState = Q2 & next(nextMoveMode = FWD)) -> next(specState) = Q2)
G((nextMoveMode = TURN_RIGHT | nextMoveMode = TURN_LEFT) -> next(specState = Q0))
G ((Button = PRESSED) -> next(nextHead = Heading))
G ((Button = FREE) -> (next(nextHead) = nextHead))
G (next(turnState) = T0 -> (turnState = T0 | turnState = T3))
G ((turnState = T0 & !(nextMoveMode = TURN_RIGHT | nextMoveMode = TURN_LEFT)) -> next(turnState) = T0)
G (turnState = T1 -> (next(turnState) = T2 & (nextMoveMode = TURN_RIGHT | nextMoveMode = TURN_LEFT)))
G ((turnState = T2 & (nextMoveMode = TURN_RIGHT | nextMoveMode = TURN_LEFT)) -> next(turnState) = T1)
G ((turnState = T2 & nextMoveMode = FWD) -> next(turnState) = T3)
G ((turnState = T3 & nextMoveMode = FWD) -> next(turnState = T0))
G ((turnState = T3 & nextMoveMode != FWD) -> next(turnState = T2))
G((spec_policy = SEEKING)-> (next(spec_policy)=SEEKING| next(spec_policy) = MEASURING| next(spec_policy) = PARKING_0))
G((spec_policy = MEASURING)-> (next(spec_policy)=SEEKING| next(spec_policy) = MEASURING| next(spec_policy) = PARKING_0))
G((spec_policy = PARKING_0)-> (next(spec_policy)=(PARKING_1)))
G((spec_policy = PARKING_1)-> (next(spec_policy)=(PARKING_2)))
G((spec_policy = PARKING_2)-> (next(spec_policy)=(PARKED)))
G(((obstacle=BLOCKED) &(spec_policy=MEASURING |spec_policy=SEEKING))->(next(spec_policy) = SEEKING))
G(((spec_policy = SEEKING) & (sideSense = BLOCKED) & parkResult=NA) -> ((next(spec_policy) = spec_policy) & (parkCommand = STOP)))
G (((spec_policy = SEEKING) & sideSense=CLEAR & (obstacle = CLEAR) & parkResult = NA) -> (next(spec_policy) = MEASURING) & throttle=FWD & parkCommand=START & steer = CENTER)
G (((spec_policy = MEASURING) & (sideSense=BLOCKED) &(parkResult =NA)) -> (next(spec_policy) = SEEKING) & (parkCommand = STOP))
G (((spec_policy = MEASURING) & sideSense=CLEAR & (obstacle = CLEAR) &(parkResult =NA)) -> (next(spec_policy) = spec_policy)&throttle=FWD & parkCommand=CHECK & steer = CENTER)
G ((spec_policy = PARKING_0) -> (next(spec_policy) = PARKING_1) & (throttle = BWD) & steer = RIGHT & (parkCommand = STOP))
G ((spec_policy = PARKING_1) -> (next(spec_policy) = PARKING_2) & (throttle = STOP) & steer = LEFT & (parkCommand = STOP))
G ((spec_policy = PARKING_2) -> (next(spec_policy) = PARKED) & (throttle = BWD) & steer = LEFT & (parkCommand = STOP))
G (((spec_policy = PARKED)) -> (next(spec_policy) = spec_policy) & (throttle = STOP) & (steer = CENTER) & (parkCommand = STOP))
G((policy = SEEKING)-> (next(policy)=SEEKING| next(policy) = MEASURING| next(policy) = PARKING_0))
G((policy = MEASURING)-> (next(policy)=SEEKING| next(policy) = MEASURING| next(policy) = PARKING_0))
G((policy = PARKING_0)-> (next(policy)=(PARKING_1)))
G((policy = PARKING_1)-> (next(policy)=(PARKING_2)))
G((policy = PARKING_2)-> (next(policy)=(PARKED)))
G((policy = PARKED)-> (next(policy)=(PARKED)))
G(((obstacle=BLOCKED) & (policy = SEEKING | policy = MEASURING)) ->(next(policy) = SEEKING) & !(throttle = FWD | throttle = BLOCKING_FWD | throttle = BLOCKING_BWD) & !(steer = EASY_RIGHT | steer = EASY_LEFT))
G(((policy = SEEKING) & (sideSense = CLOSE | sideSense = CENTERED | sideSense = FAR) & parkResult=NA) -> ((next(policy) = policy) & (parkCommand = STOP)))
G (((policy = SEEKING) & !(sideSense = CLOSE | sideSense = CENTERED | sideSense = FAR) & (obstacle = CLEAR)) -> (next(policy) = MEASURING) & throttle=FWD & parkCommand=START & steer = CENTER)
G (((policy = MEASURING) & (sideSense = CLOSE | sideSense = CENTERED | sideSense = FAR) &(parkResult =NA)) -> (next(policy) = SEEKING) & (parkCommand = STOP))
G (((policy = MEASURING) & !(sideSense = CLOSE | sideSense = CENTERED | sideSense = FAR) & (obstacle = CLEAR) &(parkResult =NA)) -> (next(policy) = policy) & throttle=FWD & parkCommand=CHECK)
G ((policy = PARKING_0) -> (next(policy) = PARKING_1) & (throttle = STOP) & steer = CENTER & (parkCommand = STOP))
G ((policy = PARKING_1) -> (next(policy) = PARKING_2) & (throttle = BLOCKING_BWD) & steer = RIGHT & (parkCommand = STOP))
G ((policy = PARKING_2) -> (next(policy) = PARKED) & (throttle = BLOCKING_BWD) & steer = LEFT & (parkCommand = STOP))
G (((policy = PARKED)) -> (next(policy) = policy) & (throttle = STOP) & (steer = CENTER) & (parkCommand = STOP))
G((policy = PARKED)-> (next(policy)=(PARKED) | next(policy)=(EXIT_0)))
G((policy = EXIT_0)-> (next(policy)=(EXIT_1)))
G((policy = EXIT_1)-> (next(policy)=(SEEKING)))
G(((policy = SEEKING) & (sideSense = CLOSE | sideSense = CENTERED | sideSense = FAR)) -> ((next(policy) = policy) & (parkCommand = STOP)))
G ((policy = PARKING_0) -> (next(policy) = PARKING_1) & (throttle = BLOCKING_FWD) & steer = CENTER & (parkCommand = STOP))
G (((policy = PARKED) & colorSense = GREEN & reset = FREE) -> (next(policy) = policy) & (throttle = STOP) & (steer = CENTER) & (parkCommand = STOP))
G (((policy = PARKED) & (!(colorSense = GREEN) | reset = PRESSED )) -> (next(policy) = EXIT_0) & (throttle = EXIT_FWD) & (steer = LEFT) & (parkCommand = STOP))
G (((policy = EXIT_0)) -> (next(policy) = EXIT_1) & (throttle = EXIT_FWD) & (steer = RIGHT) & (parkCommand = STOP))
G (((policy = EXIT_1)) -> (next(policy) = SEEKING) & (steer = CENTER) & (throttle = STOP))
G(!next(spec_park) -> !next(spec_policy = PARKED))
G(next(spec_park) -> next(spec_policy = PARKED))
G (((spec_policy = SEEKING) & (sideSense=BLOCKED) & (obstacle=CLEAR)) -> (next(spec_policy=SEEKING) & throttle=FWD & parkCommand=STOP &steer = CENTER) )
G (((spec_policy = SEEKING) & (sideSense=BLOCKED)) -> (next(spec_policy=SEEKING) & parkCommand=STOP &steer = CENTER) )
G (((spec_policy = SEEKING) & (sideSense=CLEAR | sideSense = P_O) & (obstacle = CLEAR) &(parkResult =NA)) -> (next(spec_policy = MEASURING)&throttle=FWD & parkCommand=START & steer = CENTER))
G (((spec_policy = MEASURING) & (sideSense=CLEAR | sideSense = P_O)& (obstacle = CLEAR) &(parkResult =NA)) -> (next(spec_policy = MEASURING)&throttle=FWD & parkCommand=CHECK & steer = CENTER))
G (((spec_policy = MEASURING) & (sideSense=CLEAR | sideSense = P_O)& (obstacle = CLEAR) &(parkResult =PARALLEL)) -> (next(spec_policy = PARKING) & (throttle = STOP) & (parkCommand = STOP) & steer = CENTER) )
G (((spec_policy = MEASURING) & (sideSense=BLOCKED) & (obstacle = CLEAR) & (parkResult =PARALLEL)) -> (next(spec_policy = PARKING) & (throttle = STOP) & (parkCommand = STOP)) )
G (((spec_policy = MEASURING) & (sideSense=BLOCKED)& (obstacle = CLEAR) &(parkResult =NA)) -> (next(spec_policy = SEEKING) & (throttle = FWD) & (parkCommand = STOP)) )
G ( (spec_policy = PARKING) -> (next(spec_policy = PARKED)))
G (((spec_policy = PARKED)) -> (next(spec_policy = PARKED) & (throttle = STOP) & (steer = LEFT) & (parkCommand = STOP)) )
G(((obstacle=BLOCKED) &!(spec_policy=PARKING | spec_policy = PARKED))->(next(spec_policy = SEEKING)))
G(((spec_policy = SEEKING) & (sideSense = BLOCKED)) -> ((next(spec_policy) = spec_policy)))
G (((spec_policy = SEEKING) & (sideSense=CLEAR | sideSense = P_O) & (obstacle = CLEAR)) -> (next(spec_policy) = MEASURING)&throttle=FWD & parkCommand=START & steer = CENTER)
G (((spec_policy = MEASURING) & (sideSense=CLEAR | sideSense = P_O)& (obstacle = CLEAR) &(parkResult =NA)) -> (next(spec_policy) = spec_policy)&throttle=FWD & parkCommand=CHECK & steer = CENTER)
G (((spec_policy = MEASURING) & (sideSense=CLEAR | sideSense = P_O)& (obstacle = CLEAR) &(parkResult =PARALLEL)) -> (next(spec_policy) = PARKING_0) & (throttle = STOP) & (parkCommand = STOP) & steer = RIGHT)
G (((spec_policy = MEASURING) & (sideSense=BLOCKED) & (obstacle = CLEAR) & (parkResult =PARALLEL)) -> (next(spec_policy) = PARKING_0) & (throttle = STOP) & (parkCommand = STOP) & steer = RIGHT)
G (((spec_policy = MEASURING) & (sideSense=BLOCKED)& (obstacle = CLEAR) &(parkResult =NA)) -> (next(spec_policy) = SEEKING) & (throttle = FWD) & (parkCommand = STOP))
G(((obstacle=BLOCKED) &!(spec_policy=PARKING_0 |spec_policy=PARKING_1 |spec_policy=PARKING_2| spec_policy=PARKED))->(next(spec_policy) = SEEKING))
G((spec_policy = PARKED)-> (next(spec_policy)=(PARKED) | next(spec_policy)=(EXIT_0)))
G((spec_policy = EXIT_0)-> (next(spec_policy)=(EXIT_1)))
G((spec_policy = EXIT_1)-> (next(spec_policy)=(EXIT_2)))
G((spec_policy = EXIT_2)-> (next(spec_policy)=(SEEKING)))
G(((obstacle=BLOCKED) & (spec_policy = SEEKING | spec_policy = MEASURING)) ->(next(spec_policy) = SEEKING) & !(throttle = FWD | throttle = BLOCKING_FWD | throttle = BLOCKING_BWD) & !(steer = EASY_RIGHT | steer = EASY_LEFT))
G(((spec_policy = SEEKING) & (sideSense = CLOSE | sideSense = CENTERED | sideSense = FAR) & parkResult=NA) -> ((next(spec_policy) = spec_policy) & (parkCommand = STOP)))
G (((spec_policy = SEEKING) & !(sideSense = CLOSE | sideSense = CENTERED | sideSense = FAR) & (obstacle = CLEAR)) -> (next(spec_policy) = MEASURING) & throttle=FWD & parkCommand=START & steer = CENTER)
G (((spec_policy = MEASURING) & (sideSense = CLOSE | sideSense = CENTERED | sideSense = FAR) &(parkResult =NA)) -> (next(spec_policy) = SEEKING) & (parkCommand = STOP))
G (((spec_policy = MEASURING) & !(sideSense = CLOSE | sideSense = CENTERED | sideSense = FAR) & (obstacle = CLEAR) &(parkResult =NA)) -> (next(spec_policy) = spec_policy) & throttle=FWD & parkCommand=CHECK)
G ((spec_policy = PARKING_0) -> (next(spec_policy) = PARKING_1) & (throttle = BLOCKING_FWD) & steer = CENTER & (parkCommand = STOP))
G ((spec_policy = PARKING_1) -> (next(spec_policy) = PARKING_2) & (throttle = BLOCKING_BWD) & steer = RIGHT & (parkCommand = STOP))
G ((spec_policy = PARKING_2) -> (next(spec_policy) = PARKED) & (throttle = BLOCKING_BWD) & steer = LEFT & (parkCommand = STOP))
G (((spec_policy = PARKED)) -> (next(spec_policy) = EXIT_0) & (throttle = EXIT_FWD) & (steer = LEFT) & (parkCommand = STOP))
G (((spec_policy = EXIT_0)) -> (next(spec_policy) = EXIT_1) & (throttle = EXIT_FWD) & (steer = RIGHT) & (parkCommand = STOP))
G (((spec_policy = EXIT_1)) -> (next(spec_policy) = EXIT_2) & (steer = CENTER) & (throttle = STOP))
G (((spec_policy = EXIT_2)) -> (next(spec_policy) = SEEKING))
G((spec_policy = EXIT_1)-> (next(spec_policy)=(SEEKING)))
G(((spec_policy = SEEKING) & (sideSense = CLOSE | sideSense = CENTERED | sideSense = FAR)) -> ((next(spec_policy) = spec_policy) & (parkCommand = STOP)))
G (((spec_policy = PARKED) & colorSense = RED) -> (next(spec_policy) = spec_policy) & (throttle = STOP) & (steer = CENTER) & (parkCommand = STOP))
G (((spec_policy = PARKED) & colorSense != RED) -> (next(spec_policy) = EXIT_0) & (throttle = EXIT_FWD) & (steer = LEFT) & (parkCommand = STOP))
G (((spec_policy = EXIT_1)) -> (next(spec_policy) = SEEKING) & (steer = CENTER) & (throttle = STOP))
G (((spec_policy = PARKED) & colorSense = GREEN & reset = FREE) -> (next(spec_policy) = spec_policy) & (throttle = STOP) & (steer = CENTER) & (parkCommand = STOP))
G (((spec_policy = PARKED) & (!(colorSense = GREEN) | reset = PRESSED )) -> (next(spec_policy) = EXIT_0) & (throttle = EXIT_FWD) & (steer = LEFT) & (parkCommand = STOP))
G(((obstacle=BLOCKED) & (spec_policy = SEEKING | spec_policy = MEASURING) & command=AUTO) ->(next(spec_policy) = SEEKING) & !(throttle = FWD | throttle = BLOCKING_FWD | throttle = BLOCKING_BWD) & !(steer = EASY_RIGHT | steer = EASY_LEFT))
G (((spec_policy = SEEKING) & !(sideSense = CLOSE | sideSense = CENTERED | sideSense = FAR) & (obstacle = CLEAR)& command=AUTO) -> (next(spec_policy) = MEASURING) & throttle=FWD & parkCommand=START & steer = CENTER)
G (((spec_policy = MEASURING) & !(sideSense = CLOSE | sideSense = CENTERED | sideSense = FAR) & (obstacle = CLEAR) &(parkResult =NA)& command=AUTO) -> (next(spec_policy) = spec_policy) & throttle=FWD & parkCommand=CHECK)
G ((spec_policy = PARKING_0 & command=AUTO) -> (next(spec_policy) = PARKING_1) & (throttle = BLOCKING_FWD) & steer = CENTER & (parkCommand = STOP))
G ((spec_policy = PARKING_1 & command=AUTO) -> (next(spec_policy) = PARKING_2) & (throttle = BLOCKING_BWD) & steer = RIGHT & (parkCommand = STOP))
G ((spec_policy = PARKING_2 & command=AUTO) -> (next(spec_policy) = PARKED) & (throttle = BLOCKING_BWD) & steer = LEFT & (parkCommand = STOP))
G (((spec_policy = PARKED) & colorSense = GREEN & reset = FREE & command=AUTO) -> (next(spec_policy) = spec_policy) & (throttle = STOP) & (steer = CENTER) & (parkCommand = STOP))
G (((spec_policy = PARKED) & (!(colorSense = GREEN) | reset = PRESSED ) & command=AUTO) -> (next(spec_policy) = EXIT_0) & (throttle = EXIT_FWD) & (steer = LEFT) & (parkCommand = STOP))
G (((spec_policy = EXIT_0 ) & command=AUTO) -> (next(spec_policy) = EXIT_1) & (throttle = EXIT_FWD) & (steer = RIGHT) & (parkCommand = STOP))
G (((spec_policy = EXIT_1) & command=AUTO) -> (next(spec_policy) = SEEKING) & (steer = CENTER) & (throttle = STOP))
G((carStatus = SEEKING_FOR_PS & (weGotSideSensorMeasuringValues) & obstacle = CLEAR ) -> ( (engineMot = STOP) & (next(carStatus = MEASURE_PARKING)) & (next(spec_counter) = 1) ) )
G((carStatus = MEASURE_PARKING & (weGotSideSensorSeekingValues) & obstacle = CLEAR & spec_counter < suitableParallelPS & !capablePerpendicular ) -> (next(carStatus = SEEKING_FOR_PS)) )
G((carStatus = MEASURE_PARKING & (weGotSideSensorSeekingValues) & obstacle = CLEAR & spec_counter < suitableParallelPS & capablePerpendicular ) -> (next(carStatus = ALIGN_BEFORE_PARKING) & (next(spec_parkingType) = PERPENDICULAR) & next(spec_counter = 0) ) )
G((carStatus = MEASURE_PARKING & (weGotSideSensorMeasuringValues) & obstacle = CLEAR & engineMot = FWD & spec_counter < suitableParallelPS ) -> (next(spec_counter) = (spec_counter + 1)) )
G ((carStatus = MEASURE_PARKING & spec_counter = suitableParallelPS & obstacle = CLEAR ) -> ( (next(carStatus) = PREPARE_FOR_PARALLEL_PARKING) & (next(spec_counter) = 0) ))
G((carStatus = PREPARE_FOR_PARALLEL_PARKING & obstacle = CLEAR & spec_counter < preparingParallelSteps ) -> ((next(spec_counter) = (spec_counter + 1)) & engineMot = FWD) )
G ((carStatus = PREPARE_FOR_PARALLEL_PARKING & spec_counter = preparingParallelSteps & obstacle = CLEAR ) -> ( (Stop) & (next(carStatus) = ALIGN_BEFORE_PARKING) & (next(spec_parkingType) = PARALLEL) & (next(spec_counter) = 0) ))
G((carStatus = ALIGN_BEFORE_PARKING & spec_counter = 0 & obstacle = CLEAR & ((rearTooFar & (frontCentered | frontTooClose)) | (rearCentered & frontTooClose)))-> (sensorMot = BWD & Stop & keepCarStatus & next(spec_counter = 1)) )
G((carStatus = ALIGN_BEFORE_PARKING & spec_counter = 1 & obstacle = CLEAR) -> (engineMot = BWD & keepCarStatus & next(spec_counter = 2) & steeringMot = ALIGN_RIGHT) )
G((carStatus = ALIGN_BEFORE_PARKING & spec_counter = 2 & obstacle = CLEAR ) -> (sensorMot = FWD & Stop & keepCarStatus & next(spec_counter = 3)) )
G((carStatus = ALIGN_BEFORE_PARKING & spec_counter = 3 & obstacle = CLEAR) -> (engineMot = FWD & keepCarStatus & next(spec_counter = 0) & steeringMot = CENTER) )
G((carStatus = ALIGN_BEFORE_PARKING & spec_counter = 0 & obstacle = CLEAR & ((frontTooFar & (rearCentered | rearTooClose)) | (frontCentered & rearTooClose)))-> (engineMot = FWD & keepCarStatus & next(spec_counter = 4) & (steeringMot = ALIGN_RIGHT)) )
G((carStatus = ALIGN_BEFORE_PARKING & spec_counter = 4 & obstacle = CLEAR)-> (sensorMot = BWD & Stop & keepCarStatus & next(spec_counter = 5)) )
G ((carStatus = ALIGN_BEFORE_PARKING & spec_counter = 5 & obstacle = CLEAR)-> (engineMot = BWD & keepCarStatus & next(spec_counter = 0) & steeringMot = CENTER) )
G((carStatus = ALIGN_BEFORE_PARKING & spec_counter = 0 & obstacle = CLEAR & (rearTooFar & frontTooFar))-> (engineMot = FWD & steeringMot = ALIGN_RIGHT & keepCarStatus & next(spec_counter = 6)) )
G((carStatus = ALIGN_BEFORE_PARKING & spec_counter = 6 & obstacle = CLEAR) -> (engineMot = FWD & steeringMot=ALIGN_LEFT & keepCarStatus & next(spec_counter = 7)) )
G((carStatus = ALIGN_BEFORE_PARKING & spec_counter = 7 & obstacle = CLEAR) -> (sensorMot = BWD & Stop & keepCarStatus & next(spec_counter = 8)) )
G((carStatus = ALIGN_BEFORE_PARKING & spec_counter = 8 & obstacle = CLEAR) -> (engineMot = BWD & keepCarStatus & next(spec_counter = 9) & steeringMot = CENTER) )
G((carStatus = ALIGN_BEFORE_PARKING & spec_counter = 9 & obstacle = CLEAR) -> (engineMot = BWD & keepCarStatus & next(spec_counter = 0) & steeringMot = CENTER) )
G((carStatus = ALIGN_BEFORE_PARKING & spec_counter = 0 & obstacle = CLEAR & (rearTooClose & frontTooClose))-> (engineMot = FWD & steeringMot = ALIGN_LEFT & keepCarStatus & next(spec_counter = 10)) )
G((carStatus = ALIGN_BEFORE_PARKING & spec_counter = 10 & obstacle = CLEAR) -> (engineMot = FWD & steeringMot=ALIGN_RIGHT & keepCarStatus & next(spec_counter = 11)) )
G((carStatus = ALIGN_BEFORE_PARKING & spec_counter = 11 & obstacle = CLEAR) -> (sensorMot = BWD & Stop & keepCarStatus & next(spec_counter = 12)) )
G((carStatus = ALIGN_BEFORE_PARKING & spec_counter = 12 & obstacle = CLEAR) -> (engineMot = BWD & keepCarStatus & next(spec_counter = 13) & steeringMot = CENTER) )
G((carStatus = ALIGN_BEFORE_PARKING & spec_counter = 13 & obstacle = CLEAR) -> (engineMot = BWD & keepCarStatus & next(spec_counter = 0) & steeringMot = CENTER) )
G((carStatus = ALIGN_BEFORE_PARKING & spec_counter = 0 & spec_parkingType = PERPENDICULAR & rearCentered & frontCentered & obstacle = CLEAR ) -> ((sensorMot = BWD) & Stop & next(spec_counter = firstPhase) & next(carStatus) = PERPENDICULAR) )
G((carStatus = ALIGN_BEFORE_PARKING & spec_counter = 0 & spec_parkingType = PARALLEL & rearCentered & frontCentered & obstacle = CLEAR ) -> ((sensorMot = BWD) & Stop & next(spec_counter = firstPhase) & next(carStatus) = PARALLEL) )
G((carStatus = PARALLEL & spec_counter = firstPhase & obstacle = CLEAR ) -> (engineMot = PARKING_BWD & (keepCarStatus) & steeringMot = MAX_RIGHT & next(spec_counter = secondPhase)) )
G((carStatus = PARALLEL & spec_counter = secondPhase & obstacle = CLEAR ) -> (engineMot = PARKING_BWD & (next(carStatus = PARKED)) & steeringMot = MAX_LEFT) )
G((carStatus = PERPENDICULAR & spec_counter = firstPhase & obstacle = CLEAR ) -> (engineMot = PREPARE_PERPENDICULAR_BWD & (keepCarStatus) & steeringMot = CENTER & next(spec_counter = secondPhase)) )
G((carStatus = PERPENDICULAR & spec_counter = secondPhase & obstacle = CLEAR ) -> (engineMot = PARKING_FWD & (keepCarStatus) & steeringMot = MAX_LEFT & next(spec_counter = thirdPhase)) )
G((carStatus = PERPENDICULAR & spec_counter = thirdPhase & obstacle = CLEAR ) -> (engineMot = PERPENDICULAR_BWD & next(carStatus = PARKED) & steeringMot = MAX_RIGHT) )
G((carStatus = MEASURE_PARKING & (weGotSideSensorSeekingValues) & obstacle = CLEAR & spec_counter < suitableParallelPS & capablePerpendicular ) -> (next(carStatus = PERPENDICULAR) & next(spec_counter = firstPhase) & sensorMot = BWD & Stop ) )
G ((carStatus = PREPARE_FOR_PARALLEL_PARKING & spec_counter = preparingParallelSteps & obstacle = CLEAR ) -> ( (Stop) & (next(carStatus) = PARALLEL) & next(spec_counter = firstPhase) & (sensorMot = BWD) ))
G(((carStatus = SEEKING_FOR_PS | carStatus = MEASURE_PARKING) & spec_obstacleCounter < 2 & obstacle = BLOCKED ) -> (Stop & (next(spec_obstacleCounter) = spec_obstacleCounter + 1) & keepCarStatus & keepCounterValue) )
G((carStatus = BYPASSING & spec_counter = 0 & obstacle = CLEAR )-> (next(spec_counter = 1) ) )
G((carStatus = BYPASSING & spec_counter = 1 & obstacle = CLEAR )-> (engineMot = BWD & steeringMot = CENTER & next(spec_counter = 2) ) )
G((carStatus = BYPASSING & spec_counter = 2 & obstacle = CLEAR )-> (engineMot = BWD & steeringMot = CENTER & next(spec_counter = 3) ) )
G((carStatus = BYPASSING & spec_counter = 3 & obstacle = CLEAR )-> (next(spec_counter = 4) ) )
G((carStatus = BYPASSING & spec_counter = 4 & obstacle = CLEAR )-> (engineMot = BYPASS_FWD & steeringMot = MAX_LEFT & next(spec_counter = 5) ) )
G((carStatus = BYPASSING & spec_counter = 5 & obstacle = CLEAR & sideSensor = TOO_CLOSE)-> (engineMot = FWD & steeringMot = CENTER & next(spec_counter = 6)) )
G((carStatus = BYPASSING & spec_counter = 5 & obstacle = CLEAR & sideSensor != TOO_CLOSE)-> (Stop & steeringMot = CENTER & next(spec_counter = 6)) )
G((carStatus = BYPASSING & spec_counter = 6 & obstacle = CLEAR )-> (engineMot = PARKING_FWD & steeringMot = MAX_RIGHT & next(spec_counter = 7) & next(spec_obstacleCounter = 0 ) ))
G((movingNextToObstacle & (weGotSideSensorSeekingValues | weGotRearSideSensorSeekingValues) & obstacle = CLEAR & spec_obstacleCounter < 3 )-> (keepCounterValue & next(spec_obstacleCounter = 0 )) )
G((movingNextToObstacle & weGotSideSensorMeasuringValues & weGotRearSideSensorMeasuringValues & obstacle = CLEAR & spec_obstacleCounter < 6 )-> (keepCounterValue & (next(spec_obstacleCounter) = 1 + spec_obstacleCounter)) )
G((movingNextToObstacle & obstacle = CLEAR & spec_obstacleCounter = 6)-> (Stop & sensorMot = BWD & next(spec_counter = 8)))
G((carStatus = BYPASSING & spec_counter = 8 & obstacle = CLEAR )-> (engineMot = PARKING_BWD & steeringMot = MAX_RIGHT & next(spec_counter = 9) ) )
G((carStatus = BYPASSING & spec_counter = 9 & obstacle = CLEAR )-> (engineMot = PARKING_BWD & steeringMot = MAX_LEFT & next(spec_counter = 10)) )
G((carStatus = BYPASSING & spec_counter = 10)-> (sensorMot = FWD & Stop & next(carStatus = SEEKING_FOR_PS)) )
G((carStatus = BYPASSING) -> (next(carStatus = SEEKING_FOR_PS) | next(carStatus = BYPASSING)))
G (!stopping -> (next(motors) = motors | next(stopping)))
G noTasksForward -> next(!forwarding)
G noTasksBackward -> next(!backwarding)
G (accelerating -> (next(mLeft) - mLeft = 1 | (mLeft = 4 & next(mLeft)=4) ))
G (slowingDown -> ((mLeft = 0 & next(mLeft)=0) | mLeft - next(mLeft) = 1 ))
G ((inRange & (lastDist = sense)) -> (mLeft = next(mLeft)))
G (!inLane -> (next(turning) | next(stopping)))
G ((inRange & (lastDist = sense) & inLane) -> (mLeft = next(mLeft)))
G (inLane -> !next(turning))
G farFromNextCar -> next(accelerating)
G ((inRange & (lastDist > sense)) -> next(slowingDown))
G ((inRange & (lastDist < sense)) -> next(accelerating))
G ((inRange & (lastDist = sense)) -> (!next(accelerating) & !next(slowingDown) ))
G (tooClose -> next(slowingDown))
G moving -> (next (lightIsOn) = !lightIsOn)
G (!moving) -> (next(!lightIsOn) )
G goingUp->next(goingUp|atDesignatedFloor|floor3|atEmergencyFloor)
G goingDown->next(goingDown|atDesignatedFloor|floor0|atEmergencyFloor)
G (!atFloor&next(atDesignatedFloor)&(!returnTo0))->next(stayInPlace)
G (atFloor&stayInPlace&next(atDesignatedFloor)/*&!returnTo0*/)->next(stayInPlace)
G (atFloor&!stayInPlace)/*&(floor_c=next(floor_c))*/->next(!stayInPlace|atEmergencyFloor)
G !stayInPlace -> next(sound_c)
G (stayInPlace) -> (next(!sound_c))
G (atFloor&stayInPlace&next(atDesignatedFloor))->next(stayInPlace)
G (atFloor&!stayInPlace)->next(!stayInPlace|atEmergencyFloor)
G(moving->(next(lightIsOn)!=lightIsOn))
G((!moving)->(!next(lightIsOn)))
G moving -> (next (lightIsOn) != lightIsOn)
G (mode = PARKING & done = true & align = true & color = BLUE ) -> (next(mode) = PARKING )
G (align = false) -> (next(mode) = PARKING )
G(mode = PARKING & status = REVERSE & align = false & done = false & next(frontSense >0)) -> (next(steeringMotor)= STRAIGHT & next(driveMotor) = FWD)
G(mode = PARKING & status = REVERSE & align = true & done = false & next(frontSense >0)) -> (next(steeringMotor) = HARD_RIGHT & next(driveMotor) = FWD & next(velocity) =1 & next(mode) = PARKING ) 
G(mode = PARKING & status = PARALLEL & align = false & done = false & next(frontSense >0)) -> (next(steeringMotor)= LIGHT_LEFT& next(driveMotor) = FWD)
G(mode = PARKING & status = PARALLEL & align = true & done = false & next(frontSense >0)) -> (next(steeringMotor) = LIGHT_RIGHT & next(driveMotor) = FWD & next(velocity) =1 & next(mode) = PARKING ) 
G(valid_parking_spot) -> (next(mode) = PARKED)
G driveMotor = STOP -> next(velocity) <= velocity
G mode = PARKING -> next(mode = PARKING | mode = PARKED)
G (mode = PARKING & done = false) -> next(mode = PARKING | mode = PARKED)
G (align = false) -> (next(mode) = PARKING)
G(mode = PARKING & align = false & done = false) -> (next(steeringMotor)= HARD_RIGHT & next(driveMotor) = BWD)
G(mode = PARKING & status = PARALLEL & align = true & done = false) -> (next(steeringMotor) = HARD_LEFT & next(driveMotor) = BWD & next(velocity) =1 & next(mode) = PARKING) 
G(mode = PARKING & status = REVERSE & align = true & done = false) -> (next(steeringMotor) = STRAIGHT & next(driveMotor) = BWD & next(velocity) =1 & next(mode) = PARKING) 
G ((frontSense <= 2) & (mode !=EXIT)) -> (((driveMotor != FWD) | steeringMotor = HARD_LEFT & next(mode = SEARCHING)))
G ((mode = SEARCHING) & status = NONE) -> (next(driveMotor) = FWD)
G (mode = SCANNING & sideStatus = NONE) -> (next(mode) = SEARCHING)
G (mode = SCANNING & status = NONE & sideStatus != NONE & frontSense >2 ) -> (next(mode) = SCANNING)
G (mode = SEARCHING & sideStatus = NONE) -> (next(mode) = SEARCHING)
G (mode = SEARCHING & sideStatus != NONE & frontSense >2) -> (next(mode) = SCANNING)
G (mode = SCANNING & status = REVERSE & sideStatus = MIN_PARALLEL & frontSense >2) -> (next(mode) = SCANNING)
G (mode = SCANNING & ((status = REVERSE & sideStatus = MIN_REVERSE) | (status = PARALLEL & sideStatus = MIN_PARALLEL)) ) -> (next(stopping) & (next(mode) = PARKING) & steeringMotor = STRAIGHT)
G (mode = PARKING & align = false) -> (next(mode) = PARKING)
G(mode = PARKING & valid_parking_spot) -> (next(mode) = PARKED)
G (mode = PARKED & !button) -> (next(mode) = PARKED)
G (mode = PARKED & button) -> (next(mode) = EXIT)
G (mode = PARKING & done = true & align = true & color = BLUE ) -> (next(mode) = EXIT ) & next(stopping)
G (mode = EXIT & done = true & align = true ) -> (next(mode) = SEARCHING ) & next(stopping)
G (mode = EXIT & align = false) -> (next(mode) = EXIT)
G (mode = EXIT & next(frontSense<=2) & done = false) -> (next(mode) = EXIT) & next(stopping)
G(mode = EXIT & status = REVERSE & align = false & done = false & next(frontSense) >2 ) -> (next(steeringMotor)= STRAIGHT & next(driveMotor) = FWD)
G(mode = EXIT & status = REVERSE & align = true & done = false & next(frontSense) >2 ) -> (next(steeringMotor) = HARD_RIGHT & next(driveMotor) = FWD & next(velocity) =1 & next(mode) = EXIT ) 
G(mode = EXIT & status = PARALLEL & align = false & done = false & next(frontSense) >2) -> (next(steeringMotor)= LIGHT_LEFT& next(driveMotor) = FWD)
G(mode = EXIT & status = PARALLEL & align = true & done = false & next(frontSense) >2) -> (next(steeringMotor) = LIGHT_RIGHT & next(driveMotor) = FWD & next(velocity) =1 & next(mode) = EXIT ) 
G(mode = PARKED) -> (next(mode) = EXIT)
G mode = SCANNING & frontSense > 2 & sideSense > 2 -> senseMotor = SIDE & next(mode) = SCANNING & driveMotor = FWD & steeringMotor = STRAIGHT
G mode = PARKED -> next(mode) = PARKED & driveMotor = STOP & steeringMotor = STRAIGHT
G (mode = SEARCHING & frontSense > 2 & sideSense > 2 & status = NONE) -> (senseMotor = SIDE & next(mode) = SCANNING & driveMotor = FWD & steeringMotor = STRAIGHT)
G (mode = SCANNING & frontSense > 2 & sideSense > 2 & status = NONE) -> (senseMotor = SIDE & next(mode) = SCANNING & driveMotor = FWD & steeringMotor = STRAIGHT)
G (frontSense <= 2 & (mode = SCANNING | mode = SEARCHING) & status = NONE) -> (senseMotor = SIDE & next(mode) = SEARCHING & driveMotor = FWD & steeringMotor = HARD_LEFT)
G (mode = PARKING) -> (next(mode) = PARKING | next(mode) = PARKED)
G (driveMotor = BWD) -> (next(driveMotor) = BWD | next(sideSense) = sideSense - 1)
G (driveMotor = FWD) -> (next(driveMotor) = FWD | next(sideSense) = sideSense + 1)
G ((mode = SEARCHING) & status = NONE & frontSense > 2 & next(frontSense)>2 ) -> (steeringMotor = STRAIGHT & next(driveMotor) = FWD)
G (mode = SCANNING & sideSense <= 2 & status = NONE) -> (next(mode) = SEARCHING)
G (mode = SCANNING & status = NONE & sideSense >2 ) -> (next(mode) = SCANNING)
G (mode = SEARCHING & sideSense <= 2) -> (next(mode) = SEARCHING)
G ((mode = SEARCHING) & frontSense > 2 & sideSense > 2) -> (next(mode) = SCANNING)
G (status = PARALLEL & mode = SCANNING) -> (next(mode) = PARKING)
G (mode = PARKING) -> (next(mode) != SEARCHING & next(mode) != SCANNING)
G (mode = SCANNING & status = NONE & sideStatus != NONE ) -> (next(mode) = SCANNING)
G (mode = SEARCHING & sideStatus != NONE) -> (next(mode) = SCANNING)
G (mode = SCANNING & status = REVERSE & sideStatus = MIN_PARALLEL) -> (next(mode) = SCANNING)
G ((frontSense <= 2)) -> (((driveMotor != FWD) | steeringMotor = HARD_LEFT & next(mode = SEARCHING)))
G(mode = PARKED) -> (next(mode) = PARKED)
G(mode = PARKED & !button) -> (next(mode) = PARKED)
G(mode = PARKED & button) -> (next(mode) = EXIT)
G ((frontSense <= 2) & (mode !=EXIT)) -> (((driveMotor != FWD) | (steeringMotor = HARD_LEFT & next(mode = SEARCHING)) | next(mode = MANUAL)))
G ((mode = SEARCHING) & status = NONE) -> (next(driveMotor = FWD) | !manual)
G (mode = SCANNING & sideStatus = NONE ) -> (next(mode = SEARCHING)| !manual)
G (mode = SEARCHING & sideStatus = NONE) -> (next(mode = SEARCHING) | !manual)
G (mode = SEARCHING & sideStatus != NONE & frontSense >2) -> (next(mode) = SCANNING | !manual)
G (mode = SCANNING & status = REVERSE & sideStatus = MIN_PARALLEL & frontSense >2) -> (next(mode) = SCANNING | !manual)
G (mode = SCANNING & manual = false & ((status = REVERSE & sideStatus = MIN_REVERSE) | (status = PARALLEL & sideStatus = MIN_PARALLEL)) ) -> (next(stopping) & (next(mode) = PARKING) & steeringMotor = STRAIGHT)
G (mode = PARKING & align = false & manual = false) -> (next(mode) = PARKING)
G(mode = PARKING & status = PARALLEL & align = true & done = false) -> ((next(steeringMotor) = HARD_LEFT & next(driveMotor) = BWD & next(velocity) =1 & next(mode) = PARKING) | !manual)
G(mode = PARKING & status = REVERSE & align = true & done = false) -> ((next(steeringMotor) = STRAIGHT & next(driveMotor) = BWD & next(velocity) =1 & next(mode) = PARKING) | !manual) 
G(mode = PARKED & !button) -> (next(mode = PARKED) | !manual)
G(mode = PARKED & button) -> (next(mode = EXIT) | !manual)
G (mode = PARKING & done = true & align = true & color = BLUE) -> (next(mode = EXIT & stopping) | !manual)
G (mode = EXIT & done = true & align = true) -> (next(mode = SEARCHING & stopping) | !manual)
G(mode = EXIT & status = REVERSE & align = true & done = false & next(frontSense) >2 ) -> ((next(steeringMotor) = HARD_RIGHT & next(driveMotor) = FWD & next(velocity) =1 & next(mode) = EXIT) | !manual) 
G ((mode = SEARCHING) & status = NONE) -> (next(driveMotor = FWD) | next(mode)= MANUAL)
G (mode = SCANNING & sideStatus = NONE ) -> (next(mode = SEARCHING)| next(mode)= MANUAL)
G (mode = SCANNING & status = NONE & sideStatus != NONE & frontSense >2) -> ((next(mode) = SCANNING) | next(mode)= MANUAL)
G (mode = SEARCHING & sideStatus = NONE) -> (next(mode = SEARCHING) | next(mode)= MANUAL)
G (mode = SEARCHING & sideStatus != NONE & frontSense >2) -> (next(mode) = SCANNING |next(mode)= MANUAL)
G (mode = SCANNING & status = REVERSE & sideStatus = MIN_PARALLEL & frontSense >2) -> (next(mode) = SCANNING | next(mode)= MANUAL)
G (mode = SCANNING & ((status = REVERSE & sideStatus = MIN_REVERSE) | (status = PARALLEL & sideStatus = MIN_PARALLEL)) ) -> ((next(stopping) & (next(mode) = PARKING) & steeringMotor = STRAIGHT) | (next(mode) = MANUAL))
G (mode = PARKING & align = false & manual = false) -> (next(mode) = PARKING | (next(mode) = MANUAL))
G(mode = PARKING & align = false & done = false) -> ((next(steeringMotor)= HARD_RIGHT & next(driveMotor) = BWD) | next(mode)= MANUAL)
G(mode = PARKING & status = PARALLEL & align = true & done = false) -> ((next(steeringMotor) = HARD_LEFT & next(driveMotor) = BWD & next(velocity) =1 & next(mode) = PARKING) | next(mode)= MANUAL)
G(mode = PARKING & status = REVERSE & align = true & done = false) -> ((next(steeringMotor) = STRAIGHT & next(driveMotor) = BWD & next(velocity) =1 & next(mode) = PARKING) | next(mode)= MANUAL) 
G(mode = PARKING & valid_parking_spot) -> ((next(mode) = PARKED) | next(mode)= MANUAL)
G(mode = PARKED & !button) -> (next(mode = PARKED) | next(mode)= MANUAL)
G(mode = PARKED & button) -> (next(mode = EXIT) | next(mode)= MANUAL)
G (mode = PARKING & done = true & align = true & color = BLUE) -> (next(mode = EXIT & stopping) | next(mode)= MANUAL)
G (mode = EXIT & done = true & align = true) -> (next(mode = SEARCHING & stopping) | next(mode)= MANUAL)
G (mode = EXIT & align = false) -> (next(mode) = EXIT | next(mode)= MANUAL)
G (mode = EXIT & next(frontSense<=2) & done = false) -> ((next(mode) = EXIT & next(stopping))) | next(mode)= MANUAL
G(mode = EXIT & status = REVERSE & align = false & done = false & next(frontSense) >2 ) -> ((next(steeringMotor)= STRAIGHT & next(driveMotor) = FWD)| next(mode)= MANUAL)
G(mode = EXIT & status = REVERSE & align = true & done = false & next(frontSense) >2 ) -> ((next(steeringMotor) = HARD_RIGHT & next(driveMotor) = FWD & next(velocity) =1 & next(mode) = EXIT) | next(mode)= MANUAL) 
G(mode = EXIT & status = PARALLEL & align = false & done = false & next(frontSense) >2) -> ((next(steeringMotor)= LIGHT_LEFT& next(driveMotor) = FWD)| next(mode)= MANUAL)
G(mode = EXIT & status = PARALLEL & align = true & done = false & next(frontSense) >2) -> ((next(steeringMotor) = LIGHT_RIGHT & next(driveMotor) = FWD & next(velocity) =1 & next(mode) = EXIT )| next(mode)= MANUAL) 
G (mode = SCANNING & sideStatus = NONE & status = NONE) -> (next(mode) = SEARCHING)
G (mode = SEARCHING & sideStatus!= NONE) -> (next(mode) = SCANNING)
G (mode = SCANNING & ((status = REVERSE & sideStatus = MIN_REVERSE) | (status = PARALLEL & sideStatus = MIN_PARALLEL)) ) -> (next(stopping) & (next(mode) = PARKING) & steeringMotor = STRAIGHT & next(steeringMotor) = STRAIGHT)
G task = HANOI & !hanoiIsMoving -> next(r0) = r0 & next(r1) = r1 & next(r2) = r2 
G task != HANOI -> next(initRs)
G task != HANOI -> next(initCounters)
