Determining totally defined automaton from symbolic representation of automaton

Question

In protocol of 15.02.2017 problem 8 d) part ii), the following automaton has been given and asked to convert to LO2 formula:

A∀({p}, 1,(p ∧ Xp ∧ a), G¬p) ∨ A∀({}, 1, 1, q)

The following is the solution 

= ¬A∃({p}, 1,(p ∧ Xp ∧ a), Fp) ∨ A∀({}, 1, 1, q) 

// A∃({p}, 1,(p ∧ Xp ∧ a) is not totally defined. 

= ¬Ga ∨ q 

I have two questions regarding this solution:

a) How did you you say that the first automaton is not totally defined?

b) And after saying it is not totally defined, how did you end up with  "¬Ga ∨ q "?

Answer 1

a) The automaton has no transitions for !a or !p. Hence, it is not total.

b) We can conclude that the said automaton only has infinite paths if there is nothing else but a. Hence we know the negation ¬Ga. The other automaton has no state variables. Hence, q is an input variable. Hence, the automaton just requires q in the first step.

The resulting formula is just a disjunction between the two findings we had about these automata.