G(!(state = Q3))
G(!(spec_state = Q3))
G(HeadMotor = STOP)
G((spec_counter <= counterLimit))
G (forwarding | backwarding | stopping)
G addTasks
G keepTasksStatus
G taskWillBeFalse
G updateTasks
G !turning
G (!moving)
G (keepDoorsState)
G !lightIsOn
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 steeringMotor != FWD & steeringMotor != BWD & steeringMotor != STOP
G driveMotor != HARD_LEFT & driveMotor != LIGHT_LEFT & driveMotor != STRAIGHT & driveMotor != LIGHT_RIGHT & driveMotor != HARD_RIGHT
G assign(a, aColor)
G assign(b, bColor)
G assign(a, aColor) & assign(b, bColor)
G assign(from, fromColor)
G assign(to, toColor)
