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 (verMot = SLEEP -> spec_currentColor = next(spec_currentColor))
G (verMot = MOVE -> color = next(spec_currentColor))
G (spec_dropping = next(spec_dropping) <-> verMot = SLEEP & horMot = SLEEP)
motSpeed = LEVEL1 & !spec_dropping
!spec_dropping & motSpeed = LEVEL1 & spec_pausing = GO & direction = RIGHT
G (spec_pausing = GO & !spec_dropping & starting_pos = NO & verhor_dontmove <-> botMot = RETURN)
G (!spec_dropping & starting_pos = YES & color = BLACK -> allsleep)
G (color = BLACK | spec_dropping -> verMot = SLEEP)
G (spec_pausing = GO & !spec_dropping & starting_pos = YES & nonemove & color != BLACK <-> verMot = MOVE)
G (edge = YES <-> direction != next(direction))
G (spec_pausing = GO & spec_dropping & detect != spec_currentColor & verhor_dontmove <-> botMot = SEEK)
G (spec_pausing = GO & spec_dropping & detect = spec_currentColor & verhor_dontmove <-> horMot = MOVE)
G (speedButton = PRESS & PREV(speedButton = RELEASE) <-> spec_speedButtonValidPressed)
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 (haltButton = PRESS & PREV(haltButton = RELEASE) <-> spec_pauseButtonValidPressed)
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_pausing = PAUSE -> allsleep)
!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 & 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))
!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 & 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))
respondsTo(color!=BLACK,(horMot=MOVE&detect=spec_currentColor))
GF (horMot=MOVE)
spec_state=S0
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)))
GF (spec_state=S0|spec_state=S1)
G (haltButton = PRESS & PREV(haltButton = RELEASE) <-> spec_haltButtonValidPressed = true)
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)
respondsTo(spec_haltButtonValidPressed=true&spec_pausing=go,(spec_haltButtonValidPressed=true))
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 (spec_allsleep = true <-> verMot = SLEEP & horMot = SLEEP & botMot = STOP)
motSpeed = LEVEL1 & spec_stage = WAIT & spec_pausing = go
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 (((ack_ver_hor = SLEEP & spec_stage = DROP) | ((ack_bot = MOVE | (ack_bot = SLEEP & PREV(spec_pausing = pause))) & spec_stage = FROMANGLE)) & spec_pausing = go -> botMot = INITPOS & next(spec_stage) = FROMANGLE)
G (spec_finished_cycle <-> ack_bot = SLEEP & PREV(spec_pausing = go) & spec_stage = FROMANGLE & spec_pausing = go)
G (spec_finished_cycle -> spec_allsleep = true & next(spec_stage) = WAIT)
G (spec_finished_cycle <-> reduce_num_of_cubes = REDUCE)
G (speedButton = PRESS & PREV(speedButton = RELEASE) <-> spec_speedButtonValidPressed = true)
G (spec_speedButtonValidPressed = true & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL2)
G (spec_speedButtonValidPressed = true & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL3)
G (spec_speedButtonValidPressed = true & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL1)
G (spec_speedButtonValidPressed = false & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL1)
G (spec_speedButtonValidPressed = false & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL2)
G (spec_speedButtonValidPressed = false & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL3)
G ((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)
respondsTo(spec_haltButtonValidPressed=true&spec_pausing=GO,(spec_haltButtonValidPressed=true))
G (spec_pausing = PAUSE | ack_ver_hor = MOVE -> spec_allsleep = true & next(spec_stage) = spec_stage)
motSpeed = LEVEL1 & spec_stage = WAIT & spec_pausing = GO
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 | 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_stage = TOANGLERIGHT | spec_stage = TOANGLELEFT) & spec_pausing = GO & detect = spec_currentColor -> verMot = SLEEP & horMot = MOVE & botMot = STOP & next(spec_stage) = DROP )
G (((ack_ver_hor = SLEEP & spec_stage = DROP) | ((ack_bot = MOVE | (ack_bot = SLEEP & PREV(spec_pausing = PAUSE))) & spec_stage = FROMANGLE)) & spec_pausing = GO -> botMot = INITPOS & next(spec_stage) = FROMANGLE)
G (spec_finished_cycle <-> ack_bot = SLEEP & PREV(spec_pausing = GO) & spec_stage = FROMANGLE & spec_pausing = GO)
!spec_dropping & motSpeed = LEVEL1
G (!spec_dropping & starting_pos = NO & verhor_dontmove <-> botMot = RETURN)
G (!spec_dropping & starting_pos = YES & nonemove & color != BLACK <-> verMot = MOVE)
G (spec_dropping & detect != spec_currentColor & verhor_dontmove <-> botMot = SEEK)
G (spec_dropping & detect = spec_currentColor & verhor_dontmove <-> horMot = MOVE)
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 (spec_stage != WAIT -> next(botMotColor) = botMotColor)
store_place = false & motSpeed = LEVEL1 & spec_stage = WAIT & spec_pausing = go
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_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 (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 (store_place = true <-> (spec_stage = TOANGLERIGHT | spec_stage = TOANGLELEFT) & spec_pausing = go & detect = botMotColor)
G (ack_bot = SLEEP & PREV(spec_pausing = go) & spec_stage = FROMANGLE & spec_pausing = go -> spec_allsleep & next(spec_stage) = WAIT)
motSpeed = LEVEL1
G (color = BLACK & spec_nonemove & spec_allsleep -> spec_allsleep)
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)
respondsTo(color!=BLACK,(detect=spec_currentColor&horMot=MOVE))
G (verMot = SLEEP -> spec_currentColor = next(spec_currentColor) & spec_dropping = next(spec_dropping))
G (spec_dropping -> verMot = SLEEP)
G (horMot = MOVE <-> spec_dropping & detect = spec_currentColor)
G (color = BLACK & !spec_dropping -> spec_allsleep)
G (color != BLACK & !spec_dropping -> verMot = MOVE & next(spec_currentColor) = color & next(spec_dropping))
spec_state_1=S0
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_dropping = next(spec_dropping) <-> verMot = SLEEP & !(PREV(botMot = RETURN) & ack_bot = SLEEP))
G (ack_ver = MOVE | ack_hor = MOVE -> spec_allsleep)
G (!spec_dropping -> botMot = STOP & horMot = SLEEP)
G (ack_ver = SLEEP & PREV(ack_ver = MOVE) & spec_dropping -> botMot = SEEK)
spec_state__seek=S0
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_dropping & detect = spec_currentColor & PREV(botMot != STOP) <-> horMot = MOVE)
G (spec_dropping = next(spec_dropping) <-> verMot = SLEEP )
G (color = BLACK & !spec_dropping -> allsleep)
G ((nonemove & spec_dropping) | (PREV(botMot = SEEK) & onlybotmoves & detect != spec_currentColor) -> botMot = SEEK)
G (spec_dropping & onlybotmoves & detect = spec_currentColor & PREV(botMot = SEEK) -> horMot = MOVE)
G(spec_prevBotMotReturn<->PREV(botMot = RETURN))
G (spec_dropping = next(spec_dropping) <-> verMot = SLEEP & !(spec_prevBotMotReturn & nonemove))
G (color != BLACK & !spec_dropping -> verMot = MOVE & next(spec_currentColor) = color)
G ((nonemove & spec_dropping & PREV(ack_hor != MOVE)) | (PREV(botMot = SEEK) & onlybotmoves & detect != spec_currentColor) -> botMot = SEEK)
G (spec_dropping & onlybotmoves & detect = spec_currentColor & PREV(botMot = SEEK) <-> horMot = MOVE)
G (nonemove & PREV(ack_hor = MOVE) & spec_dropping -> botMot = RETURN)
spec_state_return=S0
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)))
GF (spec_state_return=S0|spec_state_return=S1|spec_state_return=S3)
G (spec_prevBotMotReturn<->PREV(botMot = RETURN))
G (spec_prevBotMotSeek<->PREV(botMot = SEEK))
G ((nonemove & spec_dropping & PREV(ack_hor != MOVE)) -> botMot = SEEK)
spec_state_seek=S0
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)))
GF (spec_state_seek=S0|spec_state_seek=S1|spec_state_seek=S3)
G (spec_dropping = next(spec_dropping) <-> verMot = SLEEP & !(spec_prevBotMotReturn & ack_bot = SLEEP))
G (nonemove & spec_dropping & PREV(ack_hor != MOVE)-> botMot = SEEK)
G (nonemove & spec_dropping & PREV(ack_ver = MOVE)-> botMot = SEEK)
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)))
GF (spec_state_return=S0|spec_state_return=S2)
G (spec_prevBotMotReturn & ack_bot = SLEEP -> allsleep)
G (num_of_cubes = ZERO -> allsleep)
G (!spec_dropping & starting_pos = YES & PREV(botMot = RETURN) <-> reduce_num_of_cubes = REDUCE)
G (num_of_cubes = NOTZERO & !spec_dropping & starting_pos = NO & verhor_dontmove <-> botMot = RETURN)
G (num_of_cubes = NOTZERO & !spec_dropping & starting_pos = YES & nonemove & color != BLACK <-> verMot = MOVE)
G (num_of_cubes = NOTZERO & spec_dropping & detect != spec_currentColor & verhor_dontmove <-> botMot = SEEK)
G (num_of_cubes = NOTZERO & spec_dropping & detect = spec_currentColor & verhor_dontmove <-> horMot = MOVE)
elevMot=STOP
GF (elevMot=FWD)
GF (floor=LOWER->elevMot=FWD)
GF (floor=UPPER->elevMot=BWD)
balancer=STP
G (!isReady -> balancer=STP)
G ((balancer=FWD) -> (frontDistSense=CLEAR))
G ((balancer=BWD) -> (backDistSense=CLEAR))
GF (spec_mode=AUTO->balancer=FWD)
spec_blockedState=S0
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))))
GF (spec_mode=AUTO->(spec_blockedState=S0|spec_blockedState=S2))
spec_mode=AUTO
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) )
balancerSpeed=REGULAR
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 ((spec_mode=MANUAL) -> ((!bluetoothDrivingCmd) -> ( (PREV(spec_manualCmd=STP) -> spec_manualCmd=STP) & (PREV(spec_manualCmd=FWD) -> spec_manualCmd=FWD) & (PREV(spec_manualCmd=BWD) -> spec_manualCmd=BWD) & (PREV(spec_manualCmd=TURN_LEFT) -> spec_manualCmd=TURN_LEFT) & (PREV(spec_manualCmd=TURN_RIGHT) -> spec_manualCmd=TURN_RIGHT) )))
G ((spec_mode=MANUAL) -> ((spec_manualCmd=FWD) -> ((frontDistSense=CLEAR & isReady)-> balancer=FWD)) )
G ((spec_mode=MANUAL) -> ((spec_manualCmd=BWD) -> ((backDistSense=CLEAR & isReady) -> balancer=BWD)) )
G ((spec_mode=MANUAL) -> ((spec_manualCmd=TURN_RIGHT) -> (isReady -> balancer=TURN_RIGHT)) )
G ((spec_mode=MANUAL) -> ((spec_manualCmd=TURN_LEFT) -> (isReady -> balancer=TURN_LEFT)) )
G ((spec_mode=MANUAL) -> ((spec_manualCmd=STP | (spec_manualCmd=FWD & frontDistSense=BLOCKED) | (spec_manualCmd=BWD & backDistSense=BLOCKED)) -> (isReady -> balancer=STP)) )
GF (balancer=FWD)
GF (balancer=TURN_RIGHT|balancer=TURN_LEFT)
G ((isReady & frontDistSense=CLEAR) -> balancer=FWD)
G ((distSense=BLOCKED & isReady) -> !(balancer=FWD))
G ((distSense=CLEAR & isReady) -> (balancer=FWD))
G ((balancer=FWD) -> next(!(balancer=TURN_RIGHT | balancer=TURN_LEFT)))
G ((distSense=BLOCKED & balancer=STP & isReady) -> next(!(balancer=STP)))
G ((balancer=FWD) -> (distSense=CLEAR))
GF (bluetoothCmd=AUTO->balancer=FWD)
G ((bluetoothCmd=AUTO) -> ((balancer=FWD) -> next((bluetoothCmd=AUTO) -> !(balancer=TURN_RIGHT | balancer=TURN_LEFT))))
G ((bluetoothCmd=AUTO) -> ((distSense=CLEAR & isReady) -> (balancer=FWD)))
G ((bluetoothCmd=AUTO) -> ((distSense=BLOCKED & balancer=STP & isReady) -> next(!(balancer=STP))))
G ((bluetoothCmd=FWD) -> ((distSense=CLEAR & isReady)-> balancer=FWD))
G ((bluetoothCmd=BWD) -> (isReady -> balancer=BWD))
G ((bluetoothCmd=TURN_RIGHT) -> (isReady -> balancer=TURN_RIGHT))
G ((bluetoothCmd=TURN_LEFT) -> (isReady -> balancer=TURN_LEFT))
G ((bluetoothCmd=NOP) -> (isReady -> balancer=STP))
G ((balancerStatus=OK) -> (bluetoothStatus=OK))
G ((balancerStatus=FELL) -> (bluetoothStatus=FELL))
GF (bluetoothCmd=AUTO->(balancer=TURN_RIGHT|balancer=TURN_LEFT))
G ((bluetoothCmd=AUTO) -> ((frontDistSense=CLEAR & isReady) -> (balancer=FWD)))
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))))
GF (bluetoothCmd=AUTO->(spec_blockedState=S0|spec_blockedState=S2))
G ((bluetoothCmd=FWD) -> ((frontDistSense=CLEAR & isReady)-> balancer=FWD))
G ((bluetoothCmd=BWD) -> ((backDistSense=CLEAR & isReady) -> balancer=BWD))
G ((bluetoothCmd=STP | (bluetoothCmd=FWD & frontDistSense=BLOCKED) | (bluetoothCmd=BWD & backDistSense=BLOCKED)) -> (isReady -> balancer=STP))
spec_moveAwayFromFrontObstacleState=S0
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))))
spec_moveAwayFromBackObstacleState=S0
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))))
spec_forwardingState=S0
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))))
spec_backwardingState=S0
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))))
spec_specState = Q0
spec_turnState = T0
spec_nextMoveMode = FWD
GF (spec_nextMoveMode=FWD)
G((Obstacle = BLOCKED) -> (!(spec_nextMoveMode = FWD)))
G(((spec_nextMoveMode = BWD) & next(spec_nextMoveMode = FWD)) <-> next(LeftMotor = FWD & RightMotor = BWD))
G(((spec_nextMoveMode = FWD) & next(spec_nextMoveMode = BWD)) <-> next(LeftMotor = BWD & RightMotor = FWD))
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 = Q2 & spec_nextMoveMode = FWD & next(spec_nextMoveMode = BWD)))
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_nextMoveMode = TURN_RIGHT | spec_nextMoveMode = TURN_LEFT) & Y(spec_nextMoveMode = FWD) & spec_turnState = T0) -> next(spec_turnState) = T1)
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 ((spec_turnState = T0 & next(spec_turnState) = T1 & spec_nextMoveMode = TURN_RIGHT) <-> (LeftMotor = CALIB_TURN_RIGHT & RightMotor = CALIB_TURN_RIGHT))
G ((spec_turnState = T0 & next(spec_turnState) = T1 & spec_nextMoveMode = TURN_LEFT) <-> (LeftMotor = CALIB_TURN_LEFT & RightMotor = CALIB_TURN_LEFT))
G ((next(spec_turnState) = T2) <-> (LeftMotor = FWD & RightMotor = TURN_FWD))
G ((spec_turnState = T2) <-> (LeftMotor = BWD & RightMotor = TURN_BWD))
G ((spec_turnState = T3 & next(spec_turnState = T0) & Y(Y(spec_nextMoveMode = TURN_RIGHT))) <-> (LeftMotor = CALIB_FWD_RIGHT & RightMotor = CALIB_FWD_RIGHT))
G ((spec_turnState = T3 & next(spec_turnState = T0) & Y(Y(spec_nextMoveMode = TURN_LEFT))) <-> (LeftMotor = CALIB_FWD_LEFT & RightMotor = CALIB_FWD_LEFT))
G((InputMoveMode = FWD & 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) <-> (OutputMoveMode = TURN_LEFT_2))
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 = 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 = TURN_LEFT_2 & Obstacle = CLEAR) -> (OutputMoveMode = 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 ((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((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(!(state = Q3))
G((Obstacle = BLOCKED) -> !(nextMoveMode = FWD))
G((Y(nextMoveMode = BWD) & (nextMoveMode = FWD)) <-> (LeftMotor = FWD & RightMotor = BWD))
G((Y(nextMoveMode = FWD) & (nextMoveMode = BWD)) <-> (LeftMotor = BWD & RightMotor = FWD))
GF (nextMoveMode=FWD)
G ((nextMoveMode = BWD) -> (Y(nextMoveMode = FWD) | Y(nextMoveMode = BWD)))
G (Y (nextMoveMode = TURN_LEFT_2) -> !(nextMoveMode = BWD))
G ((Y(nextMoveMode = FWD) & nextMoveMode = TURN_LEFT_1) <-> (LeftMotor = CALIB_TURN & RightMotor = CALIB_TURN))
G ( (Y(nextMoveMode = BWD)) -> (nextMoveMode != TURN_LEFT_1)) 
G ((Y(nextMoveMode = FWD) & Y(Y(nextMoveMode = TURN_LEFT_2))) <-> (LeftMotor = CALIB_FWD & RightMotor = CALIB_FWD))
G (Y(nextMoveMode = TURN_LEFT_1) <-> nextMoveMode = TURN_LEFT_2)
G (Y(nextMoveMode = TURN_LEFT_1) -> (LeftMotor = FWD & RightMotor = TURN_FWD))
G (Y(nextMoveMode = TURN_LEFT_2) -> (LeftMotor = BWD & RightMotor = TURN_BWD))
G (!(Y(nextMoveMode = TURN_LEFT_1) | Y(nextMoveMode = TURN_LEFT_2)) -> !(LeftMotor = TURN_BWD | RightMotor = TURN_BWD | LeftMotor = TURN_FWD | RightMotor = TURN_FWD))
spec_search = M0
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_state = Q3))
G(HeadMotor = STOP)
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(((Obstacle = BLOCKED) & !(Y(Y(spec_nextMoveMode = TURN_LEFT_2)))) -> (!(spec_nextMoveMode = FWD)))
G((Y(spec_nextMoveMode = BWD) & (spec_nextMoveMode = FWD)) <-> (LeftMotor = FWD & RightMotor = BWD))
G((Y(spec_nextMoveMode = FWD) & (spec_nextMoveMode = BWD)) <-> (LeftMotor = BWD & RightMotor = FWD))
G ((spec_nextMoveMode = BWD) -> (Y(spec_nextMoveMode = FWD) | Y(spec_nextMoveMode = BWD)))
G (Y (spec_nextMoveMode = TURN_LEFT_2) -> !(spec_nextMoveMode = BWD))
G ((Y(spec_nextMoveMode = FWD) & spec_nextMoveMode = TURN_LEFT_1) <-> (LeftMotor = CALIB_TURN & RightMotor = CALIB_TURN))
G ( (Y(spec_nextMoveMode = BWD)) -> (spec_nextMoveMode != TURN_LEFT_1)) 
G ((Y(spec_nextMoveMode = FWD) & Y(Y(spec_nextMoveMode = TURN_LEFT_2))) <-> (LeftMotor = CALIB_FWD & RightMotor = CALIB_FWD))
G (Y(spec_nextMoveMode = TURN_LEFT_1) <-> spec_nextMoveMode = TURN_LEFT_2)
G (Y(spec_nextMoveMode = TURN_LEFT_1) -> (LeftMotor = FWD & RightMotor = TURN_FWD))
G (Y(spec_nextMoveMode = TURN_LEFT_2) -> (LeftMotor = BWD & RightMotor = TURN_BWD))
G (!(Y(spec_nextMoveMode = TURN_LEFT_1) | Y(spec_nextMoveMode = TURN_LEFT_2)) -> !(LeftMotor = TURN_BWD | RightMotor = TURN_BWD | LeftMotor = TURN_FWD | RightMotor = TURN_FWD))
search = M0 & spec_state = Q0
GF (search=M0)
G(!(spec_state = Q2 & spec_nextMoveMode = FWD & next(spec_nextMoveMode = BWD)))
G(((spec_nextMoveMode = TURN_LEFT_1) | (spec_nextMoveMode = TURN_LEFT_2)) -> next(spec_state = Q0))
G ((Y(search = M0) & Noise = NOISE & Heading != next_head & Button != PRESSED) -> (search = M1))
G((Y(search = M1) & Heading = next_head) -> search = M0)
G((Y(search = M1) & Heading != next_head) -> search = M1)
G ((Button = PRESSED & Y(search = M0)) -> (next(next_head) = Heading))
G ((Button = FREE | Y(search = M1)) -> (next(next_head) = next_head))
G((next(Obstacle = BLOCKED) & !((Y(spec_nextMoveMode = TURN_LEFT_2)))) -> next(!(spec_nextMoveMode = FWD)))
G ((spec_nextMoveMode = 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) <-> next(spec_nextMoveMode = TURN_LEFT_2))
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 = FWD) & next(spec_nextMoveMode = TURN_LEFT_1)) <-> next(LeftMotor = CALIB_TURN & RightMotor = CALIB_TURN))
G (((spec_nextMoveMode = FWD) & (Y(spec_nextMoveMode = TURN_LEFT_2))) <-> next(LeftMotor = CALIB_FWD & RightMotor = CALIB_FWD))
G ( ((spec_nextMoveMode = BWD)) -> next(spec_nextMoveMode != TURN_LEFT_1))
spec_nextHead = SO
G(spec_nextMoveMode = TURN_LEFT -> next(spec_specState = Q0))
respondsTo((Noise=NOISE),(Heading=spec_nextHead))
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_nextMoveMode = TURN_LEFT & Y(spec_nextMoveMode = FWD) & spec_turnState = T0) -> next(spec_turnState) = T1)
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 ((spec_turnState = T0 & next(spec_turnState) = T1) <-> (LeftMotor = CALIB_TURN & RightMotor = CALIB_TURN))
G (next(spec_turnState) = T2 <-> (LeftMotor = FWD & RightMotor = TURN_FWD))
G (spec_turnState = T2 <-> (LeftMotor = BWD & RightMotor = TURN_BWD))
G ((spec_turnState = T3 & next(spec_turnState = T0)) <-> (LeftMotor = CALIB_FWD & RightMotor = CALIB_FWD))
specState = Q0
turnState = T0
nextHead = SO
nextMoveMode = FWD
G((Obstacle = BLOCKED) -> (!(nextMoveMode = FWD)))
G(((nextMoveMode = BWD) & next(nextMoveMode = FWD)) <-> next(LeftMotor = FWD & RightMotor = BWD))
G(((nextMoveMode = FWD) & next(nextMoveMode = BWD)) <-> next(LeftMotor = BWD & RightMotor = FWD))
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 = Q2 & nextMoveMode = FWD & next(nextMoveMode = BWD)))
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))
respondsTo((Noise=NOISE),(Heading=nextHead))
G (next(turnState) = T0 -> (turnState = T0 | turnState = T3))
G ((turnState = T0 & !(nextMoveMode = TURN_RIGHT | nextMoveMode = TURN_LEFT)) -> next(turnState) = T0)
G (((nextMoveMode = TURN_RIGHT | nextMoveMode = TURN_LEFT) & Y(nextMoveMode = FWD) & turnState = T0) -> next(turnState) = T1)
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 ((turnState = T0 & next(turnState) = T1) <-> (LeftMotor = CALIB_TURN & RightMotor = CALIB_TURN))
G ((next(turnState) = T2 & nextMoveMode = TURN_RIGHT) <-> (LeftMotor = FWD & RightMotor = TURN_FWD))
G ((turnState = T2 & Y(nextMoveMode = TURN_RIGHT)) <-> (LeftMotor = BWD & RightMotor = TURN_BWD))
G ((next(turnState) = T2 & nextMoveMode = TURN_LEFT) <-> (LeftMotor = TURN_FWD & RightMotor = FWD))
G ((turnState = T2 & Y(nextMoveMode = TURN_LEFT)) <-> (LeftMotor = TURN_BWD & RightMotor = BWD))
G ((turnState = T3 & next(turnState = T0)) <-> (LeftMotor = CALIB_FWD & RightMotor = CALIB_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)
( spec_policy=SEEKING )
GF (spec_policy=PARKED)
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)->!(throttle = FWD))
G ((sideSense = BLOCKED) -> !((steer =RIGHT) &(throttle=FWD)))
G(((obstacle=BLOCKED) &(spec_policy=MEASURING |spec_policy=SEEKING))->(next(spec_policy) = SEEKING))
G((obstacle=BLOCKED)->(parkCommand=STOP))
G ((spec_policy = SEEKING & parkResult=NA) -> (throttle != STOP))
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 = MEASURING)|(spec_policy=SEEKING & PREV(spec_policy=MEASURING)))) & (obstacle = CLEAR) &(parkResult =PARALLEL)) -> (next(spec_policy) = PARKING_0) & (throttle = STOP) & (parkCommand = STOP) & steer = RIGHT)
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))
( policy=SEEKING )
GF (policy=PARKED)
G((policy = SEEKING)-> (next(policy)=SEEKING| next(policy) = MEASURING| next(policy) = PARKING_0))
G ((policy = SEEKING) -> ((throttle = FWD | throttle = STOP | throttle = BWD)))
G((policy = MEASURING)-> (next(policy)=SEEKING| next(policy) = MEASURING| next(policy) = PARKING_0))
G ((policy = MEASURING) -> (throttle != BLOCKING_BWD & parkCommand != START & (steer = CENTER | steer = EASY_LEFT | steer = EASY_RIGHT)))
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 = CLEAR) & (policy=SEEKING) & parkResult = NA)->(throttle = FWD))
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 & 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=SEEKING & obstacle = CLEAR & sideSense = CENTERED & (PREV(sideSense != CLOSE) & PREV(sideSense != FAR))) -> (steer=CENTER))
G((policy = SEEKING & obstacle = CLEAR & PREV(sideSense = FAR) & sideSense = CENTERED) -> (steer=EASY_LEFT & next(steer)=CENTER))
G((policy = SEEKING & obstacle = CLEAR & PREV(sideSense = CLOSE) & sideSense = CENTERED) -> (steer=EASY_RIGHT & next(steer)=CENTER))
G((policy=MEASURING & 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) & (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 = MEASURING & sideSense = PARALLEL_PARKING)|(policy=SEEKING & PREV(sideSense = PARALLEL_PARKING) & PREV(policy=MEASURING)))) & (obstacle = CLEAR) &(parkResult =PARALLEL)) -> (next(policy) = PARKING_0) & (throttle = BLOCKING_FWD) & (parkCommand = STOP) )
G ((policy = 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))
( policy=SEEKING)
GF (policy=PARKED&colorSense=GREEN)
G ((policy = SEEKING & obstacle = CLEAR) -> (!(steer = RIGHT | steer = LEFT )))
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 & obstacle = CLEAR & PREV(obstacle = BLOCKED)) -> (steer=CENTER))
G((policy=SEEKING & obstacle = CLEAR & sideSense = CLOSE & PREV(obstacle = CLEAR)) -> (steer=EASY_LEFT))
G((policy=SEEKING & obstacle = CLEAR & sideSense = FAR & PREV(obstacle = CLEAR)) -> (steer=EASY_RIGHT))
G((policy=SEEKING & obstacle = CLEAR & sideSense = CENTERED & (PREV(sideSense = CENTERED)) & PREV(obstacle = CLEAR)) -> (steer=CENTER))
G((policy = SEEKING & obstacle = CLEAR & PREV(sideSense = FAR) & sideSense = CENTERED & PREV(obstacle = CLEAR)) -> (steer=EASY_LEFT))
G((policy = SEEKING & obstacle = CLEAR & PREV(sideSense = CLOSE) & sideSense = CENTERED & PREV(obstacle = CLEAR)) -> (steer=EASY_RIGHT))
G((policy=MEASURING & obstacle = CLEAR & sideSense = PARALLEL_PARKING & PREV(sideSense = PARALLEL_PARKING)) -> (steer=CENTER))
G((policy=MEASURING & obstacle = CLEAR & sideSense = PARALLEL_PARKING & PREV(sideSense = CLOSE_PARKING)) -> (steer=EASY_RIGHT))
G((policy=MEASURING & obstacle = CLEAR & sideSense = PARALLEL_PARKING & PREV(sideSense = PERPENDICULAR)) -> (steer=EASY_LEFT))
G(((policy = SEEKING) & (sideSense = CLOSE | sideSense = CENTERED | sideSense = FAR)) -> ((next(policy) = policy) & (parkCommand = STOP)))
G (((((policy = MEASURING & sideSense = PARALLEL_PARKING)|(policy=SEEKING & PREV(sideSense = PARALLEL_PARKING) & PREV(policy=MEASURING)))) & (obstacle = CLEAR) &(parkResult =PARALLEL)) -> (next(policy) = PARKING_0) & (throttle = STOP) & (parkCommand = STOP) )
G ((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 (obstacle=BLOCKED -> ( !(throttle = FWD) ))
G (((obstacle = CLEAR) & (sideSense = CLEAR)) -> (steer = CENTER))
GF ((throttle=FWD)&(steer=CENTER))
spec_b2f=S0
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)))
spec_f2b=S0
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)))
spec_policy=SEEKING & !spec_park
GF (spec_park)
G(!next(spec_park) -> !next(spec_policy = PARKED))
G(next(spec_park) -> next(spec_policy = PARKED))
respondsTo(!(spec_policy=PARKED),!(throttle=STOP))
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) & (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)))
( spec_policy=SEEKING |( spec_policy=MEASURING & parkCommand = START))
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 = 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((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 = CLEAR) & (spec_policy=SEEKING) & parkResult = NA)->(throttle = FWD))
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 & obstacle = CLEAR & sideSense = CLOSE) -> (steer=EASY_LEFT))
G((spec_policy=SEEKING & obstacle = CLEAR & sideSense = FAR) -> (steer=EASY_RIGHT))
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 = CLOSE_PARKING) -> (steer=EASY_LEFT))
G((spec_policy=MEASURING & obstacle = CLEAR & sideSense = PERPENDICULAR) -> (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) & (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 = MEASURING & sideSense = PARALLEL_PARKING)|(spec_policy=SEEKING & PREV(sideSense = PARALLEL_PARKING) & PREV(spec_policy=MEASURING)))) & (obstacle = CLEAR) &(parkResult =PARALLEL)) -> (next(spec_policy) = PARKING_0) & (throttle = STOP) & (parkCommand = STOP) )
G ((spec_policy = 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 = SEEKING & obstacle = CLEAR) -> (!(steer = RIGHT | steer = LEFT )))
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 = MEASURING & sideSense = PARALLEL_PARKING)|(spec_policy=SEEKING & PREV(sideSense = PARALLEL_PARKING) & PREV(spec_policy=MEASURING))) & (obstacle = CLEAR) &(parkResult =PARALLEL)) -> (next(spec_policy) = PARKING_0) & (throttle = STOP) & (parkCommand = STOP) )
G (((spec_policy = 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))
( spec_policy=SEEKING)
GF (spec_policy=PARKED&colorSense=GREEN)
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 = 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))
GF ((spec_policy=PARKED&colorSense=GREEN)|command!=AUTO)
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(((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 & parkResult=NA & command=AUTO) -> (throttle != STOP))
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 = CLOSE_PARKING & command=AUTO) -> (steer=EASY_LEFT))
G((spec_policy=MEASURING & obstacle = CLEAR & sideSense = PERPENDICULAR & command=AUTO) -> (steer=EASY_RIGHT))
G((spec_policy=MEASURING & obstacle = CLEAR & sideSense = PARALLEL_PARKING & PREV(sideSense = PARALLEL_PARKING) & command=AUTO) -> (steer=CENTER))
G((spec_policy=MEASURING & obstacle = CLEAR & sideSense = PARALLEL_PARKING & PREV(sideSense = CLOSE_PARKING) & command=AUTO) -> (steer=EASY_RIGHT))
G((spec_policy=MEASURING & obstacle = CLEAR & sideSense = PARALLEL_PARKING & PREV(sideSense = PERPENDICULAR) & command=AUTO) -> (steer=EASY_LEFT))
G (((spec_policy = 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 = MEASURING & sideSense = PARALLEL_PARKING)|(spec_policy=SEEKING & PREV(sideSense = PARALLEL_PARKING) & PREV(spec_policy=MEASURING)))) & (obstacle = CLEAR) &(parkResult =PARALLEL) & command=AUTO) -> (next(spec_policy) = PARKING_0) & (throttle = STOP) & (parkCommand = STOP) )
G ((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))
(carStatus = SEEKING_FOR_PS & sensorMot = FWD & spec_counter = 0)
G ((obstacle = BLOCKED) -> (Stop) )
G ((obstacle = BLOCKED ) -> (keepCarStatus & keepCounterValue ) )
G(movingBwd -> sensorMot = BWD)
G(movingFwd -> sensorMot = FWD)
GF (carStatus=PARKED)
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 = SEEKING_FOR_PS & (weGotSideSensorMeasuringValues) & obstacle = CLEAR ) -> ( (engineMot = STOP) & (next(carStatus = MEASURE_PARKING)) & (next(spec_counter) = 1) ) )
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((spec_counter <= counterLimit))
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) ))
respondsTo(carStatus=MEASURE_PARKING,(carStatus=PREPARE_FOR_PARALLEL_PARKING|carStatus=ALIGN_BEFORE_PARKING))
G((carStatus = PREPARE_FOR_PARALLEL_PARKING)-> ((steeringMot = ALIGN_RIGHT | steeringMot = CENTER | steeringMot = ALIGN_LEFT) & (engineMot = FWD | engineMot = STOP)) )
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) ) -> (keepCarStatus) )
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) ))
respondsTo(carStatus=PREPARE_FOR_PARALLEL_PARKING,(spec_counter=preparingParallelSteps))
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 = ALIGN_BEFORE_PARKING) -> keepParkingType)
respondsTo((carStatus=ALIGN_BEFORE_PARKING),(carStatus=PERPENDICULAR|carStatus=PARALLEL))
G((obstacle = BLOCKED & carStatus = PARALLEL & (PREV(sensorMot = BWD) & !movingFwd) ) -> (sensorMot = BWD))
G((carStatus = PARALLEL) -> ((steeringMot = MAX_RIGHT | steeringMot = CENTER | steeringMot = MAX_LEFT) & (engineMot = PARKING_BWD | engineMot = STOP)) )
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) -> ((steeringMot = MAX_RIGHT | steeringMot = CENTER | steeringMot = MAX_LEFT) & (engineMot = PARKING_FWD | engineMot = STOP | engineMot = PREPARE_PERPENDICULAR_BWD | engineMot = PERPENDICULAR_BWD)) )
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((obstacle = BLOCKED & (carStatus = PARALLEL | carStatus = ALIGN_BEFORE_PARKING) & (PREV(sensorMot = BWD) & !movingFwd) ) -> (sensorMot = 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 != BYPASSING & PREV(obstacle = CLEAR) & obstacle = BLOCKED ) -> (spec_obstacleCounter = 0))
G((obstacle = BLOCKED & carStatus != BYPASSING & (PREV(sensorMot = BWD) & !movingFwd) ) -> (sensorMot = BWD))
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 = MEASURE_PARKING & (weGotSideSensorSeekingValues) & obstacle = CLEAR & spec_counter < suitableParallelPS & capablePerpendicular ) -> (next(carStatus = PERPENDICULAR) & next(spec_counter = firstPhase) & sensorMot = BWD & Stop ) )
respondsTo(carStatus=MEASURE_PARKING,(carStatus=PREPARE_FOR_PARALLEL_PARKING|carStatus=PERPENDICULAR))
G ((carStatus = PREPARE_FOR_PARALLEL_PARKING & spec_counter = preparingParallelSteps & obstacle = CLEAR ) -> ( (Stop) & (next(carStatus) = PARALLEL) & next(spec_counter = firstPhase) & (sensorMot = BWD) ))
G((obstacle = BLOCKED & carStatus = BYPASSING & (spec_counter = 1 | spec_counter = 2 | spec_counter = 11) & (PREV(sensorMot = BWD) & !movingFwd) ) -> (sensorMot = BWD))
G(((carStatus = SEEKING_FOR_PS | carStatus = MEASURE_PARKING) & spec_obstacleCounter < 2 & obstacle = BLOCKED ) -> (Stop & (next(spec_obstacleCounter) = spec_obstacleCounter + 1) & keepCarStatus & keepCounterValue) )
G(((carStatus = SEEKING_FOR_PS | carStatus = MEASURE_PARKING) & spec_obstacleCounter = 2 & obstacle = BLOCKED & PREV(obstacle = BLOCKED) ) -> (Stop & next(carStatus = BYPASSING) & next(spec_counter = 0) ) )
G((carStatus = BYPASSING & spec_counter < 10) -> (keepCarStatus))
G((carStatus = BYPASSING & spec_counter = 0 )-> (Stop & sensorMot = BWD) )
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 )-> (Stop & sensorMot = FWD ) )
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)))
respondsTo((carStatus=BYPASSING),(carStatus=SEEKING_FOR_PS))
stopping & !doorReq & !startTechnicalJob
G atStationWithTask -> stopping
G (!waitingForDoor & ((atStation & atEmgState & openDoorAtEmgState)| atStationWithTask)) <-> doorReq
G waitingForDoor -> stopping
G atStation & atEmgState -> stopping
G ((atEmgState & PREV(willEnterStation))|(atStation & readyToEmgBeep & atEmgState)) <-> emgBeepProcessReq
G noTasks & atBaseStation -> stopping
G noPressedStations & !atEmgState <-> countTimeSinceReqs
G (techGuyInAction & atStation -> stopping)
G !techGuyInAction & next(techGuyInAction) <-> next(startTechnicalJob)
G atGivenStation(0) -> !backwarding
G atGivenStation(3) -> !forwarding
G noTasksForward -> !forwarding
G noTasksBackward & !goToBaseStation -> !backwarding
G noTasks & atStation & !goToBaseStation -> stopping
G !atStation -> !stopping
G (!stopping -> (next(motors) = motors | next(stopping)))
G (!goToBaseStation & atStation & !atStationWithTask & !noTasks & !waitingForDoor & !techGuyInAction) -> !stopping
GF !taskAtStationZero
GF !taskAtStationOne
GF !taskAtStationTwo
GF !taskAtStationThree
GF !goToBaseStation
stopping & doorReq=NIL
G (atStation & stopAtNearestStation -> stopping)
G (doorStatus=IN_PROCESS -> doorReq=NIL)
G (atStation & stopAtNearestStation) & (doorStatus = CLOSED) & (!doorCounterIncreased) <-> openDoorReq
G ( (doorStatus = OPENED) <-> closeDoorReq)
G (techGuyInAction -> stopping)
G (PREV(!techGuyInAction) & techGuyInAction <-> startTechnicalJob )
GF forwarding
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)
pRespondsToS(noRequests & readyToBaseStation, atBaseStation)
G ( (noRequests & atBaseStation) -> stopping & updateTasks(shuttleTasksFwd, 4, 4) & updateTasks(shuttleTasksBwd, 4, 4))
G (forwarding | backwarding | stopping)
GF (noRequests)
stopping & doorReq=NIL & !startTechnicalJob & noRequests
G (atStation & (stopAtNearestStation| taskAtCurrentStation(station))) & (doorStatus = CLOSED) & (!doorCounterIncreased) <-> openDoorReq
pRespondsToS(noRequests & longTimeWithoutRequests, atBaseStation)
stopping & doorReq=NIL & noRequests & !startTechnicalJob
pRespondsToS(forwarding, noRequestsFwd)
pRespondsToS(backwarding, noRequestsBwd)
stopping & doorReq=NIL & noRequests 
stopping & noTasks
G enteringStation & taskAtCurrentStation -> stopping & satisfiesTask 
G addTasks
G keepTasksStatus
G atStation & noTasks -> stopping
GF (noTasks)
G taskWillBeFalse
that we must stop in order to satisfy Task! */ G noTasks -> stopping
GF shuttleTasks[0]=false
GF shuttleTasks[1]=false
GF shuttleTasks[2]=false
GF shuttleTasks[3]=false
G (forwarding -> next (!backwarding)) & (backwarding -> next (!forwarding))
G updateTasks
G noTasks -> stopping
G noTasksForward -> next(!forwarding)
G noTasksBackward -> next(!backwarding)
G noTasksForwardAndExistsTaskBackward -> backwarding
G noTasksBackwardAndExistsTaskForward -> forwarding
G noTasksForward -> (!forwarding)
G noTasksBackward -> (!backwarding)
G (noTaskAtCurrentStation & !noTasks) -> (!stopping)
stopping
G (!atStationWithTask & !noTasks) -> (!stopping)
G noTasks & atStation -> stopping
G noTasksBackward -> !backwarding
G (atStation & !atStationWithTask & !noTasks) -> !stopping
stopping & countTimeSinceReqs
G (!goToBaseStation & atStation & !atStationWithTask & !noTasks) -> !stopping
stopping & countTimeSinceReqs & !doorReq
G (!goToBaseStation & atStation & !atStationWithTask & !noTasks & !waitingForDoor) -> !stopping
stopping & !doorReq
G !turning
G (!stopping <-> beep = 1)
G (accelerating -> (next(mLeft) - mLeft = 1 | (mLeft = 4 & next(mLeft)=4) ))
G (slowingDown -> ((mLeft = 0 & next(mLeft)=0) | mLeft - next(mLeft) = 1 ))
G ((-1 <= next(mLeft) - mLeft) & (next(mLeft) - mLeft <= 1))
G ((-1 <= next(mRight) - mRight) & (next(mRight) - mRight <= 1))
G farFromNextCar -> (accelerating)
G ((inRange & (lastDist > sense)) -> (slowingDown))
G ((inRange & (lastDist < sense)) -> (accelerating))
G ((inRange & (lastDist = sense)) -> (mLeft = next(mLeft)))
GF (inRange | farFromNextCar | (tooClose & stopping))
G (tooClose -> (slowingDown))
G ((trnLft <-> turningLeft) & (trnRt <-> turningRight))
G (!inLane -> (next(turning) | next(stopping)))
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 ((inRange & (lastDist = sense) & inLane) -> (mLeft = next(mLeft)))
GF (inLane)
G (accelerating <-> (accelLeft | accelRight))
G (pHolds_afterQuntilR(next(turningRight | tooClose), (rightColor = white), inLane))
G (pHolds_afterQuntilR(next(turningLeft | tooClose), (leftColor = black), inLane))
G (inLane -> !next(turning))
G ((farFromNextCar) -> (accelerating))
G ((inRange & (lastDist < sense)) -> accelerating)
GF (!stopping)
stopping & !accelerating & !slowingDown
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 (laneClear -> accelerating)
G (nextCarCloser -> slowingDown)
G (nextCarFarther -> accelerating)
G (tooClose -> slowingDown)
GF (inRange | laneClear | (tooClose & stopping))
GF (inRange | laneClear)
pHolds_afterQuntilR(openningDoors,doorsAreClosed,doorsAreFullyOpened)
pHolds_afterQuntilR(closingDoors,doorsAreFullyOpened,doorsAreClosed)
G (!moving)
pHolds_afterQuntilR(goingUp,floor0,floor1)
pHolds_afterQuntilR(goingDown,floor1,floor0)
G (keepDoorsState)
(!moving) & (keepDoorsState) & (!lightIsOn) 
G !lightIsOn
G moving -> (next (lightIsOn) = !lightIsOn)
G (!moving) -> (next(!lightIsOn) )
G floor0 -> !(goingDown) 
G floor3 -> !(goingUp) 
G doorsAreClosed -> (!closingDoors) 
G doorsAreFullyOpened->(!openningDoors)
G (((!anyCalls) & (!returnTo0))| (returnTo0 & floor0)) -> !moving
G (!atDesignatedFloor)->(!openningDoors)
G ((!doorsAreClosed)->(!moving)) & (moving->keepDoorsState)
G (goingUp -> next (!goingDown)) & (goingDown -> next (!goingUp))
G moving->(next(!moving->(atDesignatedFloor|atEdgedFloor)))
G atDesignatedFloor->(!moving)
pHolds_afterQuntilR(!openningDoors,firstStateAtDesignatedFloor,seconds3)
pHolds_afterQuntilR(openningDoors,firstStateAtDesignatedFloor&seconds3,doorsAreFullyOpened)
pHolds_afterQuntilR(keepDoorsState,doorsAreFullyOpened,seconds5)
G (!(moving|anyCalls |floor0|returnTo0) | firstStateAtDesignatedFloor | openStateAtDesignatedFloor)->countTime_c
(stayInPlace) & (keepDoorsState)
G (floor0 -> (!goingDown))
G (floor3 -> (!goingUp))
G (doorsAreClosed -> (!closingDoors))
G (doorsAreFullyOpened->(!openingDoors))
G goingUp->next(goingUp|atDesignatedFloor|floor3|atEmergencyFloor)
G goingDown->next(goingDown|atDesignatedFloor|floor0|atEmergencyFloor)
G ((!anyMemCalls & !returnTo0 & !memEmergency) | (returnTo0 & floor0)) -> stayInPlace
G (!stayInPlace->keepDoorsState)
G ((!doorsAreClosed)/*|(doorsWereFullyOpened)*/)->(stayInPlace)
G (!atDesignatedFloor&!atEmergencyFloor)->keepDoorsState
G openingDoors->next((stayInPlace&(atDesignatedFloor|atEmergencyFloor)&!doorsAreFullyOpened)->openingDoors)
G closingDoors->next((stayInPlace&(atDesignatedFloor|atEmergencyFloor)&!doorsAreClosed)->closingDoors)
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 (!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 (onlyDownCalls&PREV(stayInPlace))->(goingDown|atEmergencyFloor)
G (onlyUpCalls&PREV(stayInPlace))->(goingUp|atEmergencyFloor)
G(firstStateAtDesignatedFloor&(noSeconds)/*&!emergency*/&!atEmergencyFloor)->keepDoorsState
G(fullyOpenedStateAtDesignatedFloor&(noSeconds|seconds3)/*&!emergency*/&!memEmergency)->keepDoorsState
GF(!memCall0)
GF(!memCall1)
GF(!memCall2)
GF(!memCall3)
G (returnTo0&!floor0)->(goingDown|atEmergencyFloor)
G (atEmergencyFloor->stayInPlace)
G (atEmergencyFloor&!doorsWereFullyOpened&!doorsAreFullyOpened&stayInPlace)->openingDoors
!sound_c
G !stayInPlace -> next(sound_c)
G (stayInPlace) -> (next(!sound_c))
G ((!doorsAreClosed))->(stayInPlace)
G (!atDesignatedFloor&!atEmergencyFloor/*&!atSabbathFloor&(!doorsAreClosed)*/)->keepDoorsState
G closingDoors->next((stayInPlace&(atDesignatedFloor|atEmergencyFloor)&!doorsAreClosed)->(closingDoors|emergency_c))
GF(doorsAreClosed|(atEmergencyFloor&!doorsWereFullyOpened))
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 (atFloor&stayInPlace&next(atDesignatedFloor))->next(stayInPlace)
G (atFloor&!stayInPlace)->next(!stayInPlace|atEmergencyFloor)
G(firstStateAtDesignatedFloor&(noSeconds)&!atEmergencyFloor)->keepDoorsState
G(fullyOpenedStateAtDesignatedFloor&(noSeconds|seconds3)&!memEmergency&!sabbathMode)->keepDoorsState
G(fullyOpenedStateAtDesignatedFloor&(noSeconds|seconds3|seconds5)&!memEmergency&sabbathMode&PREV(keepDoorsState))->(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 (onlyDownCalls&PREV(stayInPlace))->(!goingUp)
G (onlyUpCalls&PREV(stayInPlace))->(!goingDown)
G(firstStateAtDesignatedFloor&(seconds3)&!atEmergencyFloor)->openingDoors
(stayingSameHeigt)&(keepDoorsState)&(!lightIsOn)&(!anyCalls)
G((floor0->(currentFloor=0))& (floor1->(currentFloor=1))& (floor2->(currentFloor=2))& (floor3->(currentFloor=3)))
G(moving -> (doorsAreClosed&keepDoorsState))
G(floor0->!(goingDown))
G(floor3->!(goingUp))
G(moving->(next(lightIsOn)!=lightIsOn))
G((!moving)->(!next(lightIsOn)))
pRespondsToS(calls_c[0],floor0)
G((goingUp->next(!goingDown))&(goingDown->next(!goingUp)))
G(xImpNextY(calls_c[0],memCalls[0])& xImpNextY(calls_c[1],memCalls[1])& xImpNextY(calls_c[2],memCalls[2])& xImpNextY(calls_c[3],memCalls[3]))
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])))
(stayingSameHeigt)&(keepDoorsState)&(!lightIsOn)
(!memCalls[0])&(!memCalls[1])&(!memCalls[2])&(!memCalls[3])
pRespondsToS(calls_c[1],floor1)
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 ((!anyCalls)&(!returnTo0))->!moving
G ((!(anyCalls|floor0))|(atFloorThatCalled&(!moving)))<->countTime_c
G (returnTo0&(!floor0))->goingDown
(!moving)&(keepDoorsState)&(!lightIsOn)
pRespondsToS(calls_c[2],floor2)
pRespondsToS(calls_c[3],floor3)
G moving->next((!moving)<->(atFloorThatCalled|edged_floor))
G ((!(anyCalls|floor0))|(takeCareOfFloor&(!moving)))<->countTime_c
pBecomesTrue_betweenQandR(floor0,returnTo0,goingUp|!moving)
pBecomesTrue_betweenQandR(doorsAreFullyOpened,atFloorThatCalled&(!moving),moving|keepDoorsState|closingDoors)
(!memCalls[0]) & (!memCalls[1]) & (!memCalls[2]) & (!memCalls[3]) 
G (moving -> (doorsAreClosed & keepDoorsState))
G floor0 -> ! (goingDown) 
G floor3 -> ! (goingUp) 
G moving -> (next (lightIsOn) != lightIsOn)
pRespondsToS (calls_c[0], floor0) 
pRespondsToS (calls_c[1], floor1) 
pRespondsToS (calls_c[2], floor2) 
pRespondsToS (calls_c[3], floor3) 
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 ( ((!anyCalls) & (!returnTo0)) | handleFloor) -> !moving
G ( (!(anyCalls | floor0 | moving)) | (handleFloor & (!moving) ))<->countTime_c
pBecomesTrue_betweenQandR (floor0&doorsAreClosed, returnTo0,goingUp|!moving|openningDoors|keepDoorsState) 
pBecomesTrue_betweenQandR(doorsAreFullyOpened, justStoppedAtDesignatedFloor,moving|closingDoors|(keepDoorsState&seconds3)) 
G (!doorsAreClosed)->(!moving)
G (moving&!returnTo0) -> next ((!moving)<->(atDesignatedFloor|edged_floor)) 
G (atDesignatedFloor&!returnTo0)->(!moving)
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 (!handleFloor)->(!openningDoors)
G (!(moving|anyCalls |floor0|returnTo0) | (handleFloor & (doorsAreClosed | doorsAreFullyOpened)))<->countTime_c
G (returnTo0&(!doorsAreClosed))->closingDoors
G (returnTo0&!floor0&doorsAreClosed)->goingDown
G (handleFloor&doorsAreFullyOpened&(!seconds5))->(!closingDoors)
pHolds_afterQuntilR(goingUp,floor0,floor3)
pHolds_afterQuntilR(goingDown,floor3,floor0)
G (((!anyCalls) & (!returnTo0)) | (returnTo0 & floor0)) -> !moving
pHolds_afterQuntilR(!moving,atDesignatedFloor,!atDesignatedFloor)
pHolds_afterQuntilR(!openningDoors,firstMomentAtDesignatedFloor,seconds3)
pHolds_afterQuntilR(openningDoors,firstMomentAtDesignatedFloor&seconds3,doorsAreFullyOpened)
G (/*!(moving|anyCalls |floor0|returnTo0) |*/ firstMomentAtDesignatedFloor | openMomentAtDesignatedFloor)->countTime_c
G moving->(next(!moving)->(atDesignatedFloor|atEdgedFloor))
G (/*!(moving|anyCalls |floor0|returnTo0) |*/ firstStateAtDesignatedFloor | openStateAtDesignatedFloor)<->countTime_c
mode = PARKING & driveMotor = STOP & steeringMotor = STRAIGHT & velocity=0
G steeringMotor != FWD & steeringMotor != BWD & steeringMotor != STOP
G driveMotor != HARD_LEFT & driveMotor != LIGHT_LEFT & driveMotor != STRAIGHT & driveMotor != LIGHT_RIGHT & driveMotor != HARD_RIGHT
G mode = PARKING -> velocity <= 1
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 ) 
GF (mode = PARKED)
pRespondsToS(driveMotor = STOP, driveMotor != STOP | next(velocity) < velocity | velocity=0)
pRespondsToS(driveMotor != STOP, driveMotor = STOP | next(velocity) > velocity | velocity=5)
G forwarding -> frontSense > 0
G(valid_parking_spot) -> (next(mode) = PARKED)
G(mode = PARKED -> stopping)
G driveMotor = STOP -> next(velocity) <= velocity
mode = PARKING & driveMotor = STOP & steeringMotor = STRAIGHT
G (mode = PARKED) <-> (valid_parking_spot = true)
G (PREV(sideSense <= 1)) -> (!right)
G (mode = PARKING) <-> (velocity = 1)
G mode = PARKING -> next(mode = PARKING | mode = PARKED)
G(valid_parking_spot <-> next(mode = PARKED))
G (mode = PARKING & done = false) -> next(mode = PARKING | mode = PARKED)
G(valid_parking_spot <-> 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) 
stopping & senseMotor = REVERSE
GF scanning
G scanning -> forwarding & steeringMotor = STRAIGHT 
G (driveMotor = BWD) -> PREV(senseMotor = REVERSE)
G frontSense = 0 -> driveMotor != FWD
G backSense = 0 & PREV(senseMotor = REVERSE) -> driveMotor != BWD
G reversing -> PREV(senseMotor = REVERSE) & velocity = 1
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
mode = SEARCHING & stopping & steeringMotor = STRAIGHT
G ((frontSense <= 2) & (mode !=EXIT)) -> (((driveMotor != FWD) | steeringMotor = HARD_LEFT & next(mode = SEARCHING)))
G ((mode = SCANNING | mode = PARKING | mode = EXIT) /*| mode = EXIT*/ & driveMotor != STOP | reversing) -> (velocity = 1)
G (mode = SCANNING) -> PREV(mode != PARKED)
G (mode = SCANNING) -> PREV(mode != PARKING)
G ((mode = SCANNING) & (status = NONE | (status = REVERSE & sideStatus = MIN_PARALLEL)) & frontSense > 2) -> (steeringMotor = STRAIGHT & driveMotor = FWD)
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 (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 = 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) -> PREV(mode != SEARCHING)
G (mode = PARKING) -> PREV(mode != PARKED)
G (mode = PARKING) -> PREV(mode != EXIT)
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 = PARKED) -> PREV(mode != SEARCHING)
G (mode = PARKED) -> PREV(mode != SCANNING)
G (mode = PARKED) -> PREV(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 = EXIT) -> PREV(mode != SEARCHING)
G (mode = EXIT) -> PREV(mode != SCANNING)
G(mode = PARKING & valid_parking_spot) <-> (next(mode) = PARKED)
G(mode = PARKED) -> (next(mode) = EXIT)
mode = SEARCHING & senseMotor = SIDE & steeringMotor = STRAIGHT
G mode = SEARCHING | mode = SCANNING -> senseMotor = SIDE
G mode = SCANNING & frontSense > 2 & sideSense > 2 -> senseMotor = SIDE & next(mode) = SCANNING & driveMotor = FWD & steeringMotor = STRAIGHT
G mode = PARKING & status = PARALLEL & backSense > 2 -> PREV(senseMotor = BACK) & driveMotor = BWD & next(mode) = PARKING & steeringMotor = HARD_RIGHT
G mode = PARKING & status = PARALLEL & backSense <= 2 & backSense > 1 -> PREV(senseMotor = BACK) & driveMotor = BWD & next(mode) = PARKING & steeringMotor = HARD_LEFT
G mode = PARKING & status = PARALLEL & backSense <= 1 -> PREV(senseMotor = BACK) & driveMotor = STOP & next(mode) = PARKED & steeringMotor = STRAIGHT
G mode = PARKED -> next(mode) = PARKED & driveMotor = STOP & steeringMotor = STRAIGHT
G backSense = 0 & PREV(senseMotor = BACK) -> driveMotor = FWD
G reversing -> PREV(senseMotor = BACK) & velocity = 1
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 = 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 (PREV(mode = SCANNING) & status = PARALLEL) -> (mode = PARKING)
G (status = PARALLEL & mode = PARKING & sideSense <= 1 & steeringMotor = STRAIGHT & driveMotor = STOP) <-> (next(mode) = PARKED)
GF mode = PARKED
G (mode = PARKED) -> (driveMotor = STOP & steeringMotor = STRAIGHT)
G (frontSense <= 2 & (mode = SCANNING | mode = SEARCHING) & status = NONE) -> (senseMotor = SIDE & next(mode) = SEARCHING & driveMotor = FWD & steeringMotor = HARD_LEFT)
G driveMotor = BWD -> backSense > 0 & PREV(senseMotor = BACK)
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)
GF (mode = PARKING -> driveMotor != STOP)
mode = SEARCHING & senseMotor = SIDE & steeringMotor = STRAIGHT & stopping
G ((mode = SCANNING) & status = NONE & frontSense > 2) -> (steeringMotor = STRAIGHT & driveMotor = FWD)
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 & stopping) <-> (next(mode) = PARKED)
G (mode = PARKING) -> (next(mode) != SEARCHING & next(mode) != SCANNING)
G (frontSense <= 2) -> (driveMotor != FWD)
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))))
G reversing -> velocity = 1
G driveMotor = STOP <-> velocity = 0
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 (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)))
GF (mode = PARKED | mode = EXIT)
G (((sense = BLOCKED) & (senseMotor =DRIVE)) -> ! forwarding)
G (((sense = BLOCKED) & (senseMotor = REVERSE)) -> ! reversing)
G(mode = PARKED) -> (next(mode) = PARKED)
G(mode = PARKED & !button) -> (next(mode) = PARKED)
G(mode = PARKED & button) -> (next(mode) = EXIT)
G (((sense = BLOCKED) & (senseMotor = DRIVE)) -> ! forwarding)
G forwarding -> senseMotor = DRIVE
G reversing -> senseMotor = REVERSE
GF parked
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
GF reverseParking | parallelParking
pRespondsToS(deepEnoughtToPark, reverseParking)
pRespondsToS(wideEnoughtToPark, parallelParking)
GF (mode = PARKED | manual = true | button = true)
G ((frontSense <= 2) & (mode !=EXIT)) -> (((driveMotor != FWD) | (steeringMotor = HARD_LEFT & next(mode = SEARCHING)) | next(mode = MANUAL)))
G ((mode = SCANNING | mode = PARKING | mode = EXIT) & driveMotor != STOP | reversing) -> (velocity = 1)
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 (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 = 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 = MANUAL & frontSense > 2 -> (driveMotor = driveCmd & steeringMotor = steeringCmd))
G (manual = true <-> mode = MANUAL)
GF (mode = PARKED | manual = true)
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 = MANUAL & frontSense > 2) -> (driveMotor = driveCmd & steeringMotor = steeringCmd))
G (manual = true) <-> (next(mode) = MANUAL)
G ((mode = MANUAL & frontSense <= 2) -> (driveMotor = STOP & steeringMotor = steeringCmd))
parkingMode = NONE
G scanning -> forwarding
pRespondsToS(foundAParallelSpot, parallelParking)
pRespondsToS(foundAReverseSpot, reverseParking)
G senseMotor = REVERSE -> velocity = 1
senseMotor = DRIVE
stopping & senseMotor = DRIVE & parkingMode = NONE & steeringMotor = 45
stopping & senseMotor = SCANNING & steeringMotor = STRAIGHT
G (driveMotor = BWD & backSense != BLOCKED) -> senseMotor = REVERSE
G frontSense = BLOCKED -> driveMotor != FWD
G (backSense = BLOCKED & steeringMotor = STRAIGHT & senseMotor = REVERSE) -> driveMotor != BWD
GF forwarding & steeringMotor = STRAIGHT
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
stopping & steeringMotor = STRAIGHT & senseMotor = REVERSE
G frontSense = 5 -> velocity = 5
G frontSense = 4 -> velocity = 4
G frontSense = 3 -> velocity = 3
G frontSense = 2 -> velocity = 2
mode = SEARCHING & steeringMotor = STRAIGHT & stopping
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)
GF (stopping & (status = PARALLEL | status = REVERSE) & mode = PARKING) 
G ( sideSense <= 1) -> (steeringMotor = STRAIGHT)
G (frontSense = 3 & (mode = SCANNING) & !stopping) -> (velocity = 1)
G (frontSense <= 2) -> ((driveMotor != FWD) | steeringMotor = HARD_LEFT)
pRespondsToS( ((mode = SEARCHING | mode = SCANNING) & (sideSense > 1)), mode != SEARCHING | mode != SCANNING | sideSense = 1)
mode = INIT
!initDone
G next(initDone) = (mode = INIT | initDone)
G initDone -> mode != INIT
GF (task = SORT) -> sorted
G (task = SORT & sorted & mode != INIT) -> mode = NOTHING
G (task = EXCHANGE & initDone) -> (mode = MOVE & incrementFrom)
G (mode = MOVE) -> (fromExists & toExists & toIsEmpty & from != to)
G assign(a, aColor)
G assign(b, bColor)
G assign(a, aColor) & assign(b, bColor)
a!=b
G next(a)!=next(b)
G (isMoving) -> (fromColor != NOT & toColor = EMPTY)
G assign(from, fromColor)
G assign(to, toColor)
from != to
G next(from) != next(to)
GF (task = SORT & sortAsms) -> sortDone
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)
GF (task = HANOI & hanoiAsms) -> hanoiDone
G task = HANOI & hanoiDone -> !isMoving
G task = HANOI & isMoving -> hanoiLegalMove
G task = EXCHANGE -> (isMoving & incrementFrom)
GF (task = GATHER_REDS & gatherRedsAsms) -> gatherRedsDone
G (task = GATHER_REDS & gatherRedsDone) -> !isMoving
GF (task = MOVE_RED_LEFT & moveRedLeftAsms) -> moveRedLeftDone
G (task = MOVE_RED_LEFT & moveRedLeftDone) -> !isMoving
G (swapRedAndBlueAsms & task = SWAP_RED_AND_BLUE) -> ((fromColor = RED -> next(fromColor) = BLUE) & (fromColor = BLUE -> next(fromColor) = RED))
G (isMoving ) -> (fromColor != NOT & toColor = EMPTY)
G next(assign(from, fromColor))
G next(assign(to, toColor))
G next(hanoiAssign(hanoiFrom, hanoiFromColor))
G next(hanoiAssign(hanoiTo, hanoiToColor))
G task = HANOI & hanoiDone -> !hanoiIsMoving
G task = HANOI & hanoiIsMoving -> hanoiLegalMove
G hanoiIsMoving -> task = HANOI
G next(hanoiFrom) != next(hanoiTo)
G isMoving -> task != HANOI
G (swapRedAndBlueAsms & task = SWAP_RED_AND_BLUE) -> isMoving & ((fromColor = RED -> next(fromColor) = BLUE) & (fromColor = BLUE -> next(fromColor) = RED))
GF task = HANOI -> hanoiDone
assign(from, fromColor)
assign(to, toColor)
hanoiAssign(hanoiFrom, hanoiFromColor)
hanoiAssign(hanoiTo, hanoiToColor)
G !hanoiIsMoving -> hanoiFrom = 0 & hanoiTo = 1
G task = SORT & !sortDone -> isMoving
G task = HANOI -> !isMoving
G task = HANOI & !hanoiDone -> hanoiIsMoving
GF task = SORT -> sortDone
GF (task = GATHER_REDS) -> gatherRedsDone
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 task = HANOI & !hanoiIsMoving -> next(r0) = r0 & next(r1) = r1 & next(r2) = r2 
G task != HANOI -> next(initRs)
GF (task = MOVE_RED_LEFT) -> moveRedLeftDone
G task = MOVE_RED_LEFT & isMoving -> fromColor = RED
G task != HANOI -> next(initCounters)
!secondStep
G next(secondStep) = (mode = INIT)
GF sortingAssumptions -> sorted
G (sorted & mode != INIT) -> mode = STOP
G (mode = MOVE) -> (fromExists & toExists & toIsEmpty)
GF sorted
G (sorted & mode != INIT) -> mode = NOTHING
