compute R' from the following FSM

Question

For above FSM constructed kripke structure and compute R',but my solution is incorrect.

Answer 1

For the following FSM

    state var: p,q
    inp. var: a
    init q
    trans a&p&!q&next(p)&next(q) | a&q&!p&next(p)&next(q) | a&q&!next(p)&next(q) 

which looks as follows

we find this associated Kripke structure:

There are deadend states and unreachable states that we would like to remove from the set of transitions. The deadend states s0,s1,s2,s4,s6 are described by 

    !p&!q&!a | !p&!q&a | !p&q&!a | p&!q&!a | p&q&!a

and the unreachable states s0,s1,s4,s5 by

    !p&!q&!a | !p&!q&a | p&!q&!a | p&!q&a

so that our updated transition relation should be

    R' := 
        R 
        & !(!p&!q&!a | !p&!q&a | p&!q&!a | p&!q&a) 
        & !(!next(p)&!next(q)&!next(a) |
            !next(p)&!next(q)& next(a) | 
            !next(p)& next(q)&!next(a) | 
             next(p)&!next(q)&!next(a) | 
             next(p)& next(q)&!next(a)
           )

and we also remove the deadends from the initial states

    I' := I & !(!p&!q&!a | !p&!q&a | !p&q&!a | p&!q&!a | p&q&!a)

which is the following structure

So, your result is missing a transition. 

Comments

thanks updated.how to write for below question this part is confusing because  my solution is incorrect :
c) R1 is obtained by removing the transitions to deadends in R′. Construct a propositional logic formula for R1.Submit your solution in the form:a&p&q&next(p)&!next(q) | a&!p&!q&next(p)&next(q)

my solution:
after removing dead ends:
p&a&!q&next(p)&next(q)&next(a)| p&a&q&next(q)&!next(p)&!next(a) | q&a&!p&next(q)&!next(p)&next(a) |!p&a&q&next(q)&next(p)&next(a)

after removing unreachable nodes:
p&a&q&next(q)&!next(p)&!next(a) | q&a&!p&next(q)&!next(p)&next(a) |!p&a&q&next(q)&next(p)&next(a)

---

your solution after removing dead ends still contains s2:{q} which is a dead end