The function checks if the automaton in the current window accepts no words. If the current automaton is not empty, one counterexample (an infinite word) will be shown. (The transitions which the counterexample passes through will be highlighted.)