G (verMot = MOVE -> (botMot = STOP & horMot = SLEEP))
G (horMot = MOVE -> (botMot = STOP & verMot = SLEEP))
G (botMot != STOP -> (verMot = SLEEP & horMot = SLEEP))
G (ack_ver = MOVE | ack_hor = MOVE -> allsleep)
G (!spec_dropping & starting_pos = YES & color = BLACK -> allsleep)
G (color = BLACK | spec_dropping -> verMot = SLEEP)
G (spec_pausing = PAUSE -> allsleep)
G (color = BLACK & spec_nonemove & spec_allsleep -> spec_allsleep)
G (spec_dropping -> verMot = SLEEP)
G (color = BLACK & !spec_dropping -> spec_allsleep)
G (ack_ver = MOVE | ack_hor = MOVE -> spec_allsleep)
G (!spec_dropping -> botMot = STOP & horMot = SLEEP)
G (color = BLACK & !spec_dropping -> allsleep)
G (spec_prevBotMotReturn & ack_bot = SLEEP -> allsleep)
G (num_of_cubes = ZERO -> allsleep)
G (!isReady -> balancer=STP)
G ((balancer=FWD) -> (frontDistSense=CLEAR))
G ((balancer=BWD) -> (backDistSense=CLEAR))
G ((isReady & frontDistSense=CLEAR) -> balancer=FWD)
G ((distSense=BLOCKED & isReady) -> !(balancer=FWD))
G ((distSense=CLEAR & isReady) -> (balancer=FWD))
G ((balancer=FWD) -> (distSense=CLEAR))
G ((balancerStatus=OK) -> (bluetoothStatus=OK))
G ((balancerStatus=FELL) -> (bluetoothStatus=FELL))
G((Obstacle = BLOCKED) -> (!(spec_nextMoveMode = FWD)))
G((InputMoveMode = FWD & Obstacle = BLOCKED) -> ((OutputMoveMode = BWD & LeftMotor = BWD & RightMotor = FWD)))
G((InputMoveMode = BWD & Obstacle = CLEAR) -> ((OutputMoveMode = FWD & LeftMotor = FWD & RightMotor = BWD)))
G ((InputMoveMode = FWD & Obstacle = CLEAR) -> (LeftMotor = FWD & RightMotor = FWD))
G ((Obstacle = BLOCKED) -> (OutputMoveMode = BWD))
G((InputMoveMode = FWD & Obstacle = BLOCKED) -> (OutputMoveMode = TURN_LEFT_1))
G ((Obstacle = BLOCKED) -> !(OutputMoveMode = FWD))
G ((InputMoveMode = TURN_LEFT_1) -> (LeftMotor = FWD & RightMotor = TURN_FWD))
G ((InputMoveMode = TURN_LEFT_2) -> (LeftMotor = BWD & RightMotor = TURN_BWD))
G (!(InputMoveMode = TURN_LEFT_1 | InputMoveMode = TURN_LEFT_2) -> !(LeftMotor = TURN_BWD | RightMotor = TURN_BWD |LeftMotor = TURN_FWD & RightMotor = TURN_FWD))
G ((InputMoveMode = TURN_LEFT_1 | InputMoveMode = TURN_LEFT_2) -> (HeadMotor = STOP))
G((InputMoveMode = FWD & Obstacle = BLOCKED) -> (OutputMoveMode = TURN_LEFT_1 & LeftMotor = CALIB_TURN & RightMotor = CALIB_TURN))
G ((InputMoveMode = TURN_LEFT_2 & Obstacle = CLEAR) -> (OutputMoveMode = FWD))
G ((InputMoveMode = DANCE & OutputMoveMode = DANCE) -> (RightMotor = STOP & LeftMotor = DANCE & HeadMotor = DANCE))
G ((Button = FREE) -> (OutputMoveMode = InputMoveMode | InputMoveMode != DANCE))
G ((Button = PRESSED & InputMoveMode = FWD & Obstacle = CLEAR) -> (OutputMoveMode = DANCE & LeftMotor = CALIB_TURN & RightMotor = CALIB_TURN))
G ((Button = PRESSED & InputMoveMode = DANCE & Obstacle = CLEAR) -> OutputMoveMode = FWD & LeftMotor = CALIB_FWD & RightMotor = CALIB_FWD)
G (!(Button = PRESSED | InputMoveMode = DANCE) -> !(OutputMoveMode = DANCE))
G((Obstacle = BLOCKED) -> !(nextMoveMode = FWD))
G((Obstacle = BLOCKED) -> (!(nextMoveMode = FWD)))
G ((((spec_nextHead = N & Heading = EA) | (spec_nextHead = EA & Heading = SO) | (spec_nextHead = SO & Heading = W) | (spec_nextHead = W & Heading = N)) & (spec_turnState = T0)) -> spec_nextMoveMode != TURN_RIGHT)
G ((((spec_nextHead = EA & Heading = N) | (spec_nextHead = SO & Heading = EA) | (spec_nextHead = W & Heading = SO) | (spec_nextHead = N & Heading = W)) & (spec_turnState = T0)) -> spec_nextMoveMode != TURN_LEFT)
G ((obstacle = BLOCKED)->!(throttle = FWD))
G ((sideSense = BLOCKED) -> !((steer =RIGHT) &(throttle=FWD)))
G((obstacle=BLOCKED)->(parkCommand=STOP))
G ((spec_policy = SEEKING & parkResult=NA) -> (throttle != STOP))
G ((policy = SEEKING) -> ((throttle = FWD | throttle = STOP | throttle = BWD)))
G ((policy = MEASURING) -> (throttle != BLOCKING_BWD & parkCommand != START & (steer = CENTER | steer = EASY_LEFT | steer = EASY_RIGHT)))
G (((obstacle = CLEAR) & (policy=SEEKING) & parkResult = NA)->(throttle = FWD))
G ((policy = SEEKING & parkResult=NA) -> (throttle != STOP))
G((policy=SEEKING & obstacle = CLEAR & sideSense = CLOSE) -> (steer=EASY_LEFT))
G((policy=SEEKING & obstacle = CLEAR & sideSense = FAR) -> (steer=EASY_RIGHT))
G((policy=MEASURING & obstacle = CLEAR & sideSense = CLOSE_PARKING) -> (steer=EASY_LEFT))
G((policy=MEASURING & obstacle = CLEAR & sideSense = PERPENDICULAR) -> (steer=EASY_RIGHT))
G((policy=MEASURING & obstacle = CLEAR & sideSense = PARALLEL_PARKING) -> (steer=CENTER))
G ((policy = SEEKING & obstacle = CLEAR) -> (!(steer = RIGHT | steer = LEFT )))
G (obstacle=BLOCKED -> ( !(throttle = FWD) ))
G (((obstacle = CLEAR) & (sideSense = CLEAR)) -> (steer = CENTER))
G (((spec_policy=SEEKING|spec_policy=MEASURING)& obstacle = BLOCKED)->(throttle = BWD))
G (((spec_policy=PARKING|spec_policy=PARKED)& obstacle = BLOCKED)->!(throttle = FWD))
G ((sideSense = BLOCKED) -> !(steer =RIGHT))
G (spec_policy = SEEKING -> (throttle != STOP))
G ((spec_policy = SEEKING) -> ((throttle = FWD | throttle = STOP | throttle = BWD)))
G ((spec_policy = MEASURING) -> (throttle != BLOCKING_BWD & parkCommand != START & (steer = CENTER | steer = EASY_LEFT | steer = EASY_RIGHT)))
G (((obstacle = CLEAR) & (spec_policy=SEEKING) & parkResult = NA)->(throttle = FWD))
G((spec_policy=SEEKING & obstacle = CLEAR & sideSense = CLOSE) -> (steer=EASY_LEFT))
G((spec_policy=SEEKING & obstacle = CLEAR & sideSense = FAR) -> (steer=EASY_RIGHT))
G((spec_policy=MEASURING & obstacle = CLEAR & sideSense = CLOSE_PARKING) -> (steer=EASY_LEFT))
G((spec_policy=MEASURING & obstacle = CLEAR & sideSense = PERPENDICULAR) -> (steer=EASY_RIGHT))
G ((spec_policy = SEEKING & obstacle = CLEAR) -> (!(steer = RIGHT | steer = LEFT )))
G(command=MANUAL -> throttle=STOP & steer=CENTER)
G(command=FWD -> throttle=FWD & steer=CENTER)
G((command=BWD)-> throttle=BWD & steer=CENTER)
G((command=RIGHT) ->( steer=RIGHT & throttle=STOP))
G((command=LEFT)-> steer=LEFT & throttle=STOP)
G((command=CENTER)-> steer=CENTER & throttle=STOP )
G((command=FWD_LEFT)-> steer=LEFT & throttle=FWD )
G((command=FWD_RIGHT)-> steer=RIGHT & throttle=FWD)
G((command=BWD_LEFT)-> steer=LEFT & throttle=BWD )
G( command=BWD_RIGHT -> steer=RIGHT & throttle=BWD)
G ((spec_policy = SEEKING & command=AUTO ) -> ((throttle = FWD | throttle = STOP | throttle = BWD)))
G ((spec_policy = SEEKING & obstacle = CLEAR & command=AUTO ) -> (!(steer = RIGHT | steer = LEFT )))
G ((spec_policy = MEASURING & command=AUTO) -> (throttle != BLOCKING_BWD & parkCommand != START & (steer = CENTER | steer = EASY_LEFT | steer = EASY_RIGHT)))
G (((obstacle = CLEAR) & (spec_policy=SEEKING) & parkResult = NA & command=AUTO)->(throttle = FWD))
G ((spec_policy = SEEKING & parkResult=NA & command=AUTO) -> (throttle != STOP))
G((spec_policy=MEASURING & obstacle = CLEAR & sideSense = CLOSE_PARKING & command=AUTO) -> (steer=EASY_LEFT))
G((spec_policy=MEASURING & obstacle = CLEAR & sideSense = PERPENDICULAR & command=AUTO) -> (steer=EASY_RIGHT))
G ((obstacle = BLOCKED) -> (Stop) )
G ((obstacle = BLOCKED ) -> (keepCarStatus & keepCounterValue ) )
G(movingBwd -> sensorMot = BWD)
G(movingFwd -> sensorMot = FWD)
G((carStatus = PARKED ) -> ((Stop) & (keepCarStatus) & steeringMot = CENTER ) )
G((carStatus = SEEKING_FOR_PS)-> ((steeringMot = ALIGN_RIGHT | steeringMot = CENTER | steeringMot = ALIGN_LEFT) & (engineMot = FWD | engineMot = STOP) & (spec_counter = 0) ) )
G((carStatus = SEEKING_FOR_PS | carStatus = PREPARE_FOR_PARALLEL_PARKING | carStatus = MEASURE_PARKING)-> ( ((sideSensor = TOO_CLOSE | sideSensor = PS_TOO_CLOSE) & steeringMot = ALIGN_LEFT) | ((sideSensor = TOO_FAR | sideSensor = PS_TOO_FAR) & steeringMot = ALIGN_RIGHT) | ((sideSensor = CENTERED | sideSensor = PS_CENTERED) & steeringMot = CENTER) ) )
G((carStatus = SEEKING_FOR_PS & (weGotSideSensorSeekingValues) & obstacle = CLEAR ) -> (keepCarStatus) )
G((carStatus = MEASURE_PARKING)-> ((steeringMot = ALIGN_RIGHT | steeringMot = CENTER | steeringMot = ALIGN_LEFT) & (engineMot = FWD | engineMot = STOP) & (spec_counter <= suitableParallelPS)) )
G((carStatus = MEASURE_PARKING & obstacle = CLEAR & weGotSideSensorMeasuringValues) -> (engineMot != STOP) )
G((carStatus = MEASURE_PARKING & (weGotSideSensorMeasuringValues) & (spec_counter < suitableParallelPS) & obstacle = CLEAR ) -> (keepCarStatus) )
G((carStatus = PREPARE_FOR_PARALLEL_PARKING)-> ((steeringMot = ALIGN_RIGHT | steeringMot = CENTER | steeringMot = ALIGN_LEFT) & (engineMot = FWD | engineMot = STOP)) )
G((carStatus = PREPARE_FOR_PARALLEL_PARKING & (spec_counter < preparingParallelSteps) ) -> (keepCarStatus) )
G((carStatus = ALIGN_BEFORE_PARKING) -> keepParkingType)
G((carStatus = PARALLEL) -> ((steeringMot = MAX_RIGHT | steeringMot = CENTER | steeringMot = MAX_LEFT) & (engineMot = PARKING_BWD | engineMot = STOP)) )
G((carStatus = PERPENDICULAR) -> ((steeringMot = MAX_RIGHT | steeringMot = CENTER | steeringMot = MAX_LEFT) & (engineMot = PARKING_FWD | engineMot = STOP | engineMot = PREPARE_PERPENDICULAR_BWD | engineMot = PERPENDICULAR_BWD)) )
G ((obstacle = BLOCKED & !(carStatus = SEEKING_FOR_PS | carStatus = MEASURE_PARKING | (carStatus = BYPASSING & spec_counter = 10) | (carStatus=PERPENDICULAR & spec_counter = thirdPhase) )) -> (keepCarStatus & keepCounterValue ) )
G((carStatus = SEEKING_FOR_PS | carStatus = PREPARE_FOR_PARALLEL_PARKING | carStatus = MEASURE_PARKING | movingNextToObstacle)-> ( ((sideSensor = TOO_CLOSE | sideSensor = PS_TOO_CLOSE) & steeringMot = ALIGN_LEFT) | ((sideSensor = TOO_FAR | sideSensor = PS_TOO_FAR) & steeringMot = ALIGN_RIGHT) | ((sideSensor = CENTERED | sideSensor = PS_CENTERED) & steeringMot = CENTER) ) )
G((carStatus = BYPASSING & spec_counter < 10) -> (keepCarStatus))
G((carStatus = BYPASSING & spec_counter = 0 )-> (Stop & sensorMot = BWD) )
G((carStatus = BYPASSING & spec_counter = 3 )-> (Stop & sensorMot = FWD ) )
G atStationWithTask -> stopping
G waitingForDoor -> stopping
G atStation & atEmgState -> stopping
G noTasks & atBaseStation -> stopping
G (techGuyInAction & atStation -> stopping)
G atGivenStation(0) -> !backwarding
G atGivenStation(3) -> !forwarding
G noTasksForward -> !forwarding
G noTasksBackward & !goToBaseStation -> !backwarding
G noTasks & atStation & !goToBaseStation -> stopping
G !atStation -> !stopping
G (!goToBaseStation & atStation & !atStationWithTask & !noTasks & !waitingForDoor & !techGuyInAction) -> !stopping
G (atStation & stopAtNearestStation -> stopping)
G (doorStatus=IN_PROCESS -> doorReq=NIL)
G (techGuyInAction -> stopping)
G doorStatus = OPENED -> pickUpStation = station
G doorStatus != OPENED -> pickUpStation = stationNone
G isTaskDirectionFwdOrNoTask(shuttleDirection, lastPassedStation, pressedStation) -> updateTasks(shuttleTasksFwd, pressedStation, pickUpStation) & updateTasks(shuttleTasksBwd, 4, 4)
G isTaskDirectionBwdOrNoTask(shuttleDirection, lastPassedStation, pressedStation) -> updateTasks(shuttleTasksBwd, pressedStation, pickUpStation) & updateTasks(shuttleTasksFwd, 4, 4)
G ( (noRequests & atBaseStation) -> stopping & updateTasks(shuttleTasksFwd, 4, 4) & updateTasks(shuttleTasksBwd, 4, 4))
G enteringStation & taskAtCurrentStation -> stopping & satisfiesTask 
G atStation & noTasks -> stopping
G noTasks -> stopping
G noTasksForwardAndExistsTaskBackward -> backwarding
G noTasksBackwardAndExistsTaskForward -> forwarding
G noTasksForward -> (!forwarding)
G noTasksBackward -> (!backwarding)
G (noTaskAtCurrentStation & !noTasks) -> (!stopping)
G (!atStationWithTask & !noTasks) -> (!stopping)
G noTasks & atStation -> stopping
G noTasksBackward -> !backwarding
G (atStation & !atStationWithTask & !noTasks) -> !stopping
G (!goToBaseStation & atStation & !atStationWithTask & !noTasks) -> !stopping
G (!goToBaseStation & atStation & !atStationWithTask & !noTasks & !waitingForDoor) -> !stopping
G farFromNextCar -> (accelerating)
G ((inRange & (lastDist > sense)) -> (slowingDown))
G ((inRange & (lastDist < sense)) -> (accelerating))
G (tooClose -> (slowingDown))
G (accelerating -> (accelLeft | accelRight))
G (slowingDown -> (slowDownLeft | slowDownRight))
G ((farFromNextCar & inLane) -> (accelerating))
G ((inRange & (lastDist > sense) & inLane) -> (slowingDown))
G ((inRange & (lastDist < sense) & inLane) -> (accelerating))
G ((farFromNextCar) -> (accelerating))
G ((inRange & (lastDist < sense)) -> accelerating)
G (laneClear -> accelerating)
G (nextCarCloser -> slowingDown)
G (nextCarFarther -> accelerating)
G (tooClose -> slowingDown)
G floor0 -> !(goingDown) 
G floor3 -> !(goingUp) 
G doorsAreClosed -> (!closingDoors) 
G doorsAreFullyOpened->(!openningDoors)
G (((!anyCalls) & (!returnTo0))| (returnTo0 & floor0)) -> !moving
G (!atDesignatedFloor)->(!openningDoors)
G atDesignatedFloor->(!moving)
G (!(moving|anyCalls |floor0|returnTo0) | firstStateAtDesignatedFloor | openStateAtDesignatedFloor)->countTime_c
G (floor0 -> (!goingDown))
G (floor3 -> (!goingUp))
G (doorsAreClosed -> (!closingDoors))
G (doorsAreFullyOpened->(!openingDoors))
G ((!anyMemCalls & !returnTo0 & !memEmergency) | (returnTo0 & floor0)) -> stayInPlace
G (!stayInPlace->keepDoorsState)
G ((!doorsAreClosed)/*|(doorsWereFullyOpened)*/)->(stayInPlace)
G (!atDesignatedFloor&!atEmergencyFloor)->keepDoorsState
G ((!((emergency_c&doorsAreClosed)|memEmergency))&(!(!stayInPlace|anyCalls|anyMemCalls|floor0|returnTo0) | firstStateAtDesignatedFloor&(!returnTo0) | fullyOpenedStateAtDesignatedFloor))->(countTime_c)
G (((emergency_c&doorsAreClosed)|memEmergency)|(returnTo0)|(!atDesignatedFloor&(floor0|anyCalls|anyMemCalls))|(!stayInPlace)|(lastStateAtDesignatedFloor)|(doorsAreOpened))->(!countTime_c)
G(firstStateAtDesignatedFloor&(noSeconds)/*&!emergency*/&!atEmergencyFloor)->keepDoorsState
G(fullyOpenedStateAtDesignatedFloor&(noSeconds|seconds3)/*&!emergency*/&!memEmergency)->keepDoorsState
G (returnTo0&!floor0)->(goingDown|atEmergencyFloor)
G (atEmergencyFloor->stayInPlace)
G (atEmergencyFloor&!doorsWereFullyOpened&!doorsAreFullyOpened&stayInPlace)->openingDoors
G ((!doorsAreClosed))->(stayInPlace)
G (!atDesignatedFloor&!atEmergencyFloor/*&!atSabbathFloor&(!doorsAreClosed)*/)->keepDoorsState
G ((!(/*sabbath_c|*/emergency_c|memEmergency))&(!(!stayInPlace|anyCalls|anyMemCalls|floor0|returnTo0) | firstStateAtDesignatedFloor&(!returnTo0) | fullyOpenedStateAtDesignatedFloor))->(countTime_c)
G (/*sabbath_c|*/(emergency_c|memEmergency)|(returnTo0)|(!atDesignatedFloor&(floor0|anyCalls|anyMemCalls))| (!stayInPlace)|(lastStateAtDesignatedFloor)|(doorsAreOpened))->(!countTime_c)
G(firstStateAtDesignatedFloor&(noSeconds)&!atEmergencyFloor)->keepDoorsState
G(fullyOpenedStateAtDesignatedFloor&(noSeconds|seconds3)&!memEmergency&!sabbathMode)->keepDoorsState
G ((!(emergency_c|memEmergency))&(!(!stayInPlace|anyCalls|anyMemCalls|floor0|returnTo0) | firstStateAtDesignatedFloor&(!returnTo0) | fullyOpenedStateAtDesignatedFloor))->(countTime_c)
G ((emergency_c|memEmergency)|(returnTo0)|(!atDesignatedFloor&(floor0|anyCalls|anyMemCalls))| (!stayInPlace)|(lastStateAtDesignatedFloor)|(doorsAreOpened))->(!countTime_c)
G (!doorsAreClosed)->(stayInPlace)
G(firstStateAtDesignatedFloor&(seconds3)&!atEmergencyFloor)->openingDoors
G(moving -> (doorsAreClosed&keepDoorsState))
G(floor0->!(goingDown))
G(floor3->!(goingUp))
G ((!anyCalls)&(!returnTo0))->!moving
G (returnTo0&(!floor0))->goingDown
G (moving -> (doorsAreClosed & keepDoorsState))
G floor0 -> ! (goingDown) 
G floor3 -> ! (goingUp) 
G ( ((!anyCalls) & (!returnTo0)) | handleFloor) -> !moving
G (!doorsAreClosed)->(!moving)
G (atDesignatedFloor&!returnTo0)->(!moving)
G (!handleFloor)->(!openningDoors)
G (returnTo0&(!doorsAreClosed))->closingDoors
G (returnTo0&!floor0&doorsAreClosed)->goingDown
G (handleFloor&doorsAreFullyOpened&(!seconds5))->(!closingDoors)
G (((!anyCalls) & (!returnTo0)) | (returnTo0 & floor0)) -> !moving
G (/*!(moving|anyCalls |floor0|returnTo0) |*/ firstMomentAtDesignatedFloor | openMomentAtDesignatedFloor)->countTime_c
G mode = PARKING -> velocity <= 1
G forwarding -> frontSense > 0
G(mode = PARKED -> stopping)
G scanning -> forwarding & steeringMotor = STRAIGHT 
G frontSense = 0 -> driveMotor != FWD
G frontSense = 5 & senseMotor != REVERSE -> velocity = 5
G frontSense = 4 & senseMotor != REVERSE -> velocity = 4
G frontSense = 3 & senseMotor != REVERSE -> velocity = 3
G frontSense = 2 & senseMotor != REVERSE-> velocity = 2
G frontSense = 1 -> velocity = 1
G senseMotor != REVERSE & sideSense =0 -> !sideways
G ((mode = SCANNING | mode = PARKING | mode = EXIT) /*| mode = EXIT*/ & driveMotor != STOP | reversing) -> (velocity = 1)
G ((mode = SCANNING) & (status = NONE | (status = REVERSE & sideStatus = MIN_PARALLEL)) & frontSense > 2) -> (steeringMotor = STRAIGHT & driveMotor = FWD)
G (frontSense = 5 & mode = SEARCHING & driveMotor = FWD) -> (velocity = 5)
G (frontSense = 4 & mode = SEARCHING & driveMotor = FWD) -> (velocity = 4)
G (frontSense = 3 & mode = SEARCHING & driveMotor = FWD) -> (velocity = 3)
G (frontSense = 2 & mode = SEARCHING & driveMotor = FWD) -> (velocity = 2)
G (frontSense = 1 & mode = SEARCHING & driveMotor = FWD) -> (velocity = 1)
G mode = SEARCHING | mode = SCANNING -> senseMotor = SIDE
G frontSense = 5 & mode = SEARCHING -> velocity = 5
G frontSense = 4 & mode = SEARCHING -> velocity = 4
G frontSense = 3 & mode = SEARCHING -> velocity = 3
G frontSense = 2 & mode = SEARCHING -> velocity = 2
G frontSense = 1 | mode = PARKING | mode = SCANNING -> velocity = 1
G (mode = SEARCHING | mode = SCANNING) & status = NONE -> senseMotor = SIDE
G (mode = PARKED) -> (driveMotor = STOP & steeringMotor = STRAIGHT)
G ((mode = SCANNING) & status = NONE & frontSense > 2) -> (steeringMotor = STRAIGHT & driveMotor = FWD)
G (frontSense <= 2) -> (driveMotor != FWD)
G reversing -> velocity = 1
G (frontSense = 5 & mode = SEARCHING & !stopping) -> (velocity = 5)
G (frontSense = 4 & mode = SEARCHING & !stopping ) -> (velocity = 4)
G (frontSense = 3 & mode = SEARCHING & !stopping) -> (velocity = 3)
G (frontSense = 3 & (mode = PARKING | mode = SCANNING) & !stopping) -> (velocity = 1)
G ((frontSense <= 2)) -> ((driveMotor != FWD) | steeringMotor = HARD_LEFT)
G ((mode = SCANNING | mode = PARKING) /*| mode = EXIT*/ & driveMotor != STOP | reversing) -> (velocity = 1)
G (((sense = BLOCKED) & (senseMotor =DRIVE)) -> ! forwarding)
G (((sense = BLOCKED) & (senseMotor = REVERSE)) -> ! reversing)
G (((sense = BLOCKED) & (senseMotor = DRIVE)) -> ! forwarding)
G forwarding -> senseMotor = DRIVE
G reversing -> senseMotor = REVERSE
G sense = CLEAR -> velocity = 5
G sense = VERY_FAR -> velocity = 4
G sense = FAR -> velocity = 3
G sense = MEDIUM -> velocity = 2
G sense = CLOSE -> velocity = 1
G ((mode = SCANNING | mode = PARKING | mode = EXIT) & driveMotor != STOP | reversing) -> (velocity = 1)
G (frontSense = 5 & (mode = SEARCHING | mode = MANUAL) & driveMotor = FWD) -> (velocity = 5)
G (frontSense = 4 & (mode = SEARCHING | mode = MANUAL) & driveMotor = FWD) -> (velocity = 4)
G (frontSense = 3 & (mode = SEARCHING | mode = MANUAL) & driveMotor = FWD) -> (velocity = 3)
G (frontSense = 2 & (mode = SEARCHING | mode = MANUAL) & driveMotor = FWD) -> (velocity = 2)
G (frontSense = 1 & (mode = SEARCHING | mode = MANUAL) & driveMotor = FWD) -> (velocity = 1)
G (mode = MANUAL & frontSense > 2 -> (driveMotor = driveCmd & steeringMotor = steeringCmd))
G ((mode = MANUAL & frontSense > 2) -> (driveMotor = driveCmd & steeringMotor = steeringCmd))
G ((mode = MANUAL & frontSense <= 2) -> (driveMotor = STOP & steeringMotor = steeringCmd))
G scanning -> forwarding
G senseMotor = REVERSE -> velocity = 1
G (driveMotor = BWD & backSense != BLOCKED) -> senseMotor = REVERSE
G frontSense = BLOCKED -> driveMotor != FWD
G (backSense = BLOCKED & steeringMotor = STRAIGHT & senseMotor = REVERSE) -> driveMotor != BWD
G senseMotor = REVERSE & reversing -> velocity = 1
G frontSense = CLEAR -> velocity = 5
G frontSense = VERY_FAR -> velocity = 4
G frontSense = FAR -> velocity = 3
G frontSense = MEDIUM -> velocity = 2
G frontSense = CLOSE -> velocity = 1
G ((sense = BLOCKED) -> ! forwarding)
G clapped -> turning
G (backSense = BLOCKED & senseMotor = REVERSE) -> driveMotor != BWD
G (senseMotor = REVERSE & reversing) -> velocity = 1
G (frontSense = CLEAR & !reversing) -> velocity = 5
G (frontSense = VERY_FAR & !reversing) -> velocity = 4
G (frontSense = FAR & !reversing) -> velocity = 3
G (frontSense = MEDIUM & !reversing) -> velocity = 2
G frontSense = 5 -> velocity = 5
G frontSense = 4 -> velocity = 4
G frontSense = 3 -> velocity = 3
G frontSense = 2 -> velocity = 2
G ( sideSense <= 1) -> (steeringMotor = STRAIGHT)
G (frontSense = 3 & (mode = SCANNING) & !stopping) -> (velocity = 1)
G (frontSense <= 2) -> ((driveMotor != FWD) | steeringMotor = HARD_LEFT)
G initDone -> mode != INIT
G (task = SORT & sorted & mode != INIT) -> mode = NOTHING
G (task = EXCHANGE & initDone) -> (mode = MOVE & incrementFrom)
G (mode = MOVE) -> (fromExists & toExists & toIsEmpty & from != to)
G (isMoving) -> (fromColor != NOT & toColor = EMPTY)
G task = SORT & sortDone -> !isMoving
G (task = SORT & sorted) -> mode = NOTHING
G (task = EXCHANGE) -> (mode = MOVE & incrementFrom)
G (isMoving & task != HANOI) -> (fromColor != NOT & toColor = EMPTY)
G task = HANOI & hanoiDone -> !isMoving
G task = HANOI & isMoving -> hanoiLegalMove
G task = EXCHANGE -> (isMoving & incrementFrom)
G (task = GATHER_REDS & gatherRedsDone) -> !isMoving
G (task = MOVE_RED_LEFT & moveRedLeftDone) -> !isMoving
G (isMoving ) -> (fromColor != NOT & toColor = EMPTY)
G task = HANOI & hanoiDone -> !hanoiIsMoving
G task = HANOI & hanoiIsMoving -> hanoiLegalMove
G hanoiIsMoving -> task = HANOI
G isMoving -> task != HANOI
G !hanoiIsMoving -> hanoiFrom = 0 & hanoiTo = 1
G task = SORT & !sortDone -> isMoving
G task = HANOI -> !isMoving
G task = HANOI & !hanoiDone -> hanoiIsMoving
G task = MOVE_RED_LEFT & isMoving -> fromColor = RED
G (sorted & mode != INIT) -> mode = STOP
G (mode = MOVE) -> (fromExists & toExists & toIsEmpty)
G (sorted & mode != INIT) -> mode = NOTHING
