I'm not familiar with the SMV notation, so I am guessing about this, but the key points are:
To avoid quantifying over all states at the outside: you don't want to say that all games can be either won or lost, but only the starting game. So just have a formula at the starting state with no outermost modality
To use a conjunction, not disjunction: you want to assert both winnability and losability
You need separate modalities wrapping each of the branches: winnability, losability is an existential claim, saying it is possible to attain a condition.
I think the formula you need is: (EG SOG=Win) & (EG SOG=Lose) at the root, which might mean in something like an init/start clause, or asserting at a named root clause. If SMV doesn't have the EG modality, you can translate into just AG using the equivalence EG p = !(AG !p), since the two are De Morgan duals.