Good question!
Yes, you are right, and the solution has a little bug. Let us clarify this. First of all, your formula for the right hand side of X r1 is perfect, and it can be simplified as follows:
X r1 <-> (r0 & !r1 & a) | (r0 & !r1 & !a) | (!r0 & r1 & !a) | (r0 & r1)
<-> (r0 & !r1 & (a | !a)) | (!r0 & r1 & !a) | (r0 & r1)
<-> (r0 & !r1) | (!r0 & r1 & !a) | (r0 & r1)
<-> (r0 & !r1) | (r0 & r1) | (!r0 & r1 & !a)
<-> (r0 & (!r1 | r1)) | (!r0 & r1 & !a)
<-> r0 | (!r0 & r1 & !a)
<-> r0 | r1 & !a
So, we should use the above formula (which would be fine). It is certainly not equivalent to true. The state transition diagram obtained for this formula looks as follows where we have a self-loop on the unreachable state s0:
However, symbolic representations of transition relations are not uniquely defined. We may modify them on the unreachable states as we like, and can use this to minimize the formulas or their BDD representations.
Looking at the state transitition diagram, you can see that the state !r0&!r1, i.e. state s0, is not reachable. Taking this into account, we can simplify the formula as follows:
X r1 <-> r0 | !a
Note that r0 | r1 & !a and r0 | !a are not equivalent, but they only differ if !r0&!r1&!a holds, i.e., on the not reachable state which we don't care. The above formulas has been obtained by logic minimization with a don't care formula !r0&!r1. This way, our transition system looks as follows:
As you can see, we have the same transitions on the reachable states, but on the unreachable state, there are now two transitions. But we don't care about transitions on the unreachable states.
The example solution had a bug in that it has been written that all transitions lead to states where next r1 holds, and that we can therefore use X r1 <-> true. The same has been written for the other transition relation for state variable s1. While that is true for s1, it is not true for r1, since there is a transition {r1} -> {r0} where next time r1 is false. So, the given transition relation is indeed incorrect. Its transition system would looks as follows:
Now transitions on the reachable states also changed since the transition {r1} -> {r0} with input a is lost. This is therefore not correct.
Still, as you can see, the transition relation can be modified such that the transitions on the unreachable states change, and this can be used to simplify the transition relation.
If that all sounds too complicated, don't worry: Using X r1 <-> r0 | r1 & !a is perfectly fine as well, since you can see above that the transition on the reachable states are exactly the same.
