G (spec_pausing = GO & !spec_dropping & starting_pos = NO & verhor_dontmove <-> botMot = RETURN)
G (spec_pausing = GO & !spec_dropping & starting_pos = YES & nonemove & color != BLACK <-> verMot = MOVE)
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 (spec_allsleep = true <-> verMot = SLEEP & horMot = SLEEP & botMot = STOP)
G (spec_finished_cycle <-> reduce_num_of_cubes = REDUCE)
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 (store_place = true <-> (spec_stage = TOANGLERIGHT | spec_stage = TOANGLELEFT) & spec_pausing = go & detect = botMotColor)
G (horMot = MOVE <-> spec_dropping & detect = spec_currentColor)
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)
G ((spec_turnState = T2) <-> (LeftMotor = BWD & RightMotor = TURN_BWD))
G ((InputMoveMode = TURN_LEFT_1) <-> (OutputMoveMode = TURN_LEFT_2))
G (spec_turnState = T2 <-> (LeftMotor = BWD & RightMotor = TURN_BWD))
G (!waitingForDoor & ((atStation & atEmgState & openDoorAtEmgState)| atStationWithTask)) <-> doorReq
G noPressedStations & !atEmgState <-> countTimeSinceReqs
G (atStation & stopAtNearestStation) & (doorStatus = CLOSED) & (!doorCounterIncreased) <-> openDoorReq
G ( (doorStatus = OPENED) <-> closeDoorReq)
G (atStation & (stopAtNearestStation| taskAtCurrentStation(station))) & (doorStatus = CLOSED) & (!doorCounterIncreased) <-> openDoorReq
G (!stopping <-> beep = 1)
G (accelerating <-> (accelLeft | accelRight))
G ((!(anyCalls|floor0))|(atFloorThatCalled&(!moving)))<->countTime_c
G ((!(anyCalls|floor0))|(takeCareOfFloor&(!moving)))<->countTime_c
G ( (!(anyCalls | floor0 | moving)) | (handleFloor & (!moving) ))<->countTime_c
G (!(moving|anyCalls |floor0|returnTo0) | (handleFloor & (doorsAreClosed | doorsAreFullyOpened)))<->countTime_c
G (/*!(moving|anyCalls |floor0|returnTo0) |*/ firstStateAtDesignatedFloor | openStateAtDesignatedFloor)<->countTime_c
G (mode = PARKED) <-> (valid_parking_spot = true)
G (mode = PARKING) <-> (velocity = 1)
G(valid_parking_spot <-> mode = PARKED)
G driveMotor = STOP <-> velocity = 0
G (manual = true <-> mode = MANUAL)
