Remove unique state annotations within an automaton constraint

We added this constrain in #714 (closed), but it turns out that this constraint is violated in practice. For instance, event-based automaton projection may produce models that violate this constraint. After minimization, I think the constraint should hold again. But, the result of projection should be a valid model. Hence, I think we should remove the constraint.