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.