Event-based synthesis analysis tool has wrong conclusion

Consider plant G and requirement H, as shown below. The synchronous product has 10 states. The synthesized supervisor has 6 states (also shown below).

Yet, the synthesis analysis tool shows the following message:

Synthesis analysis tool
1 plant automaton.
1 requirement automaton.
Synthesis created 10 states, removed 2 states, giving 8 states in the result.

It incorrectly states that 2 states were removed and 8 states remain. In reality, 4 states were removed, and 6 remained.

plant G:
    location G0: initial;
        edge a1 goto G1;
        edge a2 goto G3;

    location G1:
        edge b1 goto G2;
        edge a2 goto G4;

    location G2:
        edge a2 goto G5;

    location G3:
        edge a1 goto G4;
        edge b2 goto G6;

    location G4:
        edge b1 goto G5;
        edge b2 goto G7;

    location G5:
        edge b2 goto G8;

    location G6:
        edge a1 goto G7;

    location G7:
        edge b1 goto G8;

    location G8: marked;

end

requirement H:
    location H0: initial;
        edge a1 goto H1;
        edge a2 goto H3;

    location H1:
        edge b1 goto H2;
        edge a2 goto H9;

    location H2:
        edge a2 goto H5;

    location H3:
        edge a1 goto H4;
        edge b2 goto H6;

    location H4:
        edge b2 goto H7;

    location H9:
        edge b1 goto H5;

    location H5:
        edge b2 goto H8;

    location H6:
        edge a1 goto H7;

    location H7:
        edge b1 goto H8;

    location H8: marked;

end

controllable a1;
uncontrollable a2;
controllable b1;
uncontrollable b2;
supervisor automaton S:
  alphabet a1, a2, b1, b2;
  location s1:
    initial;
    edge a2 goto s2;
  location s2:
    edge b2 goto s3;
    edge a1 goto s4;
  location s3:
    edge a1 goto s5;
  location s4:
    edge b2 goto s5;
  location s5:
    edge b1 goto s6;
  location s6:
    marked;
end