To translate F[a WB b] ∨ [a WU (F c)] to an equivalent omega-automaton, we will abbreviate
- q0 := [a WB b]
- q1 := F q0
- q2 := F c
- q3 := [a WU q2]
Next, we replace these definitions by transition relations and fairness constraints. For each state variable, we would get one fairness constraint:
- q0 yields GF[q0∨b]
- q1 yields GF[q1->q0])
- q2 yields GF[q2->c])
- q3 yields GF[a->q3]
In the example solution, you find the fairness constraints for q1 and q2, but you miss the other two. You may safely add one or both of them if you want, the solution will be correct with them also. However, since they stem from weak operators with positive occurrences, you may omit them also if you want. See the slides of the related chapter that mentions this optimization after the unoptimized procedure has been explained.
