G ((spec_state=S0 & ((!(ack_ver_hor = SLEEP & spec_stage = KICK & spec_pausing = go) & !(detect = spec_currentColor)) | ((ack_ver_hor = SLEEP & spec_stage = KICK & spec_pausing = go) & (ack_ver_hor = MOVE & spec_stage = DROP)) | (!(ack_ver_hor = MOVE & spec_stage = DROP) & (detect = spec_currentColor)) | (!(ack_ver_hor = SLEEP & spec_stage = KICK & spec_pausing = go) & (ack_ver_hor = MOVE & spec_stage = DROP) & (detect = spec_currentColor))) & next(spec_state=S0)) | (spec_state=S0 & ((ack_ver_hor = SLEEP & spec_stage = KICK & spec_pausing = go) & !(ack_ver_hor = MOVE & spec_stage = DROP) & !(detect = spec_currentColor)) & next(spec_state=S1)) | (spec_state=S1 & (!(ack_ver_hor = MOVE & spec_stage = DROP) & (detect = spec_currentColor)) & next(spec_state=S0)) | (spec_state=S1 & (!(ack_ver_hor = MOVE & spec_stage = DROP) & !(detect = spec_currentColor)) & next(spec_state=S1)) | (spec_state=S1 & ((ack_ver_hor = MOVE & spec_stage = DROP)) & next(spec_state=S2)) | (spec_state=S2 & next(spec_state=S2)))
G (atEdge != EDGE & (spec_stage = TOANGLERIGHT | spec_stage = TOANGLELEFT) & detect != spec_currentColor & spec_pausing = GO -> (spec_stage = TOANGLERIGHT -> botMot = RIGHT) & (spec_stage = TOANGLELEFT -> botMot = LEFT) & next(spec_stage) = spec_stage)
G (atEdge = EDGE & (spec_stage = TOANGLERIGHT | spec_stage = TOANGLELEFT) & spec_pausing = GO & detect != spec_currentColor -> (spec_stage = TOANGLERIGHT -> botMot = LEFT & next(spec_stage) = TOANGLELEFT) & (spec_stage = TOANGLELEFT -> botMot = RIGHT & next(spec_stage) = TOANGLERIGHT))
G ((spec_state=S0 & ((!(ack_ver_hor = SLEEP & spec_stage = KICK & spec_pausing = go) & !(detect = botMotColor)) | ((ack_ver_hor = SLEEP & spec_stage = KICK & spec_pausing = go) & (ack_ver_hor = MOVE & spec_stage = DROP)) | (!(ack_ver_hor = MOVE & spec_stage = DROP) & (detect = botMotColor)) | (!(ack_ver_hor = SLEEP & spec_stage = KICK & spec_pausing = go) & (ack_ver_hor = MOVE & spec_stage = DROP) & (detect = botMotColor))) & next(spec_state=S0)) | (spec_state=S0 & ((ack_ver_hor = SLEEP & spec_stage = KICK & spec_pausing = go) & !(ack_ver_hor = MOVE & spec_stage = DROP) & !(detect = botMotColor)) & next(spec_state=S1)) | (spec_state=S1 & (!(ack_ver_hor = MOVE & spec_stage = DROP) & (detect = botMotColor)) & next(spec_state=S0)) | (spec_state=S1 & (!(ack_ver_hor = MOVE & spec_stage = DROP) & !(detect = botMotColor)) & next(spec_state=S1)) | (spec_state=S1 & ((ack_ver_hor = MOVE & spec_stage = DROP)) & next(spec_state=S2)) | (spec_state=S2 & next(spec_state=S2)))
G (ack_ver_hor = SLEEP & spec_stage = KICK & spec_pausing = go & color_seen = false -> (color_seen = false -> botMot = RIGHT & next(spec_stage) = TOANGLERIGHT) & (color_seen = true -> botMot = PLACE & next(spec_stage) = TOANGLERIGHT))
G ((spec_state_1=S0 & ((!(verMot = MOVE) & !(detect = spec_currentColor)) | ((detect = spec_currentColor))) & next(spec_state_1=S0)) | (spec_state_1=S0 & ((verMot = MOVE) & !(botMot = SEEK) & !(detect = spec_currentColor)) & next(spec_state_1=S1)) | (spec_state_1=S0 & ((verMot = MOVE) & (botMot = SEEK) & !(detect = spec_currentColor)) & next(spec_state_1=S2)) | (spec_state_1=S1 & next(spec_state_1=S1)) | (spec_state_1=S2 & ((detect = spec_currentColor)) & next(spec_state_1=S0)) | (spec_state_1=S2 & (!(botMot = SEEK) & !(detect = spec_currentColor)) & next(spec_state_1=S1)) | (spec_state_1=S2 & ((botMot = SEEK) & !(detect = spec_currentColor)) & next(spec_state_1=S2)))
G ((spec_state__seek=S0 & ((!(botMot = SEEK) & !(detect = spec_currentColor)) | ((detect = spec_currentColor))) & next(spec_state__seek=S0)) | (spec_state__seek=S0 & ((botMot = SEEK) & !(botMot = SEEK) & !(detect = spec_currentColor)) & next(spec_state__seek=S1)) | (spec_state__seek=S0 & ((botMot = SEEK) & (botMot = SEEK) & !(detect = spec_currentColor)) & next(spec_state__seek=S2)) | (spec_state__seek=S1 & next(spec_state__seek=S1)) | (spec_state__seek=S2 & ((detect = spec_currentColor)) & next(spec_state__seek=S0)) | (spec_state__seek=S2 & (!(botMot = SEEK) & !(detect = spec_currentColor)) & next(spec_state__seek=S1)) | (spec_state__seek=S2 & ((botMot = SEEK) & !(detect = spec_currentColor)) & next(spec_state__seek=S2)))
G ((spec_state_return=S0 & ((!(spec_prevBotMotReturn & ack_bot = MOVE)) | ((spec_prevBotMotReturn & ack_bot = SLEEP) & (spec_prevBotMotReturn & ack_bot = MOVE))) & next(spec_state_return=S0)) | (spec_state_return=S0 & (!(spec_prevBotMotReturn & ack_bot = SLEEP) & (spec_dropping & onlybotmoves -> botMot = RETURN) & (spec_prevBotMotReturn & ack_bot = MOVE)) & next(spec_state_return=S1)) | (spec_state_return=S0 & (!(spec_prevBotMotReturn & ack_bot = SLEEP) & !(spec_dropping & onlybotmoves -> botMot = RETURN) & (spec_prevBotMotReturn & ack_bot = MOVE)) & next(spec_state_return=S3)) | (spec_state_return=S1 & ((spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S0)) | (spec_state_return=S1 & (!(spec_prevBotMotReturn & ack_bot = SLEEP) & (spec_dropping & onlybotmoves -> botMot = RETURN)) & next(spec_state_return=S1)) | (spec_state_return=S1 & (!(spec_prevBotMotReturn & ack_bot = SLEEP) & !(spec_dropping & onlybotmoves -> botMot = RETURN)) & next(spec_state_return=S3)) | (spec_state_return=S2 & next(spec_state_return=S2)) | (spec_state_return=S3 & ((spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S2)) | (spec_state_return=S3 & (!(spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S3)))
G ((spec_state_seek=S0 & ((!(spec_prevBotMotSeek & ack_bot = MOVE)) | ((spec_prevBotMotSeek & detect = spec_currentColor) & (spec_prevBotMotSeek & ack_bot = MOVE))) & next(spec_state_seek=S0)) | (spec_state_seek=S0 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & (spec_dropping & onlybotmoves & detect != spec_currentColor -> botMot = SEEK) & (spec_prevBotMotSeek & ack_bot = MOVE)) & next(spec_state_seek=S1)) | (spec_state_seek=S0 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & !(spec_dropping & onlybotmoves & detect != spec_currentColor -> botMot = SEEK) & (spec_prevBotMotSeek & ack_bot = MOVE)) & next(spec_state_seek=S3)) | (spec_state_seek=S1 & ((spec_prevBotMotSeek & detect = spec_currentColor)) & next(spec_state_seek=S0)) | (spec_state_seek=S1 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & (spec_dropping & onlybotmoves & detect != spec_currentColor -> botMot = SEEK)) & next(spec_state_seek=S1)) | (spec_state_seek=S1 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & !(spec_dropping & onlybotmoves & detect != spec_currentColor -> botMot = SEEK)) & next(spec_state_seek=S3)) | (spec_state_seek=S2 & next(spec_state_seek=S2)) | (spec_state_seek=S3 & ((spec_prevBotMotSeek & detect = spec_currentColor)) & next(spec_state_seek=S2)) | (spec_state_seek=S3 & (!(spec_prevBotMotSeek & detect = spec_currentColor)) & next(spec_state_seek=S3)))
G ((spec_state_seek=S0 & ((!(spec_prevBotMotSeek & ack_bot = MOVE)) | ((spec_prevBotMotSeek & detect = spec_currentColor) & (spec_prevBotMotSeek & ack_bot = MOVE))) & next(spec_state_seek=S0)) | (spec_state_seek=S0 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & (spec_dropping & detect != spec_currentColor -> botMot = SEEK) & (spec_prevBotMotSeek & ack_bot = MOVE)) & next(spec_state_seek=S1)) | (spec_state_seek=S0 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & !(spec_dropping & detect != spec_currentColor -> botMot = SEEK) & (spec_prevBotMotSeek & ack_bot = MOVE)) & next(spec_state_seek=S3)) | (spec_state_seek=S1 & ((spec_prevBotMotSeek & detect = spec_currentColor)) & next(spec_state_seek=S0)) | (spec_state_seek=S1 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & (spec_dropping & detect != spec_currentColor -> botMot = SEEK)) & next(spec_state_seek=S1)) | (spec_state_seek=S1 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & !(spec_dropping & detect != spec_currentColor -> botMot = SEEK)) & next(spec_state_seek=S3)) | (spec_state_seek=S2 & next(spec_state_seek=S2)) | (spec_state_seek=S3 & ((spec_prevBotMotSeek & detect = spec_currentColor)) & next(spec_state_seek=S2)) | (spec_state_seek=S3 & (!(spec_prevBotMotSeek & detect = spec_currentColor)) & next(spec_state_seek=S3)))
G ((spec_state_return=S0 & ((!(spec_prevBotMotReturn & ack_bot = MOVE) & !(spec_prevBotMotReturn & ack_bot = SLEEP)) | ((spec_prevBotMotReturn & ack_bot = SLEEP))) & next(spec_state_return=S0)) | (spec_state_return=S0 & ((spec_prevBotMotReturn & ack_bot = MOVE) & !(spec_dropping & onlybotmoves -> botMot = RETURN) & !(spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S1)) | (spec_state_return=S0 & ((spec_prevBotMotReturn & ack_bot = MOVE) & (spec_dropping & onlybotmoves -> botMot = RETURN) & !(spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S2)) | (spec_state_return=S1 & next(spec_state_return=S1)) | (spec_state_return=S2 & ((spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S0)) | (spec_state_return=S2 & (!(spec_dropping & onlybotmoves -> botMot = RETURN) & !(spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S1)) | (spec_state_return=S2 & ((spec_dropping & onlybotmoves -> botMot = RETURN) & !(spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S2)))
G ((spec_mode=AUTO & bluetoothCmd=SWITCH_MODE & next(spec_mode=MANUAL) & (spec_manualCmd=STP)) | (spec_mode=MANUAL & bluetoothCmd=SWITCH_MODE & next(spec_mode=AUTO)) | (bluetoothCmd!=SWITCH_MODE & next(spec_mode)=spec_mode) )
G ((balancerSpeed=SLOW & bluetoothCmd=SPEED_DOWN & next(balancerSpeed=SLOW)) | (balancerSpeed=SLOW & bluetoothCmd=SPEED_UP & next(balancerSpeed=REGULAR)) | (balancerSpeed=REGULAR & bluetoothCmd=SPEED_DOWN & next(balancerSpeed=SLOW)) | (balancerSpeed=REGULAR & bluetoothCmd=SPEED_UP & next(balancerSpeed=FAST)) | (balancerSpeed=FAST & bluetoothCmd=SPEED_DOWN & next(balancerSpeed=REGULAR)) | (balancerSpeed=FAST & bluetoothCmd=SPEED_UP & next(balancerSpeed=FAST)) | ((bluetoothCmd!=SPEED_DOWN & bluetoothCmd!=SPEED_UP) & next(balancerSpeed)=balancerSpeed) )
G ((spec_mode=MANUAL) -> (((bluetoothCmd=STP) -> (spec_manualCmd=STP)) & ((bluetoothCmd=FWD) -> (spec_manualCmd=FWD)) & ((bluetoothCmd=BWD) -> (spec_manualCmd=BWD)) & ((bluetoothCmd=TURN_LEFT) -> (spec_manualCmd=TURN_LEFT)) & ((bluetoothCmd=TURN_RIGHT) -> (spec_manualCmd=TURN_RIGHT)) ))
G ((bluetoothCmd=AUTO) -> ((balancer=FWD) -> next((bluetoothCmd=AUTO) -> !(balancer=TURN_RIGHT | balancer=TURN_LEFT))))
G ((bluetoothCmd=AUTO) -> ((distSense=BLOCKED & balancer=STP & isReady) -> next(!(balancer=STP))))
G (((spec_moveAwayFromFrontObstacleState=S0 & ((!moveAwayFromFrontObstacle) | (moveAwayFromFrontObstacle & (!moveAwayFromFrontObstacle | frontDistSense = CLEAR))) & next(spec_moveAwayFromFrontObstacleState=S0)) | (spec_moveAwayFromFrontObstacleState=S0 & (moveAwayFromFrontObstacle & !(!moveAwayFromFrontObstacle | frontDistSense = CLEAR)) & next(spec_moveAwayFromFrontObstacleState=S1)) | (spec_moveAwayFromFrontObstacleState=S1 & ((!moveAwayFromFrontObstacle | frontDistSense = CLEAR)) & next(spec_moveAwayFromFrontObstacleState=S0)) | (spec_moveAwayFromFrontObstacleState=S1 & (!(!moveAwayFromFrontObstacle | frontDistSense = CLEAR)) & next(spec_moveAwayFromFrontObstacleState=S1))))
G (((spec_moveAwayFromBackObstacleState=S0 & ((!moveAwayFromBackObstacle) | (moveAwayFromBackObstacle & (!moveAwayFromBackObstacle | backDistSense = CLEAR))) & next(spec_moveAwayFromBackObstacleState=S0)) | (spec_moveAwayFromBackObstacleState=S0 & (moveAwayFromBackObstacle & !(!moveAwayFromBackObstacle | backDistSense = CLEAR)) & next(spec_moveAwayFromBackObstacleState=S1)) | (spec_moveAwayFromBackObstacleState=S1 & ((!moveAwayFromBackObstacle | backDistSense = CLEAR)) & next(spec_moveAwayFromBackObstacleState=S0)) | (spec_moveAwayFromBackObstacleState=S1 & (!(!moveAwayFromBackObstacle | backDistSense = CLEAR)) & next(spec_moveAwayFromBackObstacleState=S1))))
G (((spec_forwardingState=S0 & ((!(balancer=FWD)) | ((balancer=FWD) & (balancer!=FWD | frontDistSense=BLOCKED))) & next(spec_forwardingState=S0)) | (spec_forwardingState=S0 & ((balancer=FWD) & !(balancer!=FWD | frontDistSense=BLOCKED)) & next(spec_forwardingState=S1)) | (spec_forwardingState=S1 & ((balancer!=FWD | frontDistSense=BLOCKED)) & next(spec_forwardingState=S0)) | (spec_forwardingState=S1 & (!(balancer!=FWD | frontDistSense=BLOCKED)) & next(spec_forwardingState=S1))))
G (((spec_backwardingState=S0 & ((!(balancer=BWD)) | ((balancer=BWD) & (balancer!=BWD | backDistSense=BLOCKED))) & next(spec_backwardingState=S0)) | (spec_backwardingState=S0 & ((balancer=BWD) & !(balancer!=BWD | backDistSense=BLOCKED)) & next(spec_backwardingState=S1)) | (spec_backwardingState=S1 & ((balancer!=BWD | backDistSense=BLOCKED)) & next(spec_backwardingState=S0)) | (spec_backwardingState=S1 & (!(balancer!=BWD | backDistSense=BLOCKED)) & next(spec_backwardingState=S1))))
G(!(spec_specState = Q2 & spec_nextMoveMode = FWD & next(spec_nextMoveMode = BWD)))
G(!(spec_state = Q2 & spec_nextMoveMode = FWD & next(spec_nextMoveMode = BWD)))
G(!(specState = Q2 & nextMoveMode = FWD & next(nextMoveMode = BWD)))
G((spec_b2f=S0 & ((!(throttle = BWD) & !(throttle = STOP)) | (throttle = BWD & throttle = FWD) | (!(throttle = FWD) & throttle = STOP) | (!(throttle = BWD) & throttle = FWD & throttle = STOP)) & next(spec_b2f=S0)) | (spec_b2f=S0 & (throttle = BWD & !(throttle = FWD) & !(throttle = STOP)) & next(spec_b2f=S1)) | (spec_b2f=S1 & (!(throttle = FWD) & throttle = STOP) & next(spec_b2f=S0)) | (spec_b2f=S1 & (!(throttle = FWD) & !(throttle = STOP)) & next(spec_b2f=S1)) | (spec_b2f=S1 & (throttle = FWD) & next(spec_b2f=S2)) | (spec_b2f=S2 & next(spec_b2f=S2)))
G((spec_f2b=S0 & ((!(throttle = FWD) & !(throttle = STOP)) | (throttle = FWD & throttle = BWD) | (!(throttle = BWD) & throttle = STOP) | (!(throttle = FWD) & throttle = BWD & throttle = STOP)) & next(spec_f2b=S0)) | (spec_f2b=S0 & (throttle = FWD & !(throttle = BWD) & !(throttle = STOP)) & next(spec_f2b=S1)) | (spec_f2b=S1 & (!(throttle = BWD) & throttle = STOP) & next(spec_f2b=S0)) | (spec_f2b=S1 & (!(throttle = BWD) & !(throttle = STOP)) & next(spec_f2b=S1)) | (spec_f2b=S1 & (throttle = BWD) & next(spec_f2b=S2)) | (spec_f2b=S2 & next(spec_f2b=S2)))
that we must stop in order to satisfy Task! */ G noTasks -> stopping
G (forwarding -> next (!backwarding)) & (backwarding -> next (!forwarding))
G ((-1 <= next(mLeft) - mLeft) & (next(mLeft) - mLeft <= 1))
G ((-1 <= next(mRight) - mRight) & (next(mRight) - mRight <= 1))
G ((trnLft <-> turningLeft) & (trnRt <-> turningRight))
G (pHolds_afterQuntilR(next(turningRight | tooClose), (rightColor = white), inLane))
G (pHolds_afterQuntilR(next(turningLeft | tooClose), (leftColor = black), inLane))
G ((!doorsAreClosed)->(!moving)) & (moving->keepDoorsState)
G (goingUp -> next (!goingDown)) & (goingDown -> next (!goingUp))
G moving->(next(!moving->(atDesignatedFloor|atEdgedFloor)))
G openingDoors->next((stayInPlace&(atDesignatedFloor|atEmergencyFloor)&!doorsAreFullyOpened)->openingDoors)
G closingDoors->next((stayInPlace&(atDesignatedFloor|atEmergencyFloor)&!doorsAreClosed)->closingDoors)
G closingDoors->next((stayInPlace&(atDesignatedFloor|atEmergencyFloor)&!doorsAreClosed)->(closingDoors|emergency_c))
G((floor0->(currentFloor=0))& (floor1->(currentFloor=1))& (floor2->(currentFloor=2))& (floor3->(currentFloor=3)))
G((goingUp->next(!goingDown))&(goingDown->next(!goingUp)))
G(moving->next((stayingSameHeigt)<->(atFloorThatCalled|floor3|floor0)))
G(((floor0&!calls_c[0])->next(!memCalls[0]))& ((floor1&!calls_c[1])->next(!memCalls[1]))& ((floor2&!calls_c[2])->next(!memCalls[2]))& ((floor3&!calls_c[3])->next(!memCalls[3])))
G (calls_c[0]->next(memCalls[0]))& (calls_c[1]->next(memCalls[1]))& (calls_c[2]->next(memCalls[2]))& (calls_c[3]->next(memCalls[3]))
G moving->next((stayingSameHeigt)<->(atFloorThatCalled|edged_floor))
G ((floor0&!calls_c[0])->next(!memCalls[0]))& ((floor1&!calls_c[1])->next(!memCalls[1]))& ((floor2&!calls_c[2])->next(!memCalls[2]))& ((floor3&!calls_c[3])->next(!memCalls[3]))
G moving->next((!moving)<->(atFloorThatCalled|edged_floor))
G ((goingUp -> next (!goingDown) ) & (goingDown -> next (!goingUp) ))
G moving -> next ((!moving)<->(atDesignatedFloor|edged_floor)) 
G (calls_c[0] & (!memCalls[0]) -> next (memCalls[0]) ) & (calls_c[1] & (!memCalls[1]) -> next (memCalls[1]) ) & (calls_c[2] & (!memCalls[2]) -> next (memCalls[2]) ) & (calls_c[3] & (!memCalls[3]) -> next (memCalls[3]) )
G ((floor0 & handleFloor & next (!handleFloor)) -> next (!memCalls[0]) ) & ((floor1 & handleFloor & next (!handleFloor)) -> next (!memCalls[1]) ) & ((floor2 & handleFloor & next (!handleFloor)) -> next (!memCalls[2]) ) & ((floor3 & handleFloor & next (!handleFloor)) -> next (!memCalls[3]) )
G ((!(calls_c[0] & !memCalls[0])) & !(floor0 & handleFloor & next (!handleFloor))) -> (next (memCalls[0]) = memCalls[0]) & ((!(calls_c[1] & !memCalls[1])) & !(floor0 & handleFloor & next (!handleFloor))) -> (next (memCalls[1]) = memCalls[1]) & ((!(calls_c[2] & !memCalls[2])) & !(floor0 & handleFloor & next (!handleFloor))) -> (next (memCalls[2]) = memCalls[2]) & ((!(calls_c[3] & !memCalls[3])) & !(floor0 & handleFloor & next (!handleFloor))) -> (next (memCalls[3]) = memCalls[3])
G (moving&!returnTo0) -> next ((!moving)<->(atDesignatedFloor|edged_floor)) 
G (calls0_c & (!memCalls[0]) -> next (memCalls[0]) ) & (calls1_c & (!memCalls[1]) -> next (memCalls[1]) ) & (calls2_c & (!memCalls[2]) -> next (memCalls[2]) ) & (calls3_c & (!memCalls[3]) -> next (memCalls[3]) )
G ((!(calls0_c & !memCalls[0])) & !(floor0 & handleFloor & next (!handleFloor))) -> (next (memCalls[0]) = memCalls[0]) & ((!(calls1_c & !memCalls[1])) & !(floor1 & handleFloor & next (!handleFloor))) -> (next (memCalls[1]) = memCalls[1]) & ((!(calls2_c & !memCalls[2])) & !(floor2 & handleFloor & next (!handleFloor))) -> (next (memCalls[2]) = memCalls[2]) & ((!(calls3_c & !memCalls[3])) & !(floor3 & handleFloor & next (!handleFloor))) -> (next (memCalls[3]) = memCalls[3])
G moving->(next(!moving)->(atDesignatedFloor|atEdgedFloor))
pRespondsToS(driveMotor = STOP, driveMotor != STOP | next(velocity) < velocity | velocity=0)
pRespondsToS(driveMotor != STOP, driveMotor = STOP | next(velocity) > velocity | velocity=5)
G next(initDone) = (mode = INIT | initDone)
G next(a)!=next(b)
G next(from) != next(to)
G (swapRedAndBlueAsms & task = SWAP_RED_AND_BLUE) -> ((fromColor = RED -> next(fromColor) = BLUE) & (fromColor = BLUE -> next(fromColor) = RED))
G next(assign(from, fromColor))
G next(assign(to, toColor))
G next(hanoiAssign(hanoiFrom, hanoiFromColor))
G next(hanoiAssign(hanoiTo, hanoiToColor))
G next(hanoiFrom) != next(hanoiTo)
G (swapRedAndBlueAsms & task = SWAP_RED_AND_BLUE) -> isMoving & ((fromColor = RED -> next(fromColor) = BLUE) & (fromColor = BLUE -> next(fromColor) = RED))
G task = HANOI & hanoiIsMoving -> ( (hanoiFrom = 0 -> next(r0) = r0 - 1) & (hanoiFrom = 1 -> next(r1) = r1 - 1) & (hanoiFrom = 2 -> next(r2) = r2 - 1) & (hanoiTo = 0 -> next(r0) = r0 + 1) & (hanoiTo = 1 -> next(r1) = r1 + 1) & (hanoiTo = 2 -> next(r2) = r2 + 1) & (hanoiFrom != 0 & hanoiTo != 0 -> next(r0) = r0) & (hanoiFrom != 1 & hanoiTo != 1 -> next(r1) = r1) & (hanoiFrom != 2 & hanoiTo != 2 -> next(r2) = r2) )
G next(secondStep) = (mode = INIT)
